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 |