-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,s :
-t,u : local reference position level (de Bruijn's)
-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
-
-a: application
-b: binder
-d: abbreviation
-f: flat
-l: abstraction
-n: native type annotation
-
-NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
-
-- 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
-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: "big tree" reduction
-c: conversion
-d: decomposed extended reduction
-e: decomposed extended conversion
-n: reduction for "big tree" normal forms
-q: restricted reduction
-r: reduction
-s: substitution
-u: supclosure
-x: extended reduction
-
-- 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"
projects / helm.git / blobdiff