X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fcore.html;h=f0ff46f51d8f8695775ae71fabd4a13376c8a752;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=a82d853eb61ea409429e8c4b600ed4c3bdac5d07;hpb=e866d78af74246133f5a14cb711a62af39308dee;p=helm.git diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html index a82d853eb..f0ff46f51 100644 --- a/helm/www/lambdadelta/core.html +++ b/helm/www/lambdadelta/core.html @@ -1,3 +1,7121 @@ -
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 |
+ home + | ++ news + | ++ specification + | +
+ + |
+
+ + |
+ + documentation + | ++ implementation + | +
+ + |
+
+ foreword + | ++ milestones + | ++ version 2 + | +(background - core - applications) | +
+ + |
+ + version 2 + | ++ helena + | ++ Open Symbolic Notation (OSN) + | +
+ citations + | ++ visibility + | ++ version 1 + | +(background - core) | +(static HELM directory) | ++ version 1 + | ++ library + | +(static LDDL directory) | +
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 | +