X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fnames.txt;h=b0dd49768d6369c1ecc97391a424b25f2a99b75e;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hp=9a3319f5ca8d09b8ff0f44a78a3189451b3f3593;hpb=cf10254638dab42421a9281a9418001d9bdbc8c0;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 9a3319f5c..b0dd49768 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -1,98 +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,Q : -R : generic predicate (relation) -S : RTM stack -T,U,V,W: term -X,Y,Z : reserved: transient objet denoted by a capital letter - -a,b : binder polarity -c : reserved: future use (\lambda\delta 3) -d : relocation depth -e : relocation height -f : -g : sort degree parameter -h : sort hierarchy parameter -i,j : local reference position index (de Bruijn's) -k : sort index -l : term degree -m,n : reserved: future use -o : -p,q : global reference position -r : reduction kind parameter (true = ordinary, false = extended) -s : local dropping kind parameter (true = general, false = restricted) -t,u : local reference position level (de Bruijn's) (RTM) -v,w : -x,y,z : reserved: transient objet denoted by a small letter - -NAMING CONVENTIONS FOR CONSTRUCTORS - -0: atomic -2: binary - -A: application to vector -F: boolean false -T: boolean true - -a: application -b: binder -d: abbreviation -f: flat -l: abstraction -n: native type annotation - -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 - -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 -q: restricted reduction -r: reduction -s: substitution -u: supclosure -w: reserved for generic pointwise extension -x: rt-reduction -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) -x: reserved for generic pointwise extension +"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"