X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fnames.txt;h=852ff574b606a5949daec454b52b2790cc5426a8;hp=d80ea011a72c21b409719bde01ff05a83f6e4b06;hb=076439def28e649ec384fae038ed021dadd5f75c;hpb=d2545ffd201b1aa49887313791386add78fa8603 diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index d80ea011a..852ff574b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -1,105 +1,1207 @@ -NAMING CONVENTIONS FOR METAVARIABLES - -A,B : arity -C : candidate of reducibility -D,E : RTM environment -F,G : global environment -H : reserved: transient premise -IH : reserved: inductive premise -I,J : item -K,L : local environment -M,N : reserved: future use -O : -P : relocation environment -Q : elimination predicate -R : generic predicate/relation -S : RTM stack -T,U,V,W: term -X,Y,Z : reserved: transient objet denoted by a capital letter - -a : applicability condition (true = restricted, false = general) -b : local dropping kind parameter (true = restricted, false = general) -c : rt-reduction count parameter -d : term degree -e : reserved: future use (\lambda\delta 3) -f,g : local reference transforming map -h : sort hierarchy parameter -i,j : local reference depth (de Bruijn's) -k,l : global reference level -m,n : iterations -o : sort degree parameter (origin) -p,q : binder polarity -r : -s : sort index -t,u : -v,w : local reference position level (de Bruijn's) (RTM) -x,y,z : reserved: transient objet denoted by a small letter - -NAMING CONVENTIONS FOR CONSTRUCTORS - -0: atomic -2: binary - -A: application to vector -E: empty list -F: boolean false -T: boolean true - -a: application -b: generic binder with one argument -d: abbreviation -f: generic flat with one argument -i: generic binder for local environments -l: typed abstraction -n: native type annotation -u: generic binder with zero argument -x: exclusion - -NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS - -- prefix and first letter - -b: bi contex-sensitive for local environments -c: contex-sensitive for terms -f: context-freee for closures -l: sn contex-sensitive for local environments -r: dx contex-sensitive for local environments -s: stratified (prefix) -t: context-free for terms - -- second letter - -e: reserved for generic entrywise extension -i: irreducible form -n: normal form -p: reflexive parallel transformation -q: sequential transformation -r: reducible form -s: strongly normalizing form - -- third letter - -b: (q)rst-reduction -c: conversion -d: decomposed rt-reduction -e: decomposed rt-conversion -g: counted rt-transition (generic) -m: semi-counted rt-transition (mixed) -q: restricted reduction -r: reduction -s: substitution -u: supclosure -w: reserved for generic pointwise extension -x: uncounted rt-transition (extended) -y: rt-substitution - -- forth letter (if present) - -c: proper single step (general) (successor) -e: reflexive transitive closure to normal form (evaluation) -g: proper multiple step (general) (greater) -p: non-reflexive transitive closure (plus) -q: reflexive closure (question) -r: proper multiple step (restricted) (restricted) -s: reflexive transitive closure (star) -u: proper single step (restricted) (unit) +aaa_cpm_SO +aaa_csx +aaa_fsb +aaa_ind_csx +aaa_ind_csx_aux +aaa_ind_csx_cpxs +aaa_ind_csx_cpxs_aux +aaa_ind_fpb +aaa_ind_fpb_aux +aaa_ind_fpbg +aaa_ind_fpbg_aux +cnr +cnr_abbr_neg +cnr_abst +cnr_appl_simple +cnr_dec_teqx +cnr_gref +cnr_inv_abbr_neg +cnr_inv_abst +cnr_inv_appl +cnr_inv_cast +cnr_inv_lifts +cnr_inv_lref_abbr +cnr_lifts +cnr_lref_abst +cnr_lref_atom +cnr_lref_unit +cnr_sort +cnuw +cnuw_abbr_neg +cnuw_abst +cnuw_appl_simple +cnuw_atom_drops +cnuw_cpms_trans +cnuw_ctop +cnuw_dec +cnuw_dec_ex +cnuw_fwd_appl +cnuw_gref +cnuw_inv_abbr_pos +cnuw_inv_cast +cnuw_inv_lifts +cnuw_inv_zero_pair +cnuw_lifts +cnuw_lref +cnuw_sort +cnuw_unit_drops +cnuw_zero_unit +cnv +cnv_acle_omega +cnv_acle_one +cnv_acle_trans +cnv_appl +cnv_appl_cpes +cnv_appl_cpts +cnv_appl_ge +cnv_appl_ntas_ge +cnv_bind +cnv_cast +cnv_cast_cpes +cnv_cast_cpts +cnv_cpcs_dec +cnv_cpes_dec +cnv_cpm_conf_lpr_appl_appl_aux +cnv_cpm_conf_lpr_appl_beta_aux +cnv_cpm_conf_lpr_appl_theta_aux +cnv_cpm_conf_lpr_atom_atom_aux +cnv_cpm_conf_lpr_atom_delta_aux +cnv_cpm_conf_lpr_atom_ell_aux +cnv_cpm_conf_lpr_atom_ess_aux +cnv_cpm_conf_lpr_aux +cnv_cpm_conf_lpr_beta_beta_aux +cnv_cpm_conf_lpr_bind_bind_aux +cnv_cpm_conf_lpr_bind_zeta_aux +cnv_cpm_conf_lpr_cast_cast_aux +cnv_cpm_conf_lpr_cast_ee_aux +cnv_cpm_conf_lpr_cast_epsilon_aux +cnv_cpm_conf_lpr_delta_delta_aux +cnv_cpm_conf_lpr_delta_ell_aux +cnv_cpm_conf_lpr_ee_ee_aux +cnv_cpm_conf_lpr_epsilon_ee_aux +cnv_cpm_conf_lpr_epsilon_epsilon_aux +cnv_cpm_conf_lpr_sub +cnv_cpm_conf_lpr_theta_theta_aux +cnv_cpm_conf_lpr_zeta_zeta_aux +cnv_cpmre_cpms_conf +cnv_cpmre_mono +cnv_cpmre_trans +cnv_cpms_conf +cnv_cpms_conf_eq +cnv_cpms_conf_lpr +cnv_cpms_conf_lpr_aux +cnv_cpms_conf_lpr_refl_tneqx_sub +cnv_cpms_conf_lpr_step_tneqx_sub +cnv_cpms_conf_lpr_teqx_teqx_aux +cnv_cpms_conf_lpr_teqx_tneqx_aux +cnv_cpms_conf_lpr_tneqx_tneqx_aux +cnv_cpms_fwd_appl_sn_decompose +cnv_cpms_nta +cnv_cpms_ntas +cnv_cpms_strip_lpr_sub +cnv_cpms_teqx_conf_lpr_aux +cnv_cpms_teqx_strip_lpr_aux +cnv_cpms_trans +cnv_cpms_trans_lpr +cnv_cpms_trans_lpr_sub +cnv_cpm_teqx_conf_lpr +cnv_cpm_teqx_conf_lpr_appl_appl_aux +cnv_cpm_teqx_conf_lpr_atom_atom_aux +cnv_cpm_teqx_conf_lpr_atom_ess_aux +cnv_cpm_teqx_conf_lpr_aux +cnv_cpm_teqx_conf_lpr_bind_bind_aux +cnv_cpm_teqx_conf_lpr_cast_cast_aux +cnv_cpm_teqx_cpm_trans_aux +cnv_cpm_teqx_cpm_trans_sub +cnv_cpm_trans +cnv_cpm_trans_lpr +cnv_cpm_trans_lpr_aux +cnv_cpmuwe_mono +cnv_cpmuwe_trans +cnv_cpr_teqx_fwd_refl +cnv_dec +cnv_fpbg_refl_false +cnv_fqu_conf +cnv_fqup_conf +cnv_fquq_conf +cnv_fqus_conf +cnv_fwd_aaa +cnv_fwd_cpms_abst_dx_le +cnv_fwd_cpm_SO +cnv_fwd_cpms_total +cnv_fwd_csx +cnv_fwd_flat +cnv_fwd_fsb +cnv_fwd_pair_sn +cnv_ind_cpes +cnv_inv_appl +cnv_inv_appl_aux +cnv_inv_appl_cpes +cnv_inv_appl_cpts +cnv_inv_appl_ntas +cnv_inv_bind +cnv_inv_bind_aux +cnv_inv_cast +cnv_inv_cast_aux +cnv_inv_cast_cpes +cnv_inv_cast_cpts +cnv_inv_gref +cnv_inv_gref_aux +cnv_inv_lifts +cnv_inv_lref +cnv_inv_lref_atom +cnv_inv_lref_aux +cnv_inv_lref_drops +cnv_inv_lref_pair +cnv_inv_lref_unit +cnv_inv_zero +cnv_inv_zero_aux +cnv_lifts +cnv_lprs_trans +cnv_lpr_trans +cnv_lref +cnv_lref_drops +cnv_nta_sn +cnv_preserve +cnv_R_cpmuwe_dec +cnv_R_cpmuwe_total +cnv_sort +cnv_zero +cnx +cnx_abst +cnx_appl_simple +cnx_csx +cnx_inv_abbr_neg +cnx_inv_abbr_pos +cnx_inv_abst +cnx_inv_appl +cnx_inv_cast +cnx_inv_lifts +cnx_inv_lref_pair +cnx_lifts +cnx_lref_atom +cnx_lref_unit +cnx_sort +cnx_teqx_trans +cpc +cpc_conf +cpc_cpcs +cpc_fwd_cpr +cpc_refl +cpcs +cpcs_aaa_mono +cpcs_bind1 +cpcs_bind2 +cpcs_bind_dx +cpcs_bind_sn +cpcs_canc_dx +cpcs_canc_sn +cpcs_cpr_conf +cpcs_cpr_div +cpcs_cprs_conf +cpcs_cprs_div +cpcs_cprs_dx +cpcs_cprs_sn +cpcs_cprs_step_dx +cpcs_cprs_step_sn +cpcs_cpr_step_dx +cpcs_cpr_step_sn +cpcs_flat +cpcs_flat_dx_cpr_rev +cpcs_ind_dx +cpcs_ind_sn +cpcs_inv_abst_bi_dx +cpcs_inv_abst_bi_sn +cpcs_inv_abst_dx +cpcs_inv_abst_sn +cpcs_inv_cprs +cpcs_inv_lifts_bi +cpcs_inv_sort_abst +cpcs_inv_sort_bi +cpcs_lifts_bi +cpcs_refl +cpcs_step_dx +cpcs_step_sn +cpcs_strip +cpcs_sym +cpcs_trans +cpc_sym +cpes +cpes_aaa_mono +cpes_cpes_trans +cpes_cpms_div +cpes_cprs_trans +cpes_fwd_abst_bi +cpes_refl +cpes_refl_aaa +cpes_sym +cpg +cpg_appl +cpg_atom +cpg_beta +cpg_bind +cpg_cast +cpg_cpx +cpg_delta +cpg_delta_drops +cpg_ee +cpg_ell +cpg_ell_drops +cpg_eps +cpg_ess +cpg_fwd_bind1_minus +cpg_inv_abbr1 +cpg_inv_abst1 +cpg_inv_appl1 +cpg_inv_appl1_aux +cpg_inv_appl1_simple +cpg_inv_atom1 +cpg_inv_atom1_aux +cpg_inv_atom1_drops +cpg_inv_bind1 +cpg_inv_bind1_aux +cpg_inv_cast1 +cpg_inv_cast1_aux +cpg_inv_gref1 +cpg_inv_lifts_bi +cpg_inv_lifts_sn +cpg_inv_lref1 +cpg_inv_lref1_bind +cpg_inv_lref1_drops +cpg_inv_sort1 +cpg_inv_zero1 +cpg_inv_zero1_pair +cpg_lifts_bi +cpg_lifts_sn +cpg_lref +cpg_refl +cpg_theta +cpg_zeta +cpm +cpm_aaa_conf +cpm_appl +cpm_beta +cpm_bind +cpm_bind2 +cpm_bind_unit +cpm_cast +cpm_cpms +cpm_delta +cpm_delta_drops +cpm_ee +cpm_ell +cpm_ell_drops +cpm_eps +cpm_ess +cpm_fpb +cpm_fpbq +cpm_fsge_comp +cpm_fwd_bind1_minus +cpm_fwd_cpx +cpm_fwd_plus +cpm_fwd_plus_aux +cpm_ind +cpm_inv_abbr1 +cpm_inv_abst1 +cpm_inv_abst_bi +cpm_inv_appl1 +cpm_inv_appl1_simple +cpm_inv_atom1 +cpm_inv_atom1_drops +cpm_inv_bind1 +cpm_inv_cast1 +cpm_inv_gref1 +cpm_inv_lifts_bi +cpm_inv_lifts_sn +cpm_inv_lref1 +cpm_inv_lref1_ctop +cpm_inv_lref1_drops +cpm_inv_sort1 +cpm_inv_zero1 +cpm_inv_zero1_unit +cpm_lifts_bi +cpm_lifts_sn +cpm_lref +cpmre +cpmre_fwd_cpms +cpmre_intro +cpmre_total_aaa +cpm_rex_conf +cpms +cpms_aaa_conf +cpms_abst_dx_le_aaa +cpms_appl +cpms_appl_dx +cpms_beta +cpms_beta_dx +cpms_beta_rc +cpms_bind +cpms_bind2_dx +cpms_bind_alt +cpms_bind_dx +cpms_cast +cpms_cast_sn +cpms_cprre_trans +cpms_cprs_trans +cpms_delta +cpms_delta_drops +cpms_div +cpms_ee +cpms_ell +cpms_ell_drops +cpms_eps +cpms_fpbg_trans +cpms_fwd_cpxs +cpms_fwd_fpbs +cpms_ind_dx +cpms_ind_sn +cpms_inv_abbr_abst +cpms_inv_abbr_sn_dx +cpms_inv_abst_bi +cpms_inv_abst_sn +cpms_inv_abst_sn_cprs +cpms_inv_appl_sn +cpms_inv_cast1 +cpms_inv_delta_sn +cpms_inv_ell_sn +cpms_inv_gref1 +cpms_inv_lifts_bi +cpms_inv_lifts_sn +cpms_inv_lref1_ctop +cpms_inv_lref1_drops +cpms_inv_lref_sn +cpms_inv_plus +cpms_inv_sort1 +cpms_inv_succ_sn +cpms_inv_zero1_unit +cpms_lifts_bi +cpms_lifts_sn +cpms_lref +cpm_sort +cpms_reqx_conf_dx +cpms_reqx_conf_sn +cpms_sort +cpms_step_dx +cpms_step_sn +cpms_teqx_ind_sn +cpms_theta +cpms_theta_dx +cpms_theta_rc +cpms_tneqx_fwd_fpbg +cpms_tneqx_fwd_step_sn_aux +cpms_total_aaa +cpms_trans +cpms_trans_swap +cpms_zeta +cpms_zeta_dx +cpm_teqx_free +cpm_teqx_ind +cpm_teqx_inv_appl_sn +cpm_teqx_inv_atom_sn +cpm_teqx_inv_bind_dx +cpm_teqx_inv_bind_sn +cpm_teqx_inv_bind_sn_void +cpm_teqx_inv_cast_sn +cpm_teqx_inv_lref_sn +cpm_theta +cpm_tneqx_cpm_cpms_teqx_sym_fwd_fpbg +cpm_tneqx_cpm_fpbg +cpmuwe +cpmuwe_abbr_neg +cpmuwe_abst +cpmuwe_ctop +cpmuwe_fwd_cpms +cpmuwe_gref +cpmuwe_intro +cpmuwe_sort +cpmuwe_total_csx +cpmuwe_zero_unit +cpm_zeta +cpr_abbr_pos_tneqx +cpr_conf +cpr_conf_lpr +cpr_conf_lpr_atom_atom +cpr_conf_lpr_atom_delta +cpr_conf_lpr_beta_beta +cpr_conf_lpr_bind_bind +cpr_conf_lpr_bind_zeta +cpr_conf_lpr_delta_delta +cpr_conf_lpr_eps_eps +cpr_conf_lpr_flat_beta +cpr_conf_lpr_flat_eps +cpr_conf_lpr_flat_flat +cpr_conf_lpr_flat_theta +cpr_conf_lpr_theta_theta +cpr_conf_lpr_zeta_zeta +cpr_cpcs_dx +cpr_cpcs_sn +cpr_cprs_conf_cpcs +cpr_cprs_div +cpr_div +cpr_ext +cpr_flat +cpr_ind +cpr_inv_atom1 +cpr_inv_atom1_drops +cpr_inv_cast1 +cpr_inv_flat1 +cpr_inv_gref1 +cpr_inv_lref1 +cpr_inv_lref1_drops +cpr_inv_sort1 +cpr_inv_zero1 +cpr_pair_sn +cprre_cprs_conf +cpr_refl +cprre_mono +cprre_total_csx +cprs_abbr_pos_twneq +cprs_conf +cprs_conf_cpcs +cprs_cpr_conf_cpcs +cprs_cpr_div +cprs_CTC +cprs_div +cprs_ext +cprs_flat +cprs_flat_dx +cprs_flat_sn +cprs_ind_dx +cprs_ind_sn +cprs_inv_appl_sn +cprs_inv_cast1 +cprs_inv_cnr_sn +cprs_inv_CTC +cprs_inv_lref1_drops +cprs_inv_sort1 +cprs_lpr_conf_dx +cprs_lpr_conf_sn +cprs_nta_trans +cprs_nta_trans_cnv +cprs_refl +cprs_step_dx +cprs_step_sn +cprs_strip +cprs_trans +cpr_subst +cpt +cpt_appl +cpt_bind +cpt_cast +cpt_cpts +cpt_delta +cpt_delta_drops +cpt_ee +cpt_ell +cpt_ell_drops +cpt_ess +cpt_fwd_cpm +cpt_fwd_plus +cpt_fwd_plus_aux +cpt_ind +cpt_inv_appl_sn +cpt_inv_atom_sn +cpt_inv_atom_sn_drops +cpt_inv_bind_sn +cpt_inv_cast_sn +cpt_inv_gref_sn +cpt_inv_lifts_bi +cpt_inv_lifts_sn +cpt_inv_lref_sn +cpt_inv_lref_sn_ctop +cpt_inv_lref_sn_drops +cpt_inv_sort_sn +cpt_inv_zero_sn +cpt_inv_zero_sn_unit +cpt_lifts_bi +cpt_lifts_sn +cpt_lref +cpt_refl +cpts +cpts_appl_dx +cpts_bind_dx +cpts_cast_sn +cpts_cpms_conf_eq +cpts_cprs_trans +cpts_delta +cpts_delta_drops +cpts_ee +cpts_ell +cpts_ell_drops +cpts_fwd_cpms +cpts_ind_dx +cpts_ind_sn +cpts_inv_cast_sn +cpts_inv_delta_sn +cpts_inv_ell_sn +cpts_inv_gref_sn +cpts_inv_lifts_bi +cpts_inv_lifts_sn +cpts_inv_lref_sn +cpts_inv_lref_sn_ctop +cpts_inv_lref_sn_drops +cpts_inv_sort_sn +cpts_inv_succ_sn +cpts_inv_zero_sn_unit +cpts_lifts_bi +cpts_lifts_sn +cpts_lref +cpt_sort +cpts_refl +cpts_sort +cpts_step_dx +cpts_step_sn +cpts_total_aaa +cpx +cpx_aaa_conf +cpx_aaa_conf_lpx +cpx_beta +cpx_bind +cpx_bind2 +cpx_bind_unit +cpx_cpxs +cpx_delta +cpx_delta_drops +cpx_ee +cpx_eps +cpx_ess +cpx_ext +cpx_flat +cpx_fsge_comp +cpx_fwd_bind1_minus +cpx_ind +cpx_inv_abbr1 +cpx_inv_abst1 +cpx_inv_appl1 +cpx_inv_appl1_simple +cpx_inv_atom1 +cpx_inv_atom1_drops +cpx_inv_bind1 +cpx_inv_cast1 +cpx_inv_flat1 +cpx_inv_gref1 +cpx_inv_lifts_bi +cpx_inv_lifts_sn +cpx_inv_lref1 +cpx_inv_lref1_bind +cpx_inv_lref1_drops +cpx_inv_sort1 +cpx_inv_zero1 +cpx_inv_zero1_pair +cpx_lifts_bi +cpx_lifts_sn +cpx_lref +cpx_pair_sn +cpx_refl +cpx_req_conf_sn +cpx_reqx_conf +cpx_reqx_conf_dx +cpx_reqx_conf_sn +cpx_rex_conf +cpxs +cpxs_aaa_conf +cpxs_beta +cpxs_beta_dx +cpxs_beta_rc +cpxs_bind +cpxs_bind2_dx +cpxs_bind_alt +cpxs_bind_dx +cpxs_cnx +cpxs_delta +cpxs_delta_drops +cpxs_ee +cpxs_eps +cpxs_ext +cpxs_flat +cpxs_flat_dx +cpxs_flat_sn +cpxs_fpbg_trans +cpxs_fpbs +cpxs_fpbs_trans +cpxs_fqup_fpbs +cpxs_fqus_fpbs +cpxs_fqus_lpxs_fpbs +cpxs_fwd_beta +cpxs_fwd_beta_vector +cpxs_fwd_cast +cpxs_fwd_cast_vector +cpxs_fwd_cnx +cpxs_fwd_cnx_vector +cpxs_fwd_delta_drops +cpxs_fwd_delta_drops_vector +cpxs_fwd_sort +cpxs_fwd_sort_vector +cpxs_fwd_theta +cpxs_fwd_theta_vector +cpxs_ind +cpxs_ind_dx +cpxs_inv_abbr1_dx +cpxs_inv_abst1 +cpxs_inv_appl1 +cpxs_inv_cast1 +cpxs_inv_cnx1 +cpxs_inv_lifts_bi +cpxs_inv_lifts_sn +cpxs_inv_lref1 +cpxs_inv_lref1_drops +cpxs_inv_sort1 +cpxs_inv_zero1 +cpxs_lifts_bi +cpxs_lifts_sn +cpxs_lref +cpxs_pair_sn +cpxs_refl +cpxs_reqx_conf +cpxs_reqx_conf_dx +cpxs_reqx_conf_sn +cpxs_sort +cpxs_strap1 +cpxs_strap2 +cpxs_teqx_fpbs +cpxs_teqx_fpbs_trans +cpxs_theta +cpxs_theta_dx +cpxs_theta_rc +cpxs_tneqx_fpbg +cpxs_tneqx_fwd_step_sn +cpxs_trans +cpx_subst +cpxs_zeta +cpxs_zeta_dx +cpx_teqx_conf +cpx_teqx_conf_rex +cpx_theta +cpx_zeta +csx +csx_abbr +csx_abst +csx_appl_beta +csx_appl_beta_aux +csx_appl_simple +csx_appl_simple_teqo +csx_appl_theta +csx_appl_theta_aux +csx_applv_beta +csx_applv_cast +csx_applv_cnx +csx_applv_delta_drops +csx_applv_sort +csx_applv_theta +csx_bind +csx_cast +csx_cpcs_dec +csx_cpxs_trans +csx_cpx_trans +csx_feqx_conf +csx_fpbq_conf +csx_fqu_conf +csx_fqup_conf +csx_fquq_conf +csx_fqus_conf +csx_fsb +csx_fsb_fpbs +csx_fwd_applv +csx_fwd_bind +csx_fwd_bind_dx +csx_fwd_bind_dx_aux +csx_fwd_bind_dx_unit +csx_fwd_bind_dx_unit_aux +csx_fwd_bind_unit +csx_fwd_flat +csx_fwd_flat_dx +csx_fwd_flat_dx_aux +csx_fwd_pair_sn +csx_fwd_pair_sn_aux +csx_gcp +csx_gcr +csx_ind +csx_ind_cpxs +csx_ind_cpxs_teqx +csx_ind_fpb +csx_ind_fpbg +csx_intro +csx_intro_cpxs +csx_inv_lifts +csx_inv_lref_drops +csx_inv_lref_pair_drops +csx_lifts +csx_lpx_conf +csx_lpxs_conf +csx_lref_pair_drops +csx_lsubr_conf +csx_reqx_conf +csx_reqx_trans +csx_rsx +csx_sort +csx_teqx_trans +csxv +csxv_inv_cons +drops_lprs_trans +drops_lpr_trans +drops_lpxs_trans +drops_lpx_trans +feqx_cpxs_trans +feqx_cpx_trans +feqx_fpbg_trans +feqx_fpbs +feqx_fpbs_trans +feqx_fpb_trans +feqx_lpxs_trans +fleq_rpx +fpb +fpb_cpx +fpb_fpbg +fpb_fpbg_trans +fpb_fpbq +fpb_fpbq_fneqx +fpb_fpbs +fpb_fqu +fpbg +fpbg_cpms_trans +fpbg_feqx_trans +fpbg_fpbq_trans +fpbg_fpbs_trans +fpbg_fqu_trans +fpbg_fwd_fpbs +fpbg_teqx_div +fpbg_trans +fpb_inv_feqx +fpb_lpx +fpbq +fpbq_aaa_conf +fpbq_cpx +fpbq_feqx +fpbq_fneqx_inv_fpb +fpbq_fpbg_trans +fpbq_fpbs +fpbq_fquq +fpbq_inv_fpb +fpbq_lpx +fpbq_refl +fpbs +fpbs_aaa_conf +fpbs_cpxs_teqx_fqup_lpx_trans +fpbs_cpxs_trans +fpbs_cpx_tneqx_trans +fpbs_csx_conf +fpbs_feqx_trans +fpbs_fpbg_trans +fpbs_fpb_trans +fpbs_fqup_trans +fpbs_fqus_trans +fpbs_ind +fpbs_ind_dx +fpbs_intro_star +fpbs_inv_fpbg +fpbs_inv_star +fpbs_lpxs_trans +fpbs_lpx_trans +fpbs_refl +fpbs_strap1 +fpbs_strap2 +fpbs_teqx_trans +fpbs_trans +fqu_cpr_trans_dx +fqu_cpr_trans_sn +fqu_cpxs_trans +fqu_cpxs_trans_tneqx +fqu_cpx_trans +fqu_cpx_trans_tneqx +fqu_lpr_trans +fqu_lpx_trans +fqup_cpms_fwd_fpbg +fqup_cpxs_trans +fqup_cpxs_trans_tneqx +fqup_cpx_trans +fqup_cpx_trans_tneqx +fqup_fpbg +fqup_fpbg_trans +fqup_fpbs +fqup_fpbs_trans +fquq_cpr_trans_dx +fquq_cpr_trans_sn +fquq_cpxs_trans +fquq_cpxs_trans_tneqx +fquq_cpx_trans +fquq_cpx_trans_tneqx +fquq_lpr_trans +fquq_lpx_trans +fqus_cpxs_trans +fqus_cpxs_trans_tneqx +fqus_cpx_trans +fqus_cpx_trans_tneqx +fqus_fpbs +fqus_fpbs_trans +fqus_lpxs_fpbs +fsb +fsb_feqx_trans +fsb_fpbg_refl_false +fsb_fpbs_trans +fsb_ind_alt +fsb_ind_fpbg +fsb_ind_fpbg_fpbs +fsb_intro +fsb_intro_fpbg +fsb_inv_csx +IH_cnv_cpm_conf_lpr +IH_cnv_cpms_conf_lpr +IH_cnv_cpms_strip_lpr +IH_cnv_cpms_trans_lpr +IH_cnv_cpm_teqx_conf_lpr +IH_cnv_cpm_teqx_cpm_trans +IH_cnv_cpm_trans_lpr +IH_cpr_conf_lpr +jsx +jsx_atom +jsx_bind +jsx_csx_conf +jsx_fwd_bind_sn +jsx_fwd_drops_atom_sn +jsx_fwd_drops_pair_sn +jsx_fwd_drops_unit_sn +jsx_fwd_lsubr +jsx_inv_atom_sn +jsx_inv_atom_sn_aux +jsx_inv_bind_sn +jsx_inv_bind_sn_aux +jsx_inv_pair_sn +jsx_inv_void_sn +jsx_pair +jsx_refl +jsx_trans +lfsx_atom +lpr +lpr_aaa_conf +lpr_bind +lpr_bind_refl_dx +lpr_conf +lpr_cpcs_conf +lpr_cpcs_trans +lpr_cpms_trans +lpr_cpm_trans +lpr_cpr_conf +lpr_cpr_conf_dx +lpr_cpr_conf_sn +lpr_cprs_conf +lpr_cprs_trans +lpr_cpr_trans +lpr_drops_conf +lpr_drops_trans +lpr_fpb +lpr_fpbq +lpr_fquq_trans +lpr_fqu_trans +lpr_fwd_length +lpr_fwd_lpx +lpr_inv_atom_dx +lpr_inv_atom_sn +lpr_inv_bind_dx +lpr_inv_bind_sn +lpr_inv_pair +lpr_inv_pair_dx +lpr_inv_pair_sn +lpr_inv_unit_dx +lpr_inv_unit_sn +lpr_lprs +lpr_pair +lpr_refl +lprs +lprs_aaa_conf +lprs_bind_refl_dx +lprs_conf +lprs_cpcs_trans +lprs_cpms_trans +lprs_cpm_trans +lprs_cpr_conf_dx +lprs_cpr_conf_sn +lprs_cprs_conf +lprs_cprs_conf_dx +lprs_cprs_conf_sn +lprs_CTC +lprs_drops_conf +lprs_drops_trans +lprs_fwd_length +lprs_fwd_lpxs +lprs_ind +lprs_ind_dx +lprs_ind_sn +lprs_inv_atom_dx +lprs_inv_atom_sn +lprs_inv_CTC +lprs_inv_pair_dx +lprs_inv_pair_sn +lprs_inv_TC +lprs_pair +lprs_pair_dx +lprs_refl +lprs_step_dx +lprs_step_sn +lprs_strip +lprs_TC +lprs_trans +lpx +lpx_aaa_conf +lpx_bind +lpx_bind_refl_dx +lpx_cpx_conf_fsge +lpx_cpxs_trans +lpx_cpx_trans +lpx_drops_conf +lpx_drops_trans +lpx_fqup_trans +lpx_fquq_trans +lpx_fqus_trans +lpx_fqu_trans +lpx_fsge_comp +lpx_fwd_length +lpx_inv_atom_dx +lpx_inv_atom_sn +lpx_inv_bind_dx +lpx_inv_bind_sn +lpx_inv_pair +lpx_inv_pair_dx +lpx_inv_pair_sn +lpx_inv_unit_dx +lpx_inv_unit_sn +lpx_lpxs +lpx_pair +lpx_refl +lpx_rpx +lpxs +lpxs_aaa_conf +lpxs_bind_refl_dx +lpxs_cpxs_trans +lpxs_cpx_trans +lpxs_drops_conf +lpxs_drops_trans +lpxs_feqx_fpbs +lpxs_fpbs +lpxs_fpbs_trans +lpxs_fwd_length +lpxs_ind +lpxs_ind_dx +lpxs_ind_sn +lpxs_inv_atom_dx +lpxs_inv_atom_sn +lpxs_inv_bind_sn +lpxs_inv_pair_dx +lpxs_inv_pair_sn +lpxs_pair +lpxs_pair_dx +lpxs_refl +lpxs_rneqx_fpbg +lpxs_rneqx_inv_step_sn +lpxs_step_dx +lpxs_step_sn +lpxs_trans +lsubr_cpcs_trans +lsubr_cpg_trans +lsubr_cpms_trans +lsubr_cpm_trans +lsubr_cpxs_trans +lsubr_cpx_trans +lsubsv_fwd_lsuba +lsubv +lsubv_atom +lsubv_beta +lsubv_bind +lsubv_cnv_trans +lsubv_cpcs_trans +lsubv_cpms_trans +lsubv_drops_conf_isuni +lsubv_drops_trans_isuni +lsubv_fwd_lsubr +lsubv_inv_abst_sn +lsubv_inv_atom_dx +lsubv_inv_atom_dx_aux +lsubv_inv_atom_sn +lsubv_inv_atom_sn_aux +lsubv_inv_bind_dx +lsubv_inv_bind_dx_aux +lsubv_inv_bind_sn +lsubv_inv_bind_sn_aux +lsubv_refl +lsubv_trans +nta +nta_abst_predicative +nta_abst_repellent +nta_appl +nta_appl_abst +nta_appl_ntas_pos +nta_appl_ntas_zero +nta_bind_cnv +nta_cast +nta_cast_old +nta_conv +nta_conv_cnv +nta_cpcs_bi +nta_cpcs_conf +nta_cpcs_conf_cnv +nta_cpr_conf +nta_cpr_conf_lpr +nta_cprs_conf +nta_cprs_trans +nta_fwd_aaa +nta_fwd_cnv_dx +nta_fwd_cnv_sn +nta_fwd_correct +nta_fwd_fsb +nta_ind_cnv +nta_ind_ext_cnv +nta_ind_ext_cnv_mixed +nta_ind_rest_cnv +nta_inference_dec +nta_inv_abst_bi_cnv +nta_inv_appl_sn +nta_inv_appl_sn_ntas +nta_inv_bind_sn_cnv +nta_inv_cast_sn +nta_inv_cast_sn_old +nta_inv_gref_sn +nta_inv_ldec_sn_cnv +nta_inv_ldef_sn +nta_inv_lifts_sn +nta_inv_lref_sn +nta_inv_lref_sn_drops_cnv +nta_inv_pure_sn_cnv +nta_inv_sort_sn +nta_ldec_cnv +nta_ldec_drops_cnv +nta_ldef +nta_ldef_drops +nta_lifts_bi +nta_lifts_sn +nta_lpr_conf +nta_lprs_conf +nta_lref +nta_mono +nta_ntas +nta_pure_cnv +ntas +ntas_bind_cnv +ntas_fwd_cnv_dx +ntas_fwd_cnv_sn +ntas_ind_bi_nta +ntas_intro +ntas_inv_appl_sn +ntas_inv_nta +ntas_inv_plus +ntas_inv_zero +nta_sort +ntas_refl +ntas_sort +ntas_step_dx +ntas_step_sn +ntas_trans +ntas_zero +nta_typecheck +nta_typecheck_dec +R_cpmuwe +R_cpmuwe_total_csx +req_cpx_trans +reqx_cpxs_trans +reqx_cpx_trans +reqx_fpb_trans +reqx_lpxs_trans +reqx_lpx_trans +reqx_rpx_trans +rpr_fsge_comp +rpx +rpx_atom +rpx_bind +rpx_bind_dx_split +rpx_bind_dx_split_void +rpx_bind_repl_dx +rpx_bind_void +rpx_cpx_conf +rpx_cpx_conf_fsge +rpx_cpx_conf_fsge_dx +rpx_flat +rpx_flat_dx_split +rpx_fsge_comp +rpx_fwd_bind_dx +rpx_fwd_bind_dx_void +rpx_fwd_flat_dx +rpx_fwd_length +rpx_fwd_pair_sn +rpx_gref +rpx_inv_atom_dx +rpx_inv_atom_sn +rpx_inv_bind +rpx_inv_bind_void +rpx_inv_flat +rpx_inv_gref +rpx_inv_gref_bind_dx +rpx_inv_gref_bind_sn +rpx_inv_lifts_bi +rpx_inv_lifts_dx +rpx_inv_lifts_sn +rpx_inv_lpx_req +rpx_inv_lref +rpx_inv_lref_bind_dx +rpx_inv_lref_bind_sn +rpx_inv_sort +rpx_inv_sort_bind_dx +rpx_inv_sort_bind_sn +rpx_inv_zero_length +rpx_inv_zero_pair_dx +rpx_inv_zero_pair_sn +rpx_lifts_sn +rpx_lref +rpx_pair +rpx_pair_refl +rpx_pair_sn_split +rpx_refl +rpx_reqx_conf +rpx_sort +rpx_teqx_conf +rpx_teqx_div +rsx +rsx_bind +rsx_bind_lpxs_aux +rsx_bind_lpxs_void_aux +rsx_bind_void +rsx_cpxs_trans +rsx_cpx_trans +rsx_cpx_trans_jsx +rsx_flat +rsx_flat_lpxs +rsx_fwd_bind_dx_void +rsx_fwd_flat_dx +rsx_fwd_lref_pair_csx +rsx_fwd_lref_pair_csx_aux +rsx_fwd_lref_pair_csx_drops +rsx_fwd_lref_pair_drops +rsx_fwd_pair +rsx_fwd_pair_aux +rsx_fwd_pair_sn +rsx_gref +rsx_ind +rsx_ind_lpxs +rsx_ind_lpxs_reqx +rsx_intro +rsx_intro_lpxs +rsx_inv_bind_void +rsx_inv_flat +rsx_inv_lifts +rsx_inv_lref_drops +rsx_inv_lref_pair +rsx_inv_lref_pair_drops +rsx_jsx_trans +rsx_lifts +rsx_lpxs_trans +rsx_lpx_trans +rsx_lref_atom_drops +rsx_lref_pair +rsx_lref_pair_drops +rsx_lref_pair_lpxs +rsx_lref_unit_drops +rsx_reqx_trans +rsx_sort +rsx_unit +teqx_cpxs_trans +teqx_cpx_trans +teqx_fpbs_trans +teqx_fpb_trans +teqx_reqx_lpx_fpbs