Version 2A1 |
Version 2A2 |
aarity |
aarity |
destruct_apair_apair_aux |
destruct_apair_apair_aux |
discr_apair_xy_x |
discr_apair_xy_x |
discr_tpair_xy_y |
discr_apair_xy_y |
eq_aarity_dec |
eq_aarity_dec |
item0 |
item0 |
bind2 |
bind2 |
flat2 |
flat2 |
item2 |
item2 |
destruct_sort_sort_aux |
destruct_sort_sort_aux |
eq_item0_dec |
eq_item0_dec |
eq_bind2_dec |
eq_bind2_dec |
eq_flat2_dec |
eq_flat2_dec |
eq_item2_dec |
eq_item2_dec |
sh |
sh |
sh_N |
sh_N |
nexts_le |
nexts_le |
nexts_lt |
nexts_lt |
nexts_dec |
nexts_dec |
nexts_inj |
nexts_inj |
sd |
sd |
deg_O |
deg_O |
sd_O |
sd_O |
deg_SO |
deg_SO |
deg_SO_inv_pos_aux |
deg_SO_inv_succ_aux |
deg_SO_inv_pos |
deg_SO_inv_succ |
deg_SO_refl |
deg_SO_refl |
deg_SO_gt |
deg_SO_gt |
sd_SO |
sd_SO |
sd_d |
sd_d |
deg_inv_pred |
deg_inv_pred |
deg_inv_prec |
deg_inv_prec |
deg_iter |
deg_iter |
deg_next_SO |
deg_next_SO |
sd_d_SS |
sd_d_SS |
sd_d_correct |
sd_d_correct |
term |
term |
eq_term_dec |
eq_term_dec |
destruct_tatom_tatom_aux |
destruct_tatom_tatom_aux |
destruct_tpair_tpair_aux |
destruct_tpair_tpair_aux |
discr_tpair_xy_x |
discr_tpair_xy_x |
discr_tpair_xy_y |
discr_tpair_xy_y |
eq_false_inv_tpair_sn |
eq_false_inv_tpair_sn |
eq_false_inv_tpair_dx |
eq_false_inv_tpair_dx |
tw |
tw |
tw_pos |
tw_pos |
simple |
simple |
simple_inv_bind_aux |
simple_inv_bind_aux |
simple_inv_bind |
simple_inv_bind |
simple_inv_pair |
simple_inv_pair |
lenv |
lenv |
eq_lenv_dec |
eq_lenv_dec |
destruct_lpair_lpair_aux |
destruct_lpair_lpair_aux |
discr_lpair_x_xy |
discr_lpair_x_xy |
|
discr_lpair_xy_x |
|
ceq |
|
cfull |
lw |
lw |
lw_pair |
lw_pair |
length |
length |
length_inv_zero_dx |
length_inv_zero_dx |
length_inv_zero_sn |
length_inv_zero_sn |
length_inv_pos_dx |
length_inv_succ_dx |
length_inv_pos_sn |
length_inv_succ_sn |
|
length_atom |
|
length_pair |
genv |
genv |
eq_genv_dec |
eq_genv_dec |
rfw |
rfw |
rfw_shift |
rfw_shift |
rfw_tpair_sn |
rfw_tpair_sn |
rfw_tpair_dx |
rfw_tpair_dx |
rfw_lpair_sn |
rfw_lpair_sn |
rfw_lpair_dx |
rfw_lpair_dx |
da |
da |
da_inv_sort_aux |
da_inv_sort_aux |
da_inv_sort |
da_inv_sort |
da_inv_lref_aux |
da_inv_lref_aux |
da_inv_lref |
da_inv_lref |
da_inv_gref_aux |
da_inv_gref_aux |
da_inv_gref |
da_inv_gref |
da_inv_bind_aux |
da_inv_bind_aux |
da_inv_bind |
da_inv_bind |
da_inv_flat_aux |
da_inv_flat_aux |
da_inv_flat |
da_inv_flat |
lstas |
lstas |
lstas_inv_sort1_aux |
lstas_inv_sort1_aux |
lstas_inv_sort1 |
lstas_inv_sort1 |
lstas_inv_lref1_aux |
lstas_inv_lref1_aux |
lstas_inv_lref1 |
lstas_inv_lref1 |
lstas_inv_lref1_O |
lstas_inv_lref1_O |
lstas_inv_lref1_S |
lstas_inv_lref1_S |
lstas_inv_gref1_aux |
lstas_inv_gref1_aux |
lstas_inv_gref1 |
lstas_inv_gref1 |
lstas_inv_bind1_aux |
lstas_inv_bind1_aux |
lstas_inv_bind1 |
lstas_inv_bind1 |
lstas_inv_appl1_aux |
lstas_inv_appl1_aux |
lstas_inv_appl1 |
lstas_inv_appl1 |
lstas_inv_cast1_aux |
lstas_inv_cast1_aux |
lstas_inv_cast1 |
lstas_inv_cast1 |
|
|
lift |
lift |
lift_inv_O2_aux |
lift_inv_O2_aux |
lift_inv_O2 |
lift_inv_O2 |
lift_inv_sort1_aux |
lift_inv_sort1_aux |
lift_inv_sort1 |
lift_inv_sort1 |
lift_inv_lref1_aux |
lift_inv_lref1_aux |
lift_inv_lref1 |
lift_inv_lref1 |
lift_inv_lref1_lt |
lift_inv_lref1_lt |
lift_inv_lref1_ge |
lift_inv_lref1_ge |
lift_inv_gref1_aux |
lift_inv_gref1_aux |
lift_inv_gref1 |
lift_inv_gref1 |
lift_inv_bind1_aux |
lift_inv_bind1_aux |
lift_inv_bind1 |
lift_inv_bind1 |
lift_inv_flat1_aux |
lift_inv_flat1_aux |
lift_inv_flat1 |
lift_inv_flat1 |
lift_inv_sort2_aux |
lift_inv_sort2_aux |
lift_inv_sort2 |
lift_inv_sort2 |
lift_inv_lref2_aux |
lift_inv_lref2_aux |
lift_inv_lref2 |
lift_inv_lref2 |
lift_inv_lref2_lt |
lift_inv_lref2_lt |
lift_inv_lref2_be |
lift_inv_lref2_be |
lift_inv_lref2_ge |
lift_inv_lref2_ge |
lift_inv_gref2_aux |
lift_inv_gref2_aux |
lift_inv_gref2 |
lift_inv_gref2 |
lift_inv_bind2_aux |
lift_inv_bind2_aux |
lift_inv_bind2 |
lift_inv_bind2 |
lift_inv_flat2_aux |
lift_inv_flat2_aux |
lift_inv_flat2 |
lift_inv_flat2 |
lift_inv_pair_xy_x |
lift_inv_pair_xy_x |
lift_inv_pair_xy_y |
lift_inv_pair_xy_y |
lift_fwd_pair1 |
lift_fwd_pair1 |
lift_fwd_pair2 |
lift_fwd_pair2 |
lift_fwd_tw |
lift_fwd_tw |
lift_simple_dx |
lift_simple_dx |
lift_simple_sn |
lift_simple_sn |
lift_lref_ge_minus |
lift_lref_ge_minus |
lift_lref_ge_minus_eq |
lift_lref_ge_minus_eq |
lift_refl |
lift_refl |
lift_total |
lift_total |
lift_split |
lift_split |
is_lift_dec |
is_lift_dec |
drop |
drop |
d_liftable |
d_liftable |
d_deliftable_sn |
d_deliftable_sn |
dropable_sn |
dropable_sn |
dropable_dx |
dropable_dx |
drop_inv_atom1_aux |
drop_inv_atom1_aux |
drop_inv_atom1 |
drop_inv_atom1 |
drop_inv_O1_pair1_aux |
drop_inv_O1_pair1_aux |
drop_inv_O1_pair1 |
drop_inv_O1_pair1 |
drop_inv_pair1 |
drop_inv_pair1 |
drop_inv_drop1_lt |
drop_inv_drop1_lt |
drop_inv_drop1 |
drop_inv_drop1 |
drop_inv_skip1_aux |
drop_inv_skip1_aux |
drop_inv_skip1 |
drop_inv_skip1 |
drop_inv_O1_pair2 |
drop_inv_O1_pair2 |
drop_inv_skip2_aux |
drop_inv_skip2_aux |
drop_inv_skip2 |
drop_inv_skip2 |
drop_inv_O1_gt |
drop_inv_O1_gt |
drop_refl_atom_O2 |
drop_refl_atom_O2 |
drop_refl |
drop_refl |
drop_drop_lt |
drop_drop_lt |
drop_skip_lt |
drop_skip_lt |
drop_O1_le |
drop_O1_le |
drop_O1_lt |
drop_O1_lt |
drop_O1_pair |
drop_O1_pair |
drop_O1_ge |
drop_O1_ge |
drop_O1_eq |
drop_O1_eq |
drop_split |
drop_split |
drop_FT |
drop_FT |
drop_gen |
drop_gen |
drop_T |
drop_T |
d_liftable_LTC |
d_liftable_LTC |
d_deliftable_sn_LTC |
d_deliftable_sn_LTC |
dropable_sn_TC |
dropable_sn_TC |
dropable_dx_TC |
dropable_dx_TC |
d_deliftable_sn_llstar |
d_deliftable_sn_llstar |
drop_fwd_drop2 |
drop_fwd_drop2 |
drop_fwd_length_ge |
drop_fwd_length_ge |
drop_fwd_length_le_le |
drop_fwd_length_le_le |
drop_fwd_length_le_ge |
drop_fwd_length_le_ge |
drop_fwd_length |
drop_fwd_length |
drop_fwd_length_minus2 |
drop_fwd_length_minus2 |
drop_fwd_length_minus4 |
drop_fwd_length_minus4 |
drop_fwd_length_le2 |
drop_fwd_length_le2 |
drop_fwd_length_le4 |
drop_fwd_length_le4 |
drop_fwd_length_lt2 |
drop_fwd_length_lt2 |
drop_fwd_length_lt4 |
drop_fwd_length_lt4 |
drop_fwd_length_eq1 |
drop_fwd_length_eq1 |
drop_fwd_length_eq2 |
drop_fwd_length_eq2 |
drop_fwd_lw |
drop_fwd_lw |
drop_fwd_lw_lt |
drop_fwd_lw_lt |
drop_fwd_rfw |
drop_fwd_rfw |
drop_inv_O2_aux |
drop_inv_O2_aux |
drop_inv_O2 |
drop_inv_O2 |
drop_inv_length_eq |
drop_inv_length_eq |
drop_inv_refl |
drop_inv_refl |
drop_inv_FT_aux |
drop_inv_FT_aux |
drop_inv_FT |
drop_inv_FT |
drop_inv_gen |
drop_inv_gen |
drop_inv_T |
drop_inv_T |
lsubr |
lsubr |
lsubr_refl |
lsubr_refl |
lsubr_inv_atom1_aux |
lsubr_inv_atom1_aux |
lsubr_inv_atom1 |
lsubr_inv_atom1 |
lsubr_inv_abst1_aux |
lsubr_inv_abst1_aux |
lsubr_inv_abst1 |
lsubr_inv_abst1 |
lsubr_inv_abbr2_aux |
lsubr_inv_abbr2_aux |
lsubr_inv_abbr2 |
lsubr_inv_abbr2 |
lsubr_fwd_length |
lsubr_fwd_length |
lsubr_fwd_drop2_pair |
lsubr_fwd_drop2_pair |
lsubr_fwd_drop2_abbr |
lsubr_fwd_drop2_abbr |
cpr |
cpr |
lsubr_cpr_trans |
lsubr_cpr_trans |
tpr_cpr |
tpr_cpr |
cpr_refl |
cpr_refl |
cpr_pair_sn |
cpr_pair_sn |
cpr_delift |
cpr_delift |
lstas_cpr_aux |
lstas_cpr_aux |
lstas_cpr |
lstas_cpr |
cpr_inv_atom1_aux |
cpr_inv_atom1_aux |
cpr_inv_atom1 |
cpr_inv_atom1 |
cpr_inv_sort1 |
cpr_inv_sort1 |
cpr_inv_lref1 |
cpr_inv_lref1 |
cpr_inv_gref1 |
cpr_inv_gref1 |
cpr_inv_bind1_aux |
cpr_inv_bind1_aux |
cpr_inv_bind1 |
cpr_inv_bind1 |
cpr_inv_abbr1 |
cpr_inv_abbr1 |
cpr_inv_abst1 |
cpr_inv_abst1 |
cpr_inv_flat1_aux |
cpr_inv_flat1_aux |
cpr_inv_flat1 |
cpr_inv_flat1 |
cpr_inv_appl1 |
cpr_inv_appl1 |
cpr_inv_appl1_simple |
cpr_inv_appl1_simple |
cpr_inv_cast1 |
cpr_inv_cast1 |
cpr_fwd_bind1_minus |
cpr_fwd_bind1_minus |
cnr |
cnr |
cnr_inv_delta |
cnr_inv_delta |
cnr_inv_abst |
cnr_inv_abst |
cnr_inv_abbr |
cnr_inv_abbr |
cnr_inv_zeta |
cnr_inv_zeta |
cnr_inv_appl |
cnr_inv_appl |
cnr_inv_eps |
cnr_inv_eps |
cnr_sort |
cnr_sort |
cnr_lref_free |
cnr_lref_free |
cnr_lref_atom |
cnr_lref_atom |
cnr_abst |
cnr_abst |
cnr_appl_simple |
cnr_appl_simple |
cnr_dec |
cnr_dec |
cprs |
cprs |
cprs_ind |
cprs_ind |
cprs_ind_dx |
cprs_ind_dx |
cpr_cprs |
cpr_cprs |
cprs_refl |
cprs_refl |
cprs_strap1 |
cprs_strap1 |
cprs_strap2 |
cprs_strap2 |
lsubr_cprs_trans |
lsubr_cprs_trans |
tprs_cprs |
tprs_cprs |
cprs_bind_dx |
cprs_bind_dx |
cprs_flat_dx |
cprs_flat_dx |
cprs_flat_sn |
cprs_flat_sn |
cprs_zeta |
cprs_zeta |
cprs_eps |
cprs_eps |
cprs_beta_dx |
cprs_beta_dx |
cprs_theta_dx |
cprs_theta_dx |
cprs_inv_sort1 |
cprs_inv_sort1 |
cprs_inv_cast1 |
cprs_inv_cast1 |
cprs_inv_cnr1 |
cprs_inv_cnr1 |
scpds |
scpds |
sta_cprs_scpds |
sta_cprs_scpds |
lstas_scpds |
lstas_scpds |
scpds_strap1 |
scpds_strap1 |
scpds_fwd_cprs |
scpds_fwd_cprs |
scpes |
scpes |
scpds_div |
scpds_div |
scpes_sym |
scpes_sym |
lift_inj |
lift_inj |
lift_div_le |
lift_div_le |
lift_div_be |
lift_div_be |
lift_mono |
lift_mono |
lift_trans_be |
lift_trans_be |
lift_trans_le |
lift_trans_le |
lift_trans_ge |
lift_trans_ge |
lift_conf_O1 |
lift_conf_O1 |
lift_conf_be |
lift_conf_be |
drop_mono |
drop_mono |
drop_conf_ge |
drop_conf_ge |
drop_conf_be |
drop_conf_be |
drop_conf_le |
drop_conf_le |
drop_trans_ge |
drop_trans_ge |
drop_trans_le |
drop_trans_le |
d_liftable_llstar |
d_liftable_llstar |
drop_conf_lt |
drop_conf_lt |
drop_trans_lt |
drop_trans_lt |
drop_trans_ge_comm |
drop_trans_ge_comm |
drop_conf_div |
drop_conf_div |
drop_fwd_be |
drop_fwd_be |
aaa |
aaa |
aaa_inv_sort_aux |
aaa_inv_sort_aux |
aaa_inv_sort |
aaa_inv_sort |
aaa_inv_lref_aux |
aaa_inv_lref_aux |
aaa_inv_lref |
aaa_inv_lref |
aaa_inv_gref_aux |
aaa_inv_gref_aux |
aaa_inv_gref |
aaa_inv_gref |
aaa_inv_abbr_aux |
aaa_inv_abbr_aux |
aaa_inv_abbr |
aaa_inv_abbr |
aaa_inv_abst_aux |
aaa_inv_abst_aux |
aaa_inv_abst |
aaa_inv_abst |
aaa_inv_appl_aux |
aaa_inv_appl_aux |
aaa_inv_appl |
aaa_inv_appl |
aaa_inv_cast_aux |
aaa_inv_cast_aux |
aaa_inv_cast |
aaa_inv_cast |
aaa_lift |
aaa_lift |
aaa_inv_lift |
aaa_inv_lift |
aaa_mono |
aaa_mono |
lsuba |
lsuba |
lsuba_inv_atom1_aux |
lsuba_inv_atom1_aux |
lsuba_inv_atom1 |
lsuba_inv_atom1 |
lsuba_inv_pair1_aux |
lsuba_inv_pair1_aux |
lsuba_inv_pair1 |
lsuba_inv_pair1 |
lsuba_inv_atom2_aux |
lsuba_inv_atom2_aux |
lsubc_inv_atom2 |
lsubc_inv_atom2 |
lsuba_inv_pair2_aux |
lsuba_inv_pair2_aux |
lsuba_inv_pair2 |
lsuba_inv_pair2 |
lsuba_fwd_lsubr |
lsuba_fwd_lsubr |
lsuba_refl |
lsuba_refl |
lsuba_drop_O1_conf |
lsuba_drop_O1_conf |
lsuba_drop_O1_trans |
lsuba_drop_O1_trans |
lsuba_aaa_conf |
lsuba_aaa_conf |
lsuba_aaa_trans |
lsuba_aaa_trans |
lreq |
lreq |
lreq_pair_lt |
lreq_pair_lt |
lreq_succ_lt |
lreq_succ_lt |
lreq_pair_O_Y |
lreq_pair_O_Y |
lreq_refl |
lreq_refl |
lreq_O2 |
lreq_O2 |
lreq_sym |
lreq_sym |
lreq_inv_atom1_aux |
lreq_inv_atom1_aux |
lreq_inv_atom1 |
lreq_inv_atom1 |
lreq_inv_zero1_aux |
lreq_inv_zero1_aux |
lreq_inv_zero1 |
lreq_inv_zero1 |
lreq_inv_pair1_aux |
lreq_inv_pair1_aux |
lreq_inv_pair1 |
lreq_inv_pair1 |
lreq_inv_pair |
lreq_inv_pair |
lreq_inv_succ1_aux |
lreq_inv_succ1_aux |
lreq_inv_succ1 |
lreq_inv_succ1 |
lreq_inv_atom2 |
lreq_inv_atom2 |
lreq_inv_succ |
lreq_inv_succ |
lreq_inv_zero2 |
lreq_inv_zero2 |
lreq_inv_pair2 |
lreq_inv_pair2 |
lreq_inv_succ2 |
lreq_inv_succ2 |
lreq_fwd_length |
lreq_fwd_length |
lreq_inv_O_Y_aux |
lreq_inv_O_Y_aux |
lreq_inv_O_Y |
lreq_inv_O_Y |
lreq_trans |
lreq_trans |
lreq_canc_sn |
lreq_canc_sn |
lreq_canc_dx |
lreq_canc_dx |
lreq_join |
lreq_join |
dedropable_sn |
dedropable_sn |
lreq_drop_trans_be |
lreq_drop_trans_be |
lreq_drop_conf_be |
lreq_drop_conf_be |
drop_O1_ex |
drop_O1_ex |
dedropable_sn_TC |
dedropable_sn_TC |
drop_O1_inj |
drop_O1_inj |
lpx_sn |
lpx_sn |
lpx_sn_refl |
lpx_sn_refl |
lpx_sn_inv_atom1_aux |
lpx_sn_inv_atom1_aux |
lpx_sn_inv_atom1 |
lpx_sn_inv_atom1 |
lpx_sn_inv_pair1_aux |
lpx_sn_inv_pair1_aux |
lpx_sn_inv_pair1 |
lpx_sn_inv_pair1 |
lpx_sn_inv_atom2_aux |
lpx_sn_inv_atom2_aux |
lpx_sn_inv_atom2 |
lpx_sn_inv_atom2 |
lpx_sn_inv_pair2_aux |
lpx_sn_inv_pair2_aux |
lpx_sn_inv_pair2 |
lpx_sn_inv_pair2 |
lpx_sn_inv_pair |
lpx_sn_inv_pair |
lpx_sn_fwd_length |
lpx_sn_fwd_length |
lpx_sn_drop_conf |
lpx_sn_drop_conf |
lpx_sn_drop_trans |
lpx_sn_drop_trans |
lpx_sn_deliftable_dropable |
lpx_sn_deliftable_dropable |
lpx_sn_liftable_dedropable |
lpx_sn_liftable_dedropable |
lpx_sn_dropable_aux |
lpx_sn_dropable_aux |
lpx_sn_dropable |
lpx_sn_dropable |
fw |
fw |
fw_shift |
fw_shift |
fw_tpair_sn |
fw_tpair_sn |
fw_tpair_dx |
fw_tpair_dx |
fw_lpair_sn |
fw_lpair_sn |
fqu |
fqu |
fqu_drop_lt |
fqu_drop_lt |
fqu_lref_S_lt |
fqu_lref_S_lt |
fqu_fwd_fw |
fqu_fwd_fw |
fqu_fwd_length_lref1_aux |
fqu_fwd_length_lref1_aux |
fqu_fwd_length_lref1 |
fqu_fwd_length_lref1 |
fqu_inv_eq_aux |
fqu_inv_eq_aux |
fqu_inv_eq |
fqu_inv_eq |
fqu_wf_ind |
fqu_wf_ind |
fquq |
fquq |
fquq_refl |
fquq_refl |
fqu_fquq |
fqu_fquq |
fquq_fwd_fw |
fquq_fwd_fw |
fquq_fwd_length_lref1_aux |
fquq_fwd_length_lref1_aux |
fquq_fwd_length_lref1 |
fquq_fwd_length_lref1 |
fquqa |
fquqa |
fquqa_refl |
fquqa_refl |
fquqa_drop |
fquqa_drop |
fquq_fquqa |
fquq_fquqa |
fquqa_inv_fquq |
fquqa_inv_fquq |
fquq_inv_gen |
fquq_inv_gen |
fqup |
fqup |
fqu_fqup |
fqu_fqup |
fqup_strap1 |
fqup_strap1 |
fqup_strap2 |
fqup_strap2 |
fqup_drop |
fqup_drop |
fqup_lref |
fqup_lref |
fqup_pair_sn |
fqup_pair_sn |
fqup_bind_dx |
fqup_bind_dx |
fqup_flat_dx |
fqup_flat_dx |
fqup_flat_dx_pair_sn |
fqup_flat_dx_pair_sn |
fqup_bind_dx_flat_dx |
fqup_bind_dx_flat_dx |
fqup_flat_dx_bind_dx |
fqup_flat_dx_bind_dx |
fqup_ind |
fqup_ind |
fqup_ind_dx |
fqup_ind_dx |
fqup_fwd_fw |
fqup_fwd_fw |
fqup_wf_ind |
fqup_wf_ind |
fqup_wf_ind_eq |
fqup_wf_ind_eq |
fqus |
fqus |
fqus_ind |
fqus_ind |
fqus_ind_dx |
fqus_ind_dx |
fqus_refl |
fqus_refl |
fquq_fqus |
fquq_fqus |
fqus_strap1 |
fqus_strap1 |
fqus_strap2 |
fqus_strap2 |
fqus_drop |
fqus_drop |
fqup_fqus |
fqup_fqus |
fqus_fwd_fw |
fqus_fwd_fw |
fqup_inv_step_sn |
fqup_inv_step_sn |
fqus_inv_gen |
fqus_inv_gen |
fqus_strap1_fqu |
fqus_strap1_fqu |
fqus_strap2_fqu |
fqus_strap2_fqu |
fqus_fqup_trans |
fqus_fqup_trans |
fqup_fqus_trans |
fqup_fqus_trans |
cpx |
cpx |
lsubr_cpx_trans |
lsubr_cpx_trans |
cpx_refl |
cpx_refl |
cpr_cpx |
cpr_cpx |
cpx_pair_sn |
cpx_pair_sn |
cpx_delift |
cpx_delift |
cpx_inv_atom1_aux |
cpx_inv_atom1_aux |
cpx_inv_atom1 |
cpx_inv_atom1 |
cpx_inv_sort1 |
cpx_inv_sort1 |
cpx_inv_lref1 |
cpx_inv_lref1 |
cpx_inv_lref1_ge |
cpx_inv_lref1_ge |
cpx_inv_gref1 |
cpx_inv_gref1 |
cpx_inv_bind1_aux |
cpx_inv_bind1_aux |
cpx_inv_bind1 |
cpx_inv_bind1 |
cpx_inv_abbr1 |
cpx_inv_abbr1 |
cpx_inv_abst1 |
cpx_inv_abst1 |
cpx_inv_flat1_aux |
cpx_inv_flat1_aux |
cpx_inv_flat1 |
cpx_inv_flat1 |
cpx_inv_appl1 |
cpx_inv_appl1 |
cpx_inv_appl1_simple |
cpx_inv_appl1_simple |
cpx_inv_cast1 |
cpx_inv_cast1 |
cpx_fwd_bind1_minus |
cpx_fwd_bind1_minus |
sta_cpx_aux |
sta_cpx_aux |
sta_cpx |
sta_cpx |
cpx_lift |
cpx_lift |
cpx_inv_lift1 |
cpx_inv_lift1 |
fqu_cpx_trans |
fqu_cpx_trans |
fqu_sta_trans |
fqu_sta_trans |
fquq_cpx_trans |
fquq_cpx_trans |
fquq_sta_trans |
fquq_sta_trans |
fqup_cpx_trans |
fqup_cpx_trans |
fqus_cpx_trans |
fqus_cpx_trans |
fqu_cpx_trans_neq |
fqu_cpx_trans_neq |
fquq_cpx_trans_neq |
fquq_cpx_trans_neq |
fqup_cpx_trans_neq |
fqup_cpx_trans_neq |
fqus_cpx_trans_neq |
fqus_cpx_trans_neq |
lpr |
lpr |
lpr_inv_atom1 |
lpr_inv_atom1 |
lpr_inv_pair1 |
lpr_inv_pair1 |
lpr_inv_atom2 |
lpr_inv_atom2 |
lpr_inv_pair2 |
lpr_inv_pair2 |
lpr_refl |
lpr_refl |
lpr_pair |
lpr_pair |
lpr_fwd_length |
lpr_fwd_length |
lpx |
lpx |
lpx_inv_atom1 |
lpx_inv_atom1 |
lpx_inv_pair1 |
lpx_inv_pair1 |
lpx_inv_atom2 |
lpx_inv_atom2 |
lpx_inv_pair2 |
lpx_inv_pair2 |
lpx_inv_pair |
lpx_inv_pair |
lpx_refl |
lpx_refl |
lpx_pair |
lpx_pair |
lpr_lpx |
lpr_lpx |
lpx_fwd_length |
lpx_fwd_length |
lpx_drop_conf |
lpx_drop_conf |
drop_lpx_trans |
drop_lpx_trans |
lpx_drop_trans_O1 |
lpx_drop_trans_O1 |
fqu_lpx_trans |
fqu_lpx_trans |
fquq_lpx_trans |
fquq_lpx_trans |
lpx_fqu_trans |
lpx_fqu_trans |
lpx_fquq_trans |
lpx_fquq_trans |
cpx_lpx_aaa_conf |
cpx_lpx_aaa_conf |
cpx_aaa_conf |
cpx_aaa_conf |
lpx_aaa_conf |
lpx_aaa_conf |
cpr_aaa_conf |
cpr_aaa_conf |
lpr_aaa_conf |
lpr_aaa_conf |
cnx |
cnx |
cnx_inv_sort |
cnx_inv_sort |
cnx_inv_delta |
cnx_inv_delta |
cnx_inv_abst |
cnx_inv_abst |
cnx_inv_abbr |
cnx_inv_abbr |
cnx_inv_zeta |
cnx_inv_zeta |
cnx_inv_appl |
cnx_inv_appl |
cnx_inv_eps |
cnx_inv_eps |
cnx_fwd_cnr |
cnx_fwd_cnr |
cnx_sort |
cnx_sort |
cnx_sort_iter |
cnx_sort_iter |
cnx_lref_free |
cnx_lref_free |
cnx_lref_atom |
cnx_lref_atom |
cnx_abst |
cnx_abst |
cnx_appl_simple |
cnx_appl_simple |
cnx_dec |
cnx_dec |
cpxs |
cpxs |
cpxs_ind |
cpxs_ind |
cpxs_ind_dx |
cpxs_ind_dx |
cpxs_refl |
cpxs_refl |
cpx_cpxs |
cpx_cpxs |
cpxs_strap1 |
cpxs_strap1 |
cpxs_strap2 |
cpxs_strap2 |
lsubr_cpxs_trans |
lsubr_cpxs_trans |
cprs_cpxs |
cprs_cpxs |
cpxs_sort |
cpxs_sort |
cpxs_bind_dx |
cpxs_bind_dx |
cpxs_flat_dx |
cpxs_flat_dx |
cpxs_flat_sn |
cpxs_flat_sn |
cpxs_pair_sn |
cpxs_pair_sn |
cpxs_zeta |
cpxs_zeta |
cpxs_eps |
cpxs_eps |
cpxs_ct |
cpxs_ct |
cpxs_beta_dx |
cpxs_beta_dx |
cpxs_theta_dx |
cpxs_theta_dx |
cpxs_inv_sort1 |
cpxs_inv_sort1 |
cpxs_inv_cast1 |
cpxs_inv_cast1 |
cpxs_inv_cnx1 |
cpxs_inv_cnx1 |
cpxs_neq_inv_step_sn |
cpxs_neq_inv_step_sn |
cpxs_aaa_conf |
cpxs_aaa_conf |
cprs_aaa_conf |
cprs_aaa_conf |
lpx_sn_confluent |
lpx_sn_confluent |
lpx_sn_transitive |
lpx_sn_transitive |
lpx_sn_trans |
lpx_sn_trans |
lpx_sn_conf |
lpx_sn_conf |
cpr_lift |
cpr_lift |
cpr_inv_lift1 |
cpr_inv_lift1 |
lpr_drop_conf |
lpr_drop_conf |
drop_lpr_trans |
drop_lpr_trans |
lpr_drop_trans_O1 |
lpr_drop_trans_O1 |
fqu_cpr_trans_dx |
fqu_cpr_trans_dx |
fquq_cpr_trans_dx |
fquq_cpr_trans_dx |
fqu_cpr_trans_sn |
fqu_cpr_trans_sn |
fquq_cpr_trans_sn |
fquq_cpr_trans_sn |
fqu_lpr_trans |
fqu_lpr_trans |
fquq_lpr_trans |
fquq_lpr_trans |
cpr_conf_lpr_atom_atom |
cpr_conf_lpr_atom_atom |
cpr_conf_lpr_atom_delta |
cpr_conf_lpr_atom_delta |
cpr_conf_lpr_delta_delta |
cpr_conf_lpr_delta_delta |
cpr_conf_lpr_bind_bind |
cpr_conf_lpr_bind_bind |
cpr_conf_lpr_bind_zeta |
cpr_conf_lpr_bind_zeta |
cpr_conf_lpr_zeta_zeta |
cpr_conf_lpr_zeta_zeta |
cpr_conf_lpr_flat_flat |
cpr_conf_lpr_flat_flat |
cpr_conf_lpr_flat_eps |
cpr_conf_lpr_flat_eps |
cpr_conf_lpr_eps_eps |
cpr_conf_lpr_eps_eps |
cpr_conf_lpr_flat_beta |
cpr_conf_lpr_flat_beta |
cpr_conf_lpr_flat_theta |
cpr_conf_lpr_flat_theta |
cpr_conf_lpr_beta_beta |
cpr_conf_lpr_beta_beta |
cpr_conf_lpr_theta_theta |
cpr_conf_lpr_theta_theta |
cpr_conf_lpr |
cpr_conf_lpr |
cpr_conf |
cpr_conf |
lpr_cpr_conf_dx |
lpr_cpr_conf_dx |
lpr_cpr_conf_sn |
lpr_cpr_conf_sn |
lpr_conf |
lpr_conf |
cprs_delta |
cprs_delta |
cprs_inv_lref1 |
cprs_inv_lref1 |
cprs_lift |
cprs_lift |
cprs_inv_lift1 |
cprs_inv_lift1 |
cprs_trans |
cprs_trans |
cprs_conf |
cprs_conf |
cprs_bind |
cprs_bind |
cprs_flat |
cprs_flat |
cprs_beta_rc |
cprs_beta_rc |
cprs_beta |
cprs_beta |
cprs_theta_rc |
cprs_theta_rc |
cprs_theta |
cprs_theta |
cprs_inv_appl1 |
cprs_inv_appl1 |
lpr_cpr_trans |
lpr_cpr_trans |
cpr_bind2 |
cpr_bind2 |
lpr_cprs_trans |
lpr_cprs_trans |
cprs_strip |
cprs_strip |
cprs_lpr_conf_dx |
cprs_lpr_conf_dx |
cprs_lpr_conf_sn |
cprs_lpr_conf_sn |
cprs_bind2_dx |
cprs_bind2_dx |
TC_lpx_sn_pair_refl |
TC_lpx_sn_pair_refl |
TC_lpx_sn_pair |
TC_lpx_sn_pair |
lpx_sn_LTC_TC_lpx_sn |
lpx_sn_LTC_TC_lpx_sn |
TC_lpx_sn_inv_atom2 |
TC_lpx_sn_inv_atom2 |
TC_lpx_sn_inv_pair2 |
TC_lpx_sn_inv_pair2 |
TC_lpx_sn_ind |
TC_lpx_sn_ind |
TC_lpx_sn_inv_atom1 |
TC_lpx_sn_inv_atom1 |
TC_lpx_sn_inv_pair1_aux |
TC_lpx_sn_inv_pair1_aux |
TC_lpx_sn_inv_pair1 |
TC_lpx_sn_inv_pair1 |
TC_lpx_sn_inv_lpx_sn_LTC |
TC_lpx_sn_inv_lpx_sn_LTC |
TC_lpx_sn_fwd_length |
TC_lpx_sn_fwd_length |
lprs |
lprs |
lprs_ind |
lprs_ind |
lprs_ind_dx |
lprs_ind_dx |
lpr_lprs |
lpr_lprs |
lprs_refl |
lprs_refl |
lprs_strap1 |
lprs_strap1 |
lprs_strap2 |
lprs_strap2 |
lprs_pair_refl |
lprs_pair_refl |
lprs_inv_atom1 |
lprs_inv_atom1 |
lprs_inv_atom2 |
lprs_inv_atom2 |
lprs_fwd_length |
lprs_fwd_length |
lprs_pair |
lprs_pair |
lprs_inv_pair1 |
lprs_inv_pair1 |
lprs_inv_pair2 |
lprs_inv_pair2 |
lprs_ind_alt |
lprs_ind_alt |
lprs_cpr_trans |
lprs_cpr_trans |
lprs_cprs_trans |
lprs_cprs_trans |
lprs_cprs_conf_dx |
lprs_cprs_conf_dx |
lprs_cpr_conf_dx |
lprs_cpr_conf_dx |
lprs_cprs_conf_sn |
lprs_cprs_conf_sn |
lprs_cpr_conf_sn |
lprs_cpr_conf_sn |
cprs_bind2 |
cprs_bind2 |
cprs_inv_abst1 |
cprs_inv_abst1 |
cprs_inv_abst |
cprs_inv_abst |
cprs_inv_abbr1 |
cprs_inv_abbr1 |
lprs_pair2 |
lprs_pair2 |
cpc |
cpc |
cpc_refl |
cpc_refl |
cpc_sym |
cpc_sym |
cpc_fwd_cpr |
cpc_fwd_cpr |
cpc_conf |
cpc_conf |
cpcs |
cpcs |
cpcs_ind |
cpcs_ind |
cpcs_ind_dx |
cpcs_ind_dx |
cpcs_refl |
cpcs_refl |
cpcs_sym |
cpcs_sym |
cpc_cpcs |
cpc_cpcs |
cpcs_strap1 |
cpcs_strap1 |
cpcs_strap2 |
cpcs_strap2 |
cpr_cpcs_dx |
cpr_cpcs_dx |
cpr_cpcs_sn |
cpr_cpcs_sn |
cpcs_cpr_strap1 |
cpcs_cpr_strap1 |
cpcs_cpr_strap2 |
cpcs_cpr_strap2 |
cpcs_cpr_div |
cpcs_cpr_div |
cpr_div |
cpr_div |
cpcs_cpr_conf |
cpcs_cpr_conf |
cpcs_cprs_dx |
cpcs_cprs_dx |
cpcs_cprs_sn |
cpcs_cprs_sn |
cpcs_cprs_strap1 |
cpcs_cprs_strap1 |
cpcs_cprs_strap2 |
cpcs_cprs_strap2 |
cpcs_cprs_div |
cpcs_cprs_div |
cpcs_cprs_conf |
cpcs_cprs_conf |
cprs_div |
cprs_div |
cprs_cpr_div |
cprs_cpr_div |
cpr_cprs_div |
cpr_cprs_div |
cpcs_inv_cprs |
cpcs_inv_cprs |
cpcs_inv_sort |
cpcs_inv_sort |
cpcs_inv_abst1 |
cpcs_inv_abst1 |
cpcs_inv_abst2 |
cpcs_inv_abst2 |
cpcs_inv_sort_abst |
cpcs_inv_sort_abst |
cpcs_inv_lift |
cpcs_inv_lift |
lpr_cpcs_trans |
lpr_cpcs_trans |
lprs_cpcs_trans |
lprs_cpcs_trans |
cpr_cprs_conf_cpcs |
cpr_cprs_conf_cpcs |
cprs_cpr_conf_cpcs |
cprs_cpr_conf_cpcs |
cprs_conf_cpcs |
cprs_conf_cpcs |
lprs_cprs_conf |
lprs_cprs_conf |
lpr_cprs_conf |
lpr_cprs_conf |
lpr_cpr_conf |
lpr_cpr_conf |
cpcs_flat |
cpcs_flat |
cpcs_flat_dx_cpr_rev |
cpcs_flat_dx_cpr_rev |
cpcs_bind_dx |
cpcs_bind_dx |
cpcs_bind_sn |
cpcs_bind_sn |
lsubr_cpcs_trans |
lsubr_cpcs_trans |
cpcs_lift |
cpcs_lift |
cpcs_strip |
cpcs_strip |
cpcs_inv_abst_sn |
cpcs_inv_abst_sn |
cpcs_inv_abst_dx |
cpcs_inv_abst_dx |
cpcs_trans |
cpcs_trans |
cpcs_canc_sn |
cpcs_canc_sn |
cpcs_canc_dx |
cpcs_canc_dx |
cpcs_bind1 |
cpcs_bind1 |
cpcs_bind2 |
cpcs_bind2 |
lpr_cpcs_conf |
lpr_cpcs_conf |
cpcs_aaa_mono |
cpcs_aaa_mono |
da_lift |
da_lift |
da_inv_lift |
da_inv_lift |
da_mono |
da_mono |
lstas_lift |
lstas_lift |
lstas_inv_lift1 |
lstas_inv_lift1 |
lstas_split_aux |
lstas_split_aux |
lstas_split |
lstas_split |
lstas_lstas |
lstas_lstas |
lstas_trans |
lstas_trans |
lstas_mono |
lstas_mono |
lstas_correct |
lstas_correct |
lstas_conf_le |
lstas_conf_le |
lstas_conf |
lstas_conf |
da_lstas |
da_lstas |
lstas_da_conf |
lstas_da_conf |
lstas_inv_da |
lstas_inv_da |
lstas_inv_da_ge |
lstas_inv_da_ge |
lstas_inv_refl_pos |
lstas_inv_refl_pos |
fqus_trans |
fqus_trans |
cpxs_delta |
cpxs_delta |
lstas_cpxs |
lstas_cpxs |
cpxs_inv_lref1 |
cpxs_inv_lref1 |
cpxs_lift |
cpxs_lift |
cpxs_inv_lift1 |
cpxs_inv_lift1 |
fqu_cpxs_trans |
fqu_cpxs_trans |
fquq_cpxs_trans |
fquq_cpxs_trans |
fquq_lstas_trans |
fquq_lstas_trans |
fqup_cpxs_trans |
fqup_cpxs_trans |
fqus_cpxs_trans |
fqus_cpxs_trans |
fqus_lstas_trans |
fqus_lstas_trans |
cpxs_trans |
cpxs_trans |
cpxs_bind |
cpxs_bind |
cpxs_flat |
cpxs_flat |
cpxs_beta_rc |
cpxs_beta_rc |
cpxs_beta |
cpxs_beta |
cpxs_theta_rc |
cpxs_theta_rc |
cpxs_theta |
cpxs_theta |
cpxs_inv_appl1 |
cpxs_inv_appl1 |
lpx_cpx_trans |
lpx_cpx_trans |
cpx_bind2 |
cpx_bind2 |
lpx_cpxs_trans |
lpx_cpxs_trans |
cpxs_bind2_dx |
cpxs_bind2_dx |
fqu_cpxs_trans_neq |
fqu_cpxs_trans_neq |
fquq_cpxs_trans_neq |
fquq_cpxs_trans_neq |
fqup_cpxs_trans_neq |
fqup_cpxs_trans_neq |
fqus_cpxs_trans_neq |
fqus_cpxs_trans_neq |
scpds_strap2 |
scpds_strap2 |
scpds_cprs_trans |
scpds_cprs_trans |
lstas_scpds_trans |
lstas_scpds_trans |
scpds_inv_abst1 |
scpds_inv_abst1 |
scpds_inv_abbr_abst |
scpds_inv_abbr_abst |
scpds_inv_lstas_eq |
scpds_inv_lstas_eq |
scpds_fwd_cpxs |
scpds_fwd_cpxs |
scpds_conf_eq |
scpds_conf_eq |
scpes_inv_lstas_eq |
scpes_inv_lstas_eq |
cpcs_scpes |
cpcs_scpes |
scpes_inv_abst2 |
scpes_inv_abst2 |
scpes_refl |
scpes_refl |
lstas_scpes_trans |
lstas_scpes_trans |
cprs_scpds_div |
cprs_scpds_div |
scpes_trans |
scpes_trans |
scpes_canc_sn |
scpes_canc_sn |
scpes_canc_dx |
scpes_canc_dx |
aaa_lstas |
aaa_lstas |
lstas_aaa_conf |
lstas_aaa_conf |
scpds_aaa_conf |
scpds_aaa_conf |
scpes_aaa_mono |
scpes_aaa_mono |
lsubr_inv_pair1_aux |
lsubr_inv_pair1_aux |
lsubr_inv_pair1 |
lsubr_inv_pair1 |
lsubr_trans |
lsubr_trans |
applv |
applv |
applv_simple |
applv_simple |
at |
at |
at_inv_nil_aux |
at_inv_nil_aux |
at_inv_nil |
at_inv_nil |
at_inv_cons_aux |
at_inv_cons_aux |
at_inv_cons |
at_inv_cons |
at_inv_cons_lt |
at_inv_cons_lt |
at_inv_cons_ge |
at_inv_cons_ge |
minuss |
minuss |
minuss_inv_nil1_aux |
minuss_inv_nil1_aux |
minuss_inv_nil1 |
minuss_inv_nil1 |
minuss_inv_cons1_aux |
minuss_inv_cons1_aux |
minuss_inv_cons1 |
minuss_inv_cons1 |
minuss_inv_cons1_ge |
minuss_inv_cons1_ge |
minuss_inv_cons1_lt |
minuss_inv_cons1_lt |
liftv |
liftv |
liftv_inv_nil1_aux |
liftv_inv_nil1_aux |
liftv_inv_nil1 |
liftv_inv_nil1 |
liftv_inv_cons1_aux |
liftv_inv_cons1_aux |
liftv_inv_cons1 |
liftv_inv_cons1 |
liftv_total |
liftv_total |
pluss |
pluss |
pluss_inv_nil2 |
pluss_inv_nil2 |
pluss_inv_cons2 |
pluss_inv_cons2 |
lifts |
lifts |
lifts_inv_nil_aux |
lifts_inv_nil_aux |
lifts_inv_nil |
lifts_inv_nil |
lifts_inv_cons_aux |
lifts_inv_cons_aux |
lifts_inv_cons |
lifts_inv_cons |
lifts_inv_sort1 |
lifts_inv_sort1 |
lifts_inv_lref1 |
lifts_inv_lref1 |
lifts_inv_gref1 |
lifts_inv_gref1 |
lifts_inv_bind1 |
lifts_inv_bind1 |
lifts_inv_flat1 |
lifts_inv_flat1 |
lifts_simple_dx |
lifts_simple_dx |
lifts_simple_sn |
lifts_simple_sn |
lifts_bind |
lifts_bind |
lifts_flat |
lifts_flat |
lifts_total |
lifts_total |
liftsv |
liftsv |
lifts_inv_applv1 |
lifts_inv_applv1 |
lifts_applv |
lifts_applv |
drops |
drops |
d_liftable1 |
d_liftable1 |
d_liftables1 |
d_liftables1 |
d_liftables1_all |
d_liftables1_all |
drops_inv_nil_aux |
drops_inv_nil_aux |
drops_inv_nil |
drops_inv_nil |
drops_inv_cons_aux |
drops_inv_cons_aux |
drops_inv_cons |
drops_inv_cons |
drops_inv_skip2 |
drops_inv_skip2 |
drops_skip |
drops_skip |
d1_liftable_liftables |
d1_liftable_liftables |
d1_liftables_liftables_all |
d1_liftables_liftables_all |
aaa_lifts |
aaa_lifts |
aaa_fqu_conf |
aaa_fqu_conf |
aaa_fquq_conf |
aaa_fquq_conf |
aaa_fqup_conf |
aaa_fqup_conf |
aaa_fqus_conf |
aaa_fqus_conf |
lsubd |
lsubd |
lsubd_fwd_lsubr |
lsubd_fwd_lsubr |
lsubd_inv_atom1_aux |
lsubd_inv_atom1_aux |
lsubd_inv_atom1 |
lsubd_inv_atom1 |
lsubd_inv_pair1_aux |
lsubd_inv_pair1_aux |
lsubd_inv_pair1 |
lsubd_inv_pair1 |
lsubd_inv_atom2_aux |
lsubd_inv_atom2_aux |
lsubd_inv_atom2 |
lsubd_inv_atom2 |
lsubd_inv_pair2_aux |
lsubd_inv_pair2_aux |
lsubd_inv_pair2 |
lsubd_inv_pair2 |
lsubd_refl |
lsubd_refl |
lsubd_drop_O1_conf |
lsubd_drop_O1_conf |
lsubd_drop_O1_trans |
lsubd_drop_O1_trans |
lsubd_da_trans |
lsubd_da_trans |
lsubd_da_conf |
lsubd_da_conf |
lsubd_trans |
lsubd_trans |
aaa_da |
aaa_da |
llpx_sn |
llpx_sn |
llpx_sn_inv_bind_aux |
llpx_sn_inv_bind_aux |
llpx_sn_inv_bind |
llpx_sn_inv_bind |
llpx_sn_inv_flat_aux |
llpx_sn_inv_flat_aux |
llpx_sn_inv_flat |
llpx_sn_inv_flat |
llpx_sn_fwd_length |
llpx_sn_fwd_length |
llpx_sn_fwd_drop_sn |
llpx_sn_fwd_drop_sn |
llpx_sn_fwd_drop_dx |
llpx_sn_fwd_drop_dx |
llpx_sn_fwd_lref_aux |
llpx_sn_fwd_lref_aux |
llpx_sn_fwd_lref |
llpx_sn_fwd_lref |
llpx_sn_fwd_bind_sn |
llpx_sn_fwd_bind_sn |
llpx_sn_fwd_bind_dx |
llpx_sn_fwd_bind_dx |
llpx_sn_fwd_flat_sn |
llpx_sn_fwd_flat_sn |
llpx_sn_fwd_flat_dx |
llpx_sn_fwd_flat_dx |
llpx_sn_fwd_pair_sn |
llpx_sn_fwd_pair_sn |
llpx_sn_refl |
llpx_sn_refl |
llpx_sn_Y |
llpx_sn_Y |
llpx_sn_ge_up |
llpx_sn_ge_up |
llpx_sn_ge |
llpx_sn_ge |
llpx_sn_bind_O |
llpx_sn_bind_O |
llpx_sn_co |
llpx_sn_co |
lreq_llpx_sn_trans |
lreq_llpx_sn_trans |
llpx_sn_lreq_trans |
llpx_sn_lreq_trans |
llpx_sn_lreq_repl |
llpx_sn_lreq_repl |
llpx_sn_bind_repl_SO |
llpx_sn_bind_repl_SO |
llpx_sn_fwd_lref_dx |
llpx_sn_fwd_lref_dx |
llpx_sn_fwd_lref_sn |
llpx_sn_fwd_lref_sn |
llpx_sn_inv_lref_ge_dx |
llpx_sn_inv_lref_ge_dx |
llpx_sn_inv_lref_ge_sn |
llpx_sn_inv_lref_ge_sn |
llpx_sn_inv_lref_ge_bi |
llpx_sn_inv_lref_ge_bi |
llpx_sn_inv_S_aux |
llpx_sn_inv_S_aux |
llpx_sn_inv_S |
llpx_sn_inv_S |
llpx_sn_inv_bind_O |
llpx_sn_inv_bind_O |
llpx_sn_fwd_bind_O_dx |
llpx_sn_fwd_bind_O_dx |
llpx_sn_bind_repl_O |
llpx_sn_bind_repl_O |
llpx_sn_dec |
llpx_sn_dec |
llpx_sn_lift_le |
llpx_sn_lift_le |
llpx_sn_lift_ge |
llpx_sn_lift_ge |
llpx_sn_inv_lift_le |
llpx_sn_inv_lift_le |
llpx_sn_inv_lift_be |
llpx_sn_inv_lift_be |
llpx_sn_inv_lift_ge |
llpx_sn_inv_lift_ge |
llpx_sn_inv_lift_O |
llpx_sn_inv_lift_O |
llpx_sn_drop_conf_O |
llpx_sn_drop_conf_O |
llpx_sn_drop_trans_O |
llpx_sn_drop_trans_O |
nllpx_sn_inv_bind |
nllpx_sn_inv_bind |
nllpx_sn_inv_flat |
nllpx_sn_inv_flat |
nllpx_sn_inv_bind_O |
nllpx_sn_inv_bind_O |
ceq |
ceq |
lleq |
lleq |
lleq_transitive |
lleq_transitive |
lleq_ind |
lleq_ind |
lleq_inv_bind |
lleq_inv_bind |
lleq_inv_flat |
lleq_inv_flat |
lleq_fwd_length |
lleq_fwd_length |
lleq_fwd_lref |
lleq_fwd_lref |
lleq_fwd_drop_sn |
lleq_fwd_drop_sn |
lleq_fwd_drop_dx |
lleq_fwd_drop_dx |
lleq_fwd_bind_sn |
lleq_fwd_bind_sn |
lleq_fwd_bind_dx |
lleq_fwd_bind_dx |
lleq_fwd_flat_sn |
lleq_fwd_flat_sn |
lleq_fwd_flat_dx |
lleq_fwd_flat_dx |
lleq_sort |
lleq_sort |
lleq_skip |
lleq_skip |
lleq_lref |
lleq_lref |
lleq_free |
lleq_free |
lleq_gref |
lleq_gref |
lleq_bind |
lleq_bind |
lleq_flat |
lleq_flat |
lleq_refl |
lleq_refl |
lleq_Y |
lleq_Y |
lleq_sym |
lleq_sym |
lleq_ge_up |
lleq_ge_up |
lleq_ge |
lleq_ge |
lleq_bind_O |
lleq_bind_O |
llpx_sn_lrefl |
llpx_sn_lrefl |
lleq_bind_repl_O |
lleq_bind_repl_O |
lleq_dec |
lleq_dec |
lleq_llpx_sn_trans |
lleq_llpx_sn_trans |
lleq_llpx_sn_conf |
lleq_llpx_sn_conf |
lleq_inv_lref_ge_dx |
lleq_inv_lref_ge_dx |
lleq_inv_lref_ge_sn |
lleq_inv_lref_ge_sn |
lleq_inv_lref_ge_bi |
lleq_inv_lref_ge_bi |
lleq_inv_lref_ge |
lleq_inv_lref_ge |
lleq_inv_S |
lleq_inv_S |
lleq_inv_bind_O |
lleq_inv_bind_O |
lleq_fwd_lref_dx |
lleq_fwd_lref_dx |
lleq_fwd_lref_sn |
lleq_fwd_lref_sn |
lleq_fwd_bind_O_dx |
lleq_fwd_bind_O_dx |
lleq_lift_le |
lleq_lift_le |
lleq_lift_ge |
lleq_lift_ge |
lleq_inv_lift_le |
lleq_inv_lift_le |
lleq_inv_lift_be |
lleq_inv_lift_be |
lleq_inv_lift_ge |
lleq_inv_lift_ge |
nlleq_inv_bind |
nlleq_inv_bind |
nlleq_inv_flat |
nlleq_inv_flat |
nlleq_inv_bind_O |
nlleq_inv_bind_O |
lleq_aaa_trans |
lleq_aaa_trans |
aaa_lleq_conf |
aaa_lleq_conf |
lsuba_trans |
lsuba_trans |
ri2 |
ri2 |
ib2 |
ib2 |
crr |
crr |
crr_inv_sort_aux |
crr_inv_sort_aux |
crr_inv_sort |
crr_inv_sort |
crr_inv_lref_aux |
crr_inv_lref_aux |
crr_inv_lref |
crr_inv_lref |
crr_inv_gref_aux |
crr_inv_gref_aux |
crr_inv_gref |
crr_inv_gref |
trr_inv_atom |
trr_inv_atom |
crr_inv_ib2_aux |
crr_inv_ib2_aux |
crr_inv_ib2 |
crr_inv_ib2 |
crr_inv_appl_aux |
crr_inv_appl_aux |
crr_inv_appl |
crr_inv_appl |
cir |
cir |
cir_inv_delta |
cir_inv_delta |
cir_inv_ri2 |
cir_inv_ri2 |
cir_inv_ib2 |
cir_inv_ib2 |
cir_inv_bind |
cir_inv_bind |
cir_inv_appl |
cir_inv_appl |
cir_inv_flat |
cir_inv_flat |
cir_sort |
cir_sort |
cir_gref |
cir_gref |
tir_atom |
tir_atom |
cir_ib2 |
cir_ib2 |
cir_appl |
cir_appl |
crx |
crx |
crr_crx |
crr_crx |
crx_inv_sort_aux |
crx_inv_sort_aux |
crx_inv_sort |
crx_inv_sort |
crx_inv_lref_aux |
crx_inv_lref_aux |
crx_inv_lref |
crx_inv_lref |
crx_inv_gref_aux |
crx_inv_gref_aux |
crx_inv_gref |
crx_inv_gref |
trx_inv_atom |
trx_inv_atom |
crx_inv_ib2_aux |
crx_inv_ib2_aux |
crx_inv_ib2 |
crx_inv_ib2 |
crx_inv_appl_aux |
crx_inv_appl_aux |
crx_inv_appl |
crx_inv_appl |
cix |
cix |
cix_inv_sort |
cix_inv_sort |
cix_inv_delta |
cix_inv_delta |
cix_inv_ri2 |
cix_inv_ri2 |
cix_inv_ib2 |
cix_inv_ib2 |
cix_inv_bind |
cix_inv_bind |
cix_inv_appl |
cix_inv_appl |
cix_inv_flat |
cix_inv_flat |
cix_inv_cir |
cix_inv_cir |
cix_sort |
cix_sort |
tix_lref |
tix_lref |
cix_gref |
cix_gref |
cix_ib2 |
cix_ib2 |
cix_appl |
cix_appl |
cpx_fwd_cix |
cpx_fwd_cix |
nlift_lref_be_SO |
nlift_lref_be_SO |
nlift_bind_sn |
nlift_bind_sn |
nlift_bind_dx |
nlift_bind_dx |
nlift_flat_sn |
nlift_flat_sn |
nlift_flat_dx |
nlift_flat_dx |
nlift_inv_lref_be_SO |
nlift_inv_lref_be_SO |
nlift_inv_bind |
nlift_inv_bind |
nlift_inv_flat |
nlift_inv_flat |
frees |
frees |
frees_trans |
frees_trans |
frees_inv |
frees_inv |
frees_inv_sort |
frees_inv_sort |
frees_inv_gref |
frees_inv_gref |
frees_inv_lref |
frees_inv_lref |
frees_inv_lref_free |
frees_inv_lref_free |
frees_inv_lref_skip |
frees_inv_lref_skip |
frees_inv_lref_ge |
frees_inv_lref_ge |
frees_inv_lref_lt |
frees_inv_lref_lt |
frees_inv_bind |
frees_inv_bind |
frees_inv_flat |
frees_inv_flat |
frees_lref_eq |
frees_lref_eq |
frees_lref_be |
frees_lref_be |
frees_bind_sn |
frees_bind_sn |
frees_bind_dx |
frees_bind_dx |
frees_flat_sn |
frees_flat_sn |
frees_flat_dx |
frees_flat_dx |
frees_weak |
frees_weak |
frees_inv_bind_O |
frees_inv_bind_O |
frees_dec |
frees_dec |
frees_S |
frees_S |
frees_bind_dx_O |
frees_bind_dx_O |
frees_lift_ge |
frees_lift_ge |
frees_inv_lift_be |
frees_inv_lift_be |
frees_inv_lift_ge |
frees_inv_lift_ge |
append |
append |
d_appendable_sn |
d_appendable_sn |
append_atom_sn |
append_atom_sn |
append_assoc |
append_assoc |
append_length |
append_length |
ltail_length |
ltail_length |
lpair_ltail |
lpair_ltail |
append_inj_sn |
append_inj_sn |
append_inj_dx |
append_inj_dx |
append_inv_refl_dx |
append_inv_refl_dx |
append_inv_pair_dx |
append_inv_pair_dx |
length_inv_pos_dx_ltail |
length_inv_pos_dx_ltail |
length_inv_pos_sn_ltail |
length_inv_pos_sn_ltail |
lenv_ind_alt |
lenv_ind_alt |
drop_O1_append_sn_le_aux |
drop_O1_append_sn_le_aux |
drop_O1_append_sn_le |
drop_O1_append_sn_le |
drop_O1_inv_append1_ge |
drop_O1_inv_append1_ge |
drop_O1_inv_append1_le |
drop_O1_inv_append1_le |
frees_append |
frees_append |
frees_inv_append_aux |
frees_inv_append_aux |
frees_inv_append |
frees_inv_append |
llor |
llor |
llor_atom |
llor_atom |
llor_tail_frees |
llor_tail_frees |
llor_tail_cofrees |
llor_tail_cofrees |
llor_skip |
llor_skip |
llor_total |
llor_total |
lpx_sn_alt |
lpx_sn_alt |
lpx_sn_alt_fwd_length |
lpx_sn_alt_fwd_length |
lpx_sn_alt_inv_atom1 |
lpx_sn_alt_inv_atom1 |
lpx_sn_alt_inv_pair1 |
lpx_sn_alt_inv_pair1 |
lpx_sn_alt_inv_atom2 |
lpx_sn_alt_inv_atom2 |
lpx_sn_alt_inv_pair2 |
lpx_sn_alt_inv_pair2 |
lpx_sn_alt_atom |
lpx_sn_alt_atom |
lpx_sn_alt_pair |
lpx_sn_alt_pair |
lpx_sn_lpx_sn_alt |
lpx_sn_lpx_sn_alt |
lpx_sn_alt_inv_lpx_sn |
lpx_sn_alt_inv_lpx_sn |
lpx_sn_intro_alt |
lpx_sn_intro_alt |
lpx_sn_inv_alt |
lpx_sn_inv_alt |
llpx_sn_alt_r |
llpx_sn_alt_r |
llpx_sn_alt_r_intro_alt |
llpx_sn_alt_r_intro_alt |
llpx_sn_alt_r_ind_alt |
llpx_sn_alt_r_ind_alt |
llpx_sn_alt_r_inv_alt |
llpx_sn_alt_r_inv_alt |
llpx_sn_alt_r_inv_flat |
llpx_sn_alt_r_inv_flat |
llpx_sn_alt_r_inv_bind |
llpx_sn_alt_r_inv_bind |
llpx_sn_alt_r_fwd_length |
llpx_sn_alt_r_fwd_length |
llpx_sn_alt_r_fwd_lref |
llpx_sn_alt_r_fwd_lref |
llpx_sn_alt_r_sort |
llpx_sn_alt_r_sort |
llpx_sn_alt_r_gref |
llpx_sn_alt_r_gref |
llpx_sn_alt_r_skip |
llpx_sn_alt_r_skip |
llpx_sn_alt_r_free |
llpx_sn_alt_r_free |
llpx_sn_alt_r_lref |
llpx_sn_alt_r_lref |
llpx_sn_alt_r_flat |
llpx_sn_alt_r_flat |
llpx_sn_alt_r_bind |
llpx_sn_alt_r_bind |
llpx_sn_lpx_sn_alt_r |
llpx_sn_lpx_sn_alt_r |
llpx_sn_alt_r_inv_lpx_sn |
llpx_sn_alt_r_inv_lpx_sn |
llpx_sn_intro_alt_r |
llpx_sn_intro_alt_r |
llpx_sn_ind_alt_r |
llpx_sn_ind_alt_r |
llpx_sn_inv_alt_r |
llpx_sn_inv_alt_r |
llpx_sn_alt |
llpx_sn_alt |
llpx_sn_llpx_sn_alt |
llpx_sn_llpx_sn_alt |
llpx_sn_alt_inv_llpx_sn |
llpx_sn_alt_inv_llpx_sn |
lleq_intro_alt |
lleq_intro_alt |
lleq_inv_alt |
lleq_inv_alt |
llpx_sn_llor_fwd_sn |
llpx_sn_llor_fwd_sn |
lpx_sn_llpx_sn |
lpx_sn_llpx_sn |
lreq_lleq_trans |
lreq_lleq_trans |
lleq_lreq_trans |
lleq_lreq_trans |
lleq_lreq_repl |
lleq_lreq_repl |
lleq_bind_repl_SO |
lleq_bind_repl_SO |
llpx_sn_frees_trans_aux |
llpx_sn_frees_trans_aux |
llpx_sn_frees_trans |
llpx_sn_frees_trans |
llpx_sn_llor_dx |
llpx_sn_llor_dx |
llpx_sn_llor_dx_sym |
llpx_sn_llor_dx_sym |
lreq_cpx_trans |
lreq_cpx_trans |
cpx_llpx_sn_conf |
cpx_llpx_sn_conf |
lleq_cpx_trans |
lleq_cpx_trans |
cpx_lleq_conf |
cpx_lleq_conf |
cpx_lleq_conf_sn |
cpx_lleq_conf_sn |
cpx_lleq_conf_dx |
cpx_lleq_conf_dx |
lreq_frees_trans |
lreq_frees_trans |
frees_lreq_conf |
frees_lreq_conf |
lpx_cpx_frees_trans |
lpx_cpx_frees_trans |
cpx_frees_trans |
cpx_frees_trans |
lpx_frees_trans |
lpx_frees_trans |
lleq_lpx_trans |
lleq_lpx_trans |
lpx_lleq_fqu_trans |
lpx_lleq_fqu_trans |
lpx_lleq_fquq_trans |
lpx_lleq_fquq_trans |
lpx_lleq_fqup_trans |
lpx_lleq_fqup_trans |
lpx_lleq_fqus_trans |
lpx_lleq_fqus_trans |
lreq_lpx_trans_lleq_aux |
lreq_lpx_trans_lleq_aux |
lreq_lpx_trans_lleq |
lreq_lpx_trans_lleq |
cnx_inv_crx |
cnx_inv_crx |
fleq |
fleq |
fleq_refl |
fleq_refl |
fleq_sym |
fleq_sym |
fleq_inv_gen |
fleq_inv_gen |
lleq_fqu_trans |
lleq_fqu_trans |
lleq_fquq_trans |
lleq_fquq_trans |
lleq_fqup_trans |
lleq_fqup_trans |
lleq_fqus_trans |
lleq_fqus_trans |
lleq_trans |
lleq_trans |
lleq_canc_sn |
lleq_canc_sn |
lleq_canc_dx |
lleq_canc_dx |
lleq_nlleq_trans |
lleq_nlleq_trans |
nlleq_lleq_div |
nlleq_lleq_div |
fpb |
fpb |
cpr_fpb |
cpr_fpb |
lpr_fpb |
lpr_fpb |
lleq_fpb_trans |
lleq_fpb_trans |
fleq_fpb_trans |
fleq_fpb_trans |
fpb_inv_fleq |
fpb_inv_fleq |
fpbq |
fpbq |
fpbq_refl |
fpbq_refl |
cpr_fpbq |
cpr_fpbq |
lpr_fpbq |
lpr_fpbq |
fpbqa |
fpbqa |
fleq_fpbq |
fleq_fpbq |
fpb_fpbq |
fpb_fpbq |
fpbq_fpbqa |
fpbq_fpbqa |
fpbqa_inv_fpbq |
fpbqa_inv_fpbq |
fpbq_ind_alt |
fpbq_ind_alt |
fpb_fpbq_alt |
fpb_fpbq_alt |
fpbq_inv_fpb_alt |
fpbq_inv_fpb_alt |
fpbq_aaa_conf |
fpbq_aaa_conf |
cpr_fwd_cir |
cpr_fwd_cir |
sta_fpb |
sta_fpb |
crr_lift |
crr_lift |
crr_inv_lift |
crr_inv_lift |
cir_lift |
cir_lift |
cir_inv_lift |
cir_inv_lift |
cpr_llpx_sn_conf |
cpr_llpx_sn_conf |
crx_lift |
crx_lift |
crx_inv_lift |
crx_inv_lift |
cnx_lift |
cnx_lift |
cnx_inv_lift |
cnx_inv_lift |
cnr_inv_crr |
cnr_inv_crr |
cnr_lref_abst |
cnr_lref_abst |
cnr_lift |
cnr_lift |
cnr_inv_lift |
cnr_inv_lift |
cir_cnr |
cir_cnr |
cnr_inv_cir |
cnr_inv_cir |
cix_lref |
cix_lref |
cix_lift |
cix_lift |
cix_inv_lift |
cix_inv_lift |
sta_fpbq |
sta_fpbq |
cix_cnx |
cix_cnx |
cnx_inv_cix |
cnx_inv_cix |
lstas_llpx_sn_conf |
lstas_llpx_sn_conf |
unfold |
unfold |
lsuby |
lsuby |
lsuby_pair_lt |
lsuby_pair_lt |
lsuby_succ_lt |
lsuby_succ_lt |
lsuby_pair_O_Y |
lsuby_pair_O_Y |
lsuby_refl |
lsuby_refl |
lsuby_O2 |
lsuby_O2 |
lsuby_sym |
lsuby_sym |
lsuby_inv_atom1_aux |
lsuby_inv_atom1_aux |
lsuby_inv_atom1 |
lsuby_inv_atom1 |
lsuby_inv_zero1_aux |
lsuby_inv_zero1_aux |
lsuby_inv_zero1 |
lsuby_inv_zero1 |
lsuby_inv_pair1_aux |
lsuby_inv_pair1_aux |
lsuby_inv_pair1 |
lsuby_inv_pair1 |
lsuby_inv_succ1_aux |
lsuby_inv_succ1_aux |
lsuby_inv_succ1 |
lsuby_inv_succ1 |
lsuby_inv_zero2_aux |
lsuby_inv_zero2_aux |
lsuby_inv_zero2 |
lsuby_inv_zero2 |
lsuby_inv_pair2_aux |
lsuby_inv_pair2_aux |
lsuby_inv_pair2 |
lsuby_inv_pair2 |
lsuby_inv_succ2_aux |
lsuby_inv_succ2_aux |
lsuby_inv_succ2 |
lsuby_inv_succ2 |
lsuby_fwd_length |
lsuby_fwd_length |
lsuby_drop_trans_be |
lsuby_drop_trans_be |
cpy |
cpy |
lsuby_cpy_trans |
lsuby_cpy_trans |
cpy_refl |
cpy_refl |
cpy_full |
cpy_full |
cpy_weak |
cpy_weak |
cpy_weak_top |
cpy_weak_top |
cpy_weak_full |
cpy_weak_full |
cpy_split_up |
cpy_split_up |
cpy_split_down |
cpy_split_down |
cpy_fwd_up |
cpy_fwd_up |
cpy_fwd_tw |
cpy_fwd_tw |
cpy_inv_atom1_aux |
cpy_inv_atom1_aux |
cpy_inv_atom1 |
cpy_inv_atom1 |
cpy_inv_sort1 |
cpy_inv_sort1 |
cpy_inv_lref1 |
cpy_inv_lref1 |
cpy_inv_gref1 |
cpy_inv_gref1 |
cpy_inv_bind1_aux |
cpy_inv_bind1_aux |
cpy_inv_bind1 |
cpy_inv_bind1 |
cpy_inv_flat1_aux |
cpy_inv_flat1_aux |
cpy_inv_flat1 |
cpy_inv_flat1 |
cpy_inv_refl_O2_aux |
cpy_inv_refl_O2_aux |
cpy_inv_refl_O2 |
cpy_inv_refl_O2 |
cpy_inv_lift1_eq |
cpy_inv_lift1_eq |
cpy_lift_le |
cpy_lift_le |
cpy_lift_be |
cpy_lift_be |
cpy_lift_ge |
cpy_lift_ge |
cpy_inv_lift1_le |
cpy_inv_lift1_le |
cpy_inv_lift1_be |
cpy_inv_lift1_be |
cpy_inv_lift1_ge |
cpy_inv_lift1_ge |
cpy_inv_lift1_ge_up |
cpy_inv_lift1_ge_up |
cpy_inv_lift1_be_up |
cpy_inv_lift1_be_up |
cpy_inv_lift1_le_up |
cpy_inv_lift1_le_up |
cpy_conf_eq |
cpy_conf_eq |
cpy_conf_neq |
cpy_conf_neq |
cpy_trans_ge |
cpy_trans_ge |
cpy_trans_down |
cpy_trans_down |
cpy_fwd_nlift2_ge |
cpy_fwd_nlift2_ge |
gget |
gget |
gget_inv_gt |
gget_inv_gt |
gget_inv_eq |
gget_inv_eq |
gget_inv_lt_aux |
gget_inv_lt_aux |
gget_inv_lt |
gget_inv_lt |
gget_total |
gget_total |
gget_mono |
gget_mono |
gget_dec |
gget_dec |
lsuby_trans |
lsuby_trans |
liftv_mono |
liftv_mono |
csx |
csx |
csx_ind |
csx_ind |
csx_intro |
csx_intro |
csx_cpx_trans |
csx_cpx_trans |
cnx_csx |
cnx_csx |
csx_sort |
csx_sort |
csx_cast |
csx_cast |
csx_fwd_pair_sn_aux |
csx_fwd_pair_sn_aux |
csx_fwd_pair_sn |
csx_fwd_pair_sn |
csx_fwd_bind_dx_aux |
csx_fwd_bind_dx_aux |
csx_fwd_bind_dx |
csx_fwd_bind_dx |
csx_fwd_flat_dx_aux |
csx_fwd_flat_dx_aux |
csx_fwd_flat_dx |
csx_fwd_flat_dx |
csx_fwd_bind |
csx_fwd_bind |
csx_fwd_flat |
csx_fwd_flat |
cpre |
cpre |
csx_cpre |
csx_cpre |
cpre_mono |
cpre_mono |
lpxs |
lpxs |
lpxs_ind |
lpxs_ind |
lpxs_ind_dx |
lpxs_ind_dx |
lprs_lpxs |
lprs_lpxs |
lpx_lpxs |
lpx_lpxs |
lpxs_refl |
lpxs_refl |
lpxs_strap1 |
lpxs_strap1 |
lpxs_strap2 |
lpxs_strap2 |
lpxs_pair_refl |
lpxs_pair_refl |
lpxs_inv_atom1 |
lpxs_inv_atom1 |
lpxs_inv_atom2 |
lpxs_inv_atom2 |
lpxs_fwd_length |
lpxs_fwd_length |
fpbs |
fpbs |
fpbs_ind |
fpbs_ind |
fpbs_ind_dx |
fpbs_ind_dx |
fpbs_refl |
fpbs_refl |
fpbq_fpbs |
fpbq_fpbs |
fpbs_strap1 |
fpbs_strap1 |
fpbs_strap2 |
fpbs_strap2 |
fqup_fpbs |
fqup_fpbs |
fqus_fpbs |
fqus_fpbs |
cpxs_fpbs |
cpxs_fpbs |
lpxs_fpbs |
lpxs_fpbs |
lleq_fpbs |
lleq_fpbs |
cprs_fpbs |
cprs_fpbs |
lprs_fpbs |
lprs_fpbs |
fpbs_fqus_trans |
fpbs_fqus_trans |
fpbs_fqup_trans |
fpbs_fqup_trans |
fpbs_cpxs_trans |
fpbs_cpxs_trans |
fpbs_lpxs_trans |
fpbs_lpxs_trans |
fpbs_lleq_trans |
fpbs_lleq_trans |
fqus_fpbs_trans |
fqus_fpbs_trans |
cpxs_fpbs_trans |
cpxs_fpbs_trans |
lpxs_fpbs_trans |
lpxs_fpbs_trans |
lleq_fpbs_trans |
lleq_fpbs_trans |
cpxs_fqus_fpbs |
cpxs_fqus_fpbs |
cpxs_fqup_fpbs |
cpxs_fqup_fpbs |
fqus_lpxs_fpbs |
fqus_lpxs_fpbs |
cpxs_fqus_lpxs_fpbs |
cpxs_fqus_lpxs_fpbs |
lpxs_lleq_fpbs |
lpxs_lleq_fpbs |
cpr_lpr_fpbs |
cpr_lpr_fpbs |
fpbg |
fpbg |
fpb_fpbg |
fpb_fpbg |
fpbg_fpbq_trans |
fpbg_fpbq_trans |
sta_fpbg |
sta_fpbg |
csx_lleq_conf |
csx_lleq_conf |
csx_lleq_trans |
csx_lleq_trans |
fpbs_trans |
fpbs_trans |
lreq_cpxs_trans |
lreq_cpxs_trans |
lpxs_drop_conf |
lpxs_drop_conf |
drop_lpxs_trans |
drop_lpxs_trans |
lpxs_drop_trans_O1 |
lpxs_drop_trans_O1 |
lpxs_pair |
lpxs_pair |
lpxs_inv_pair1 |
lpxs_inv_pair1 |
lpxs_inv_pair2 |
lpxs_inv_pair2 |
lpxs_ind_alt |
lpxs_ind_alt |
lpxs_cpx_trans |
lpxs_cpx_trans |
lpxs_cpxs_trans |
lpxs_cpxs_trans |
cpxs_bind2 |
cpxs_bind2 |
cpxs_inv_abst1 |
cpxs_inv_abst1 |
cpxs_inv_abbr1 |
cpxs_inv_abbr1 |
lpxs_pair2 |
lpxs_pair2 |
lpx_fqup_trans |
lpx_fqup_trans |
lpx_fqus_trans |
lpx_fqus_trans |
lpxs_fquq_trans |
lpxs_fquq_trans |
lpxs_fqup_trans |
lpxs_fqup_trans |
lpxs_fqus_trans |
lpxs_fqus_trans |
lleq_lpxs_trans |
lleq_lpxs_trans |
lpxs_nlleq_inv_step_sn |
lpxs_nlleq_inv_step_sn |
lpxs_lleq_fqu_trans |
lpxs_lleq_fqu_trans |
lpxs_lleq_fquq_trans |
lpxs_lleq_fquq_trans |
lpxs_lleq_fqup_trans |
lpxs_lleq_fqup_trans |
lpxs_lleq_fqus_trans |
lpxs_lleq_fqus_trans |
lreq_lpxs_trans_lleq_aux |
lreq_lpxs_trans_lleq_aux |
lreq_lpxs_trans_lleq |
lreq_lpxs_trans_lleq |
lstas_fpbs |
lstas_fpbs |
sta_fpbs |
sta_fpbs |
cpr_lpr_sta_fpbs |
cpr_lpr_sta_fpbs |
fleq_trans |
fleq_trans |
fleq_canc_sn |
fleq_canc_sn |
fleq_canc_dx |
fleq_canc_dx |
fpbg_fleq_trans |
fpbg_fleq_trans |
fleq_fpbg_trans |
fleq_fpbg_trans |
fleq_fpbs |
fleq_fpbs |
fpbg_fwd_fpbs |
fpbg_fwd_fpbs |
fpbs_fpbg |
fpbs_fpbg |
fpbs_fpb_trans |
fpbs_fpb_trans |
fpb_fpbg_trans |
fpb_fpbg_trans |
fpbq_fpbg_trans |
fpbq_fpbg_trans |
fpbs_fpbg_trans |
fpbs_fpbg_trans |
fpbg_fpbs_trans |
fpbg_fpbs_trans |
fqup_fpbg |
fqup_fpbg |
cpxs_fpbg |
cpxs_fpbg |
lstas_fpbg |
lstas_fpbg |
lpxs_fpbg |
lpxs_fpbg |
fsb |
fsb |
fsb_ind_alt |
fsb_ind_alt |
fsb_inv_csx |
fsb_inv_csx |
fsba |
fsba |
fsba_ind_alt |
fsba_ind_alt |
fsba_fpbs_trans |
fsba_fpbs_trans |
fsb_fsba |
fsb_fsba |
fsba_inv_fsb |
fsba_inv_fsb |
fsb_fpbs_trans |
fsb_fpbs_trans |
fsb_ind_fpbg |
fsb_ind_fpbg |
lpxs_trans |
lpxs_trans |
lsx |
lsx |
lsx_ind |
lsx_ind |
lsx_intro |
lsx_intro |
lsx_atom |
lsx_atom |
lsx_sort |
lsx_sort |
lsx_gref |
lsx_gref |
lsx_ge_up |
lsx_ge_up |
lsx_ge |
lsx_ge |
lsx_fwd_bind_sn |
lsx_fwd_bind_sn |
lsx_fwd_flat_sn |
lsx_fwd_flat_sn |
lsx_fwd_flat_dx |
lsx_fwd_flat_dx |
lsx_fwd_pair_sn |
lsx_fwd_pair_sn |
lsx_inv_flat |
lsx_inv_flat |
lsxa |
lsxa |
lsxa_ind |
lsxa_ind |
lsxa_intro |
lsxa_intro |
lsxa_intro_aux |
lsxa_intro_aux |
lsxa_lleq_trans |
lsxa_lleq_trans |
lsxa_lpxs_trans |
lsxa_lpxs_trans |
lsxa_intro_lpx |
lsxa_intro_lpx |
lsx_lsxa |
lsx_lsxa |
lsxa_inv_lsx |
lsxa_inv_lsx |
lsx_intro_alt |
lsx_intro_alt |
lsx_lpxs_trans |
lsx_lpxs_trans |
lsx_ind_alt |
lsx_ind_alt |
lsx_bind_lpxs_aux |
lsx_bind_lpxs_aux |
lsx_bind |
lsx_bind |
lsx_flat_lpxs |
lsx_flat_lpxs |
lsx_flat |
lsx_flat |
tsts |
tsts |
tsts_inv_atom1_aux |
tsts_inv_atom1_aux |
tsts_inv_atom1 |
tsts_inv_atom1 |
tsts_inv_pair1_aux |
tsts_inv_pair1_aux |
tsts_inv_pair1 |
tsts_inv_pair1 |
tsts_inv_atom2_aux |
tsts_inv_atom2_aux |
tsts_inv_atom2 |
tsts_inv_atom2 |
tsts_inv_pair2_aux |
tsts_inv_pair2_aux |
tsts_inv_pair2 |
tsts_inv_pair2 |
tsts_refl |
tsts_refl |
tsts_sym |
tsts_sym |
tsts_dec |
tsts_dec |
simple_tsts_repl_dx |
simple_tsts_repl_dx |
simple_tsts_repl_sn |
simple_tsts_repl_sn |
tsts_trans |
tsts_trans |
tsts_canc_sn |
tsts_canc_sn |
tsts_canc_dx |
tsts_canc_dx |
csxa |
csxa |
csxa_ind |
csxa_ind |
csx_intro_cpxs |
csx_intro_cpxs |
csxa_intro |
csxa_intro |
csxa_intro_aux |
csxa_intro_aux |
csxa_cpxs_trans |
csxa_cpxs_trans |
csxa_intro_cpx |
csxa_intro_cpx |
csx_csxa |
csx_csxa |
csxa_csx |
csxa_csx |
csx_cpxs_trans |
csx_cpxs_trans |
csx_ind_alt |
csx_ind_alt |
nf |
nf |
candidate |
candidate |
CP0 |
CP0 |
CP1 |
CP1 |
CP2 |
CP2 |
CP3 |
CP3 |
gcp |
gcp |
gcp0_lifts |
gcp0_lifts |
gcp2_lifts |
gcp2_lifts |
gcp2_lifts_all |
gcp2_lifts_all |
csx_lift |
csx_lift |
csx_inv_lift |
csx_inv_lift |
csx_inv_lref_bind |
csx_inv_lref_bind |
csx_lref_bind |
csx_lref_bind |
csx_appl_simple |
csx_appl_simple |
csx_fqu_conf |
csx_fqu_conf |
csx_fquq_conf |
csx_fquq_conf |
csx_fqup_conf |
csx_fqup_conf |
csx_fqus_conf |
csx_fqus_conf |
csx_gcp |
csx_gcp |
csx_lpx_conf |
csx_lpx_conf |
csx_abst |
csx_abst |
csx_abbr |
csx_abbr |
csx_appl_beta_aux |
csx_appl_beta_aux |
csx_appl_beta |
csx_appl_beta |
csx_appl_theta_aux |
csx_appl_theta_aux |
csx_appl_theta |
csx_appl_theta |
csx_appl_simple_tsts |
csx_appl_simple_tsts |
csx_lpxs_conf |
csx_lpxs_conf |
lsx_lref_free |
lsx_lref_free |
lsx_lref_skip |
lsx_lref_skip |
lsx_fwd_lref_be |
lsx_fwd_lref_be |
lsx_lift_le |
lsx_lift_le |
lsx_lift_ge |
lsx_lift_ge |
lsx_inv_lift_le |
lsx_inv_lift_le |
lsx_inv_lift_be |
lsx_inv_lift_be |
lsx_inv_lift_ge |
lsx_inv_lift_ge |
lsx_lleq_trans |
lsx_lleq_trans |
lsx_lpx_trans |
lsx_lpx_trans |
lsx_lreq_conf |
lsx_lreq_conf |
lsx_fwd_bind_dx |
lsx_fwd_bind_dx |
lsx_inv_bind |
lsx_inv_bind |
lcosx |
lcosx |
lcosx_O |
lcosx_O |
lcosx_drop_trans_lt |
lcosx_drop_trans_lt |
lcosx_inv_succ_aux |
lcosx_inv_succ_aux |
lcosx_inv_succ |
lcosx_inv_succ |
lcosx_inv_pair |
lcosx_inv_pair |
lsx_cpx_trans_lcosx |
lsx_cpx_trans_lcosx |
lsx_cpx_trans_O |
lsx_cpx_trans_O |
lsx_lref_be_lpxs |
lsx_lref_be_lpxs |
lsx_lref_be |
lsx_lref_be |
csx_lsx |
csx_lsx |
fpbs_aaa_conf |
fpbs_aaa_conf |
at_mono |
at_mono |
lifts_lift_trans_le |
lifts_lift_trans_le |
lifts_lift_trans |
lifts_lift_trans |
liftsv_liftv_trans_le |
liftsv_liftv_trans_le |
drops_drop_trans |
drops_drop_trans |
S1 |
S1 |
S2 |
S2 |
S3 |
S3 |
S4 |
S4 |
S5 |
S5 |
S6 |
S6 |
S7 |
S7 |
gcr |
gcr |
cfun |
cfun |
acr |
acr |
gcr_lift |
gcr_lift |
gcr_lifts |
gcr_lifts |
acr_gcr |
acr_gcr |
acr_abst |
acr_abst |
cpxs_fwd_cnx |
cpxs_fwd_cnx |
cpxs_fwd_sort |
cpxs_fwd_sort |
cpxs_fwd_beta |
cpxs_fwd_beta |
cpxs_fwd_delta |
cpxs_fwd_delta |
cpxs_fwd_theta |
cpxs_fwd_theta |
cpxs_fwd_cast |
cpxs_fwd_cast |
lleq_cpxs_trans |
lleq_cpxs_trans |
cpxs_lleq_conf |
cpxs_lleq_conf |
cpxs_lleq_conf_dx |
cpxs_lleq_conf_dx |
cpxs_lleq_conf_sn |
cpxs_lleq_conf_sn |
lprs_drop_conf |
lprs_drop_conf |
drop_lprs_trans |
drop_lprs_trans |
lprs_drop_trans_O1 |
lprs_drop_trans_O1 |
fpbg_trans |
fpbg_trans |
scpds_lift |
scpds_lift |
scpds_inv_lift1 |
scpds_inv_lift1 |
lifts_trans |
lifts_trans |
drops_trans |
drops_trans |
lsubc |
lsubc |
lsubc_inv_atom1_aux |
lsubc_inv_atom1_aux |
lsubc_inv_atom1 |
lsubc_inv_atom1 |
lsubc_inv_pair1_aux |
lsubc_inv_pair1_aux |
lsubc_inv_pair1 |
lsubc_inv_pair1 |
lsubc_inv_atom2_aux |
lsubc_inv_atom2_aux |
lsubc_inv_atom2 |
lsubc_inv_atom2 |
lsubc_inv_pair2_aux |
lsubc_inv_pair2_aux |
lsubc_inv_pair2 |
lsubc_inv_pair2 |
lsubc_fwd_lsubr |
lsubc_fwd_lsubr |
lsubc_refl |
lsubc_refl |
lsubc_drop_O1_trans |
lsubc_drop_O1_trans |
drop_lsubc_trans |
drop_lsubc_trans |
drops_lsubc_trans |
drops_lsubc_trans |
acr_aaa_csubc_lifts |
acr_aaa_csubc_lifts |
acr_aaa |
acr_aaa |
gcr_aaa |
gcr_aaa |
tsts_inv_bind_applv_simple |
tsts_inv_bind_applv_simple |
cpxs_fwd_cnx_vector |
cpxs_fwd_cnx_vector |
cpxs_fwd_sort_vector |
cpxs_fwd_sort_vector |
cpxs_fwd_beta_vector |
cpxs_fwd_beta_vector |
cpxs_fwd_delta_vector |
cpxs_fwd_delta_vector |
cpxs_fwd_theta_vector |
cpxs_fwd_theta_vector |
cpxs_fwd_cast_vector |
cpxs_fwd_cast_vector |
csxv |
csxv |
csxv_inv_cons |
csxv_inv_cons |
csx_fwd_applv |
csx_fwd_applv |
csx_applv_cnx |
csx_applv_cnx |
csx_applv_sort |
csx_applv_sort |
csx_applv_beta |
csx_applv_beta |
csx_applv_delta |
csx_applv_delta |
csx_applv_theta |
csx_applv_theta |
csx_applv_cast |
csx_applv_cast |
csx_gcr |
csx_gcr |
aaa_csx |
aaa_csx |
aaa_ind_csx_aux |
aaa_ind_csx_aux |
aaa_ind_csx |
aaa_ind_csx |
aaa_ind_csx_alt_aux |
aaa_ind_csx_alt_aux |
aaa_ind_csx_alt |
aaa_ind_csx_alt |
lprs_strip |
lprs_strip |
lprs_conf |
lprs_conf |
lprs_trans |
lprs_trans |
fpbsa |
fpbsa |
fpb_fpbsa_trans |
fpb_fpbsa_trans |
fpbs_fpbsa |
fpbs_fpbsa |
fpbsa_inv_fpbs |
fpbsa_inv_fpbs |
fpbs_intro_alt |
fpbs_intro_alt |
fpbs_inv_alt |
fpbs_inv_alt |
fpbs_cpx_trans_neq |
fpbs_cpx_trans_neq |
fpb_fpbs |
fpb_fpbs |
csx_fpb_conf |
csx_fpb_conf |
csx_fpbs_conf |
csx_fpbs_conf |
csx_fsb_fpbs |
csx_fsb_fpbs |
csx_fsb |
csx_fsb |
csx_ind_fpb |
csx_ind_fpb |
csx_ind_fpbg |
csx_ind_fpbg |
aaa_fsb |
aaa_fsb |
aaa_fsba |
aaa_fsba |
aaa_ind_fpb_aux |
aaa_ind_fpb_aux |
aaa_ind_fpb |
aaa_ind_fpb |
aaa_ind_fpbg_aux |
aaa_ind_fpbg_aux |
aaa_ind_fpbg |
aaa_ind_fpbg |
cpxe |
cpxe |
csx_cpxe |
csx_cpxe |
lpxs_aaa_conf |
lpxs_aaa_conf |
lprs_aaa_conf |
lprs_aaa_conf |
lsuba_lsubc |
lsuba_lsubc |
ApplDelta |
ApplDelta |
ApplOmega1 |
ApplOmega1 |
ApplOmega2 |
ApplOmega2 |
ApplOmega3 |
ApplOmega3 |
ApplDelta_lift |
ApplDelta_lift |
cpr_ApplOmega_12 |
cpr_ApplOmega_12 |
cpr_ApplOmega_23 |
cpr_ApplOmega_23 |
cpxs_ApplOmega_13 |
cpxs_ApplOmega_13 |
fqup_ApplOmega_13 |
fqup_ApplOmega_13 |
fpbg_refl |
fpbg_refl |
Delta |
Delta |
Omega1 |
Omega1 |
Omega2 |
Omega2 |
Delta_lift |
Delta_lift |
cpr_Omega_12 |
cpr_Omega_12 |
cpr_Omega_21 |
cpr_Omega_21 |
sta_ldec |
sta_ldec |
snv |
snv |
snv_inv_lref_aux |
snv_inv_lref_aux |
snv_inv_lref |
snv_inv_lref |
snv_inv_gref_aux |
snv_inv_gref_aux |
snv_inv_gref |
snv_inv_gref |
snv_inv_bind_aux |
snv_inv_bind_aux |
snv_inv_bind |
snv_inv_bind |
snv_inv_appl_aux |
snv_inv_appl_aux |
snv_inv_appl |
snv_inv_appl |
snv_inv_cast_aux |
snv_inv_cast_aux |
snv_inv_cast |
snv_inv_cast |
snv_extended |
snv_extended |
snv_restricted |
snv_restricted |
snv_fwd_aaa |
snv_fwd_aaa |
snv_fwd_da |
snv_fwd_da |
snv_fwd_lstas |
snv_fwd_lstas |
snv_fwd_fsb |
snv_fwd_fsb |
snv_lift |
snv_lift |
snv_inv_lift |
snv_inv_lift |
snv_fqu_conf |
snv_fqu_conf |
snv_fquq_conf |
snv_fquq_conf |
snv_fqup_conf |
snv_fqup_conf |
snv_fqus_conf |
snv_fqus_conf |
IH_snv_cpr_lpr |
IH_snv_cpr_lpr |
IH_da_cpr_lpr |
IH_da_cpr_lpr |
IH_lstas_cpr_lpr |
IH_lstas_cpr_lpr |
IH_snv_lstas |
IH_snv_lstas |
snv_cprs_lpr_aux |
snv_cprs_lpr_aux |
da_cprs_lpr_aux |
da_cprs_lpr_aux |
da_scpds_lpr_aux |
da_scpds_lpr_aux |
da_scpes_aux |
da_scpes_aux |
lstas_cprs_lpr_aux |
lstas_cprs_lpr_aux |
scpds_cpr_lpr_aux |
scpds_cpr_lpr_aux |
scpes_cpr_lpr_aux |
scpes_cpr_lpr_aux |
lstas_scpds_aux |
lstas_scpds_aux |
scpes_le_aux |
scpes_le_aux |
snv_cast_scpes |
snv_cast_scpes |
shnv |
shnv |
shnv_inv_cast_aux |
shnv_inv_cast_aux |
shnv_inv_cast |
shnv_inv_cast |
shnv_inv_snv |
shnv_inv_snv |
snv_shnv_cast |
snv_shnv_cast |
lsubsv |
lsubsv |
lsubsv_inv_atom1_aux |
lsubsv_inv_atom1_aux |
lsubsv_inv_atom1 |
lsubsv_inv_atom1 |
lsubsv_inv_pair1_aux |
lsubsv_inv_pair1_aux |
lsubsv_inv_pair1 |
lsubsv_inv_pair1 |
lsubsv_inv_atom2_aux |
lsubsv_inv_atom2_aux |
lsubsv_inv_atom2 |
lsubsv_inv_atom2 |
lsubsv_inv_pair2_aux |
lsubsv_inv_pair2_aux |
lsubsv_inv_pair2 |
lsubsv_inv_pair2 |
lsubsv_fwd_lsubr |
lsubsv_fwd_lsubr |
lsubsv_refl |
lsubsv_refl |
lsubsv_cprs_trans |
lsubsv_cprs_trans |
lsubsv_drop_O1_conf |
lsubsv_drop_O1_conf |
lsubsv_drop_O1_trans |
lsubsv_drop_O1_trans |
lsubsv_fwd_lsubd |
lsubsv_fwd_lsubd |
lsubsv_lstas_trans |
lsubsv_lstas_trans |
lsubsv_sta_trans |
lsubsv_sta_trans |
lsubsv_scpds_trans |
lsubsv_scpds_trans |
lsubsv_snv_trans |
lsubsv_snv_trans |
snv_cpr_lpr_aux |
snv_cpr_lpr_aux |
lstas_cpr_lpr_aux |
lstas_cpr_lpr_aux |
snv_lstas_aux |
snv_lstas_aux |
lsubsv_fwd_lsuba |
lsubsv_fwd_lsuba |
da_cpr_lpr_aux |
da_cpr_lpr_aux |
lsubsv_cpcs_trans |
lsubsv_cpcs_trans |
snv_preserve |
snv_preserve |
da_cpr_lpr |
da_cpr_lpr |
snv_cpr_lpr |
snv_cpr_lpr |
snv_lstas |
snv_lstas |
lstas_cpr_lpr |
lstas_cpr_lpr |
snv_cprs_lpr |
snv_cprs_lpr |
da_cprs_lpr |
da_cprs_lpr |
lstas_cprs_lpr |
lstas_cprs_lpr |
lstas_cpcs_lpr |
lstas_cpcs_lpr |
cpys |
cpys |
cpys_ind |
cpys_ind |
cpys_ind_dx |
cpys_ind_dx |
cpy_cpys |
cpy_cpys |
cpys_strap1 |
cpys_strap1 |
cpys_strap2 |
cpys_strap2 |
lsuby_cpys_trans |
lsuby_cpys_trans |
cpys_refl |
cpys_refl |
cpys_bind |
cpys_bind |
cpys_flat |
cpys_flat |
cpys_weak |
cpys_weak |
cpys_weak_top |
cpys_weak_top |
cpys_weak_full |
cpys_weak_full |
cpys_fwd_up |
cpys_fwd_up |
cpys_fwd_tw |
cpys_fwd_tw |
cpys_inv_sort1 |
cpys_inv_sort1 |
cpys_inv_gref1 |
cpys_inv_gref1 |
cpys_inv_bind1 |
cpys_inv_bind1 |
cpys_inv_flat1 |
cpys_inv_flat1 |
cpys_inv_refl_O2 |
cpys_inv_refl_O2 |
cpys_inv_lift1_eq |
cpys_inv_lift1_eq |
cpys_subst |
cpys_subst |
cpys_subst_Y2 |
cpys_subst_Y2 |
cpys_inv_atom1 |
cpys_inv_atom1 |
cpys_inv_lref1 |
cpys_inv_lref1 |
cpys_inv_lref1_Y2 |
cpys_inv_lref1_Y2 |
cpys_inv_lref1_drop |
cpys_inv_lref1_drop |
cpys_lift_le |
cpys_lift_le |
cpys_lift_be |
cpys_lift_be |
cpys_lift_ge |
cpys_lift_ge |
cpys_inv_lift1_le |
cpys_inv_lift1_le |
cpys_inv_lift1_be |
cpys_inv_lift1_be |
cpys_inv_lift1_ge |
cpys_inv_lift1_ge |
cpys_inv_lift1_ge_up |
cpys_inv_lift1_ge_up |
cpys_inv_lift1_be_up |
cpys_inv_lift1_be_up |
cpys_inv_lift1_le_up |
cpys_inv_lift1_le_up |
cpys_inv_lift1_subst |
cpys_inv_lift1_subst |
cpysa |
cpysa |
lsuby_cpysa_trans |
lsuby_cpysa_trans |
cpysa_refl |
cpysa_refl |
cpysa_cpy_trans |
cpysa_cpy_trans |
cpys_cpysa |
cpys_cpysa |
cpysa_inv_cpys |
cpysa_inv_cpys |
cpys_ind_alt |
cpys_ind_alt |
cpys_inv_SO2 |
cpys_inv_SO2 |
cpys_strip_eq |
cpys_strip_eq |
cpys_strip_neq |
cpys_strip_neq |
cpys_strap1_down |
cpys_strap1_down |
cpys_strap2_down |
cpys_strap2_down |
cpys_split_up |
cpys_split_up |
cpys_inv_lift1_up |
cpys_inv_lift1_up |
cpys_conf_eq |
cpys_conf_eq |
cpys_conf_neq |
cpys_conf_neq |
cpys_trans_eq |
cpys_trans_eq |
cpys_trans_down |
cpys_trans_down |
cpys_antisym_eq |
cpys_antisym_eq |
llpx_sn_TC_pair_dx |
llpx_sn_TC_pair_dx |
fqup_trans |
fqup_trans |
lleq_intro_alt_r |
lleq_intro_alt_r |
lleq_ind_alt_r |
lleq_ind_alt_r |
lleq_inv_alt_r |
lleq_inv_alt_r |