-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
projects / helm.git / blobdiff