X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fcore.html;h=a82d853eb61ea409429e8c4b600ed4c3bdac5d07;hb=e866d78af74246133f5a14cb711a62af39308dee;hp=23fa28631d570d38dc30e3fc28ac5adaa34760dc;hpb=65383ff6ec2236b0a61310b872ea4cd5fcc26fb7;p=helm.git
diff --git a/helm/www/lambdadelta/core.html b/helm/www/lambdadelta/core.html
index 23fa28631..a82d853eb 100644
--- a/helm/www/lambdadelta/core.html
+++ b/helm/www/lambdadelta/core.html
@@ -1,7121 +1,3 @@
-
-
-
-
-
-
-
- \lambda\delta home page
-
-
-
-
-
-
-
- cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
-
-
-
-
-
-
-
- Summary of the Specification
-
-
-
-
-
- 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 |
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- Last update: Wed, 08 Mar 2017 22:36:31 +0100
-
-
+\lambda\delta home pagecic:/matita/lambdadelta/basic_2/ (core λδ version 2)
Summary of the Specification
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 |
Last update: Thu, 09 Mar 2017 13:38:17 +0100