]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_1A/names.txt
update in lambdadelta
[helm.git] / matita / matita / contribs / lambdadelta / basic_1A / names.txt
diff --git a/matita/matita/contribs/lambdadelta/basic_1A/names.txt b/matita/matita/contribs/lambdadelta/basic_1A/names.txt
new file mode 100644 (file)
index 0000000..d85e059
--- /dev/null
@@ -0,0 +1,931 @@
+A
+Abbr
+Abst
+abst_dec
+AHead
+ahead_inj_snd
+aplus
+aplus_ahead_simpl
+aplus_asort_le_simpl
+aplus_asort_O_simpl
+aplus_asort_simpl
+aplus_assoc
+aplus_asucc
+aplus_asucc_false
+aplus_gz_ge
+aplus_gz_le
+aplus_inj
+aplus_reg_r
+aplus_sort_O_S_simpl
+aplus_sort_S_S_simpl
+app1
+Appl
+aprem
+aprem_asucc
+aprem_gen_head_O
+aprem_gen_head_S
+aprem_gen_sort
+aprem_repl
+aprem_succ
+aprem_zero
+arity
+arity_abbr
+arity_abst
+arity_appl
+arity_appls_abbr
+arity_appls_appl
+arity_appls_bind
+arity_appls_cast
+arity_aprem
+arity_bind
+arity_cast
+arity_cimp_conf
+arity_fsubst0
+arity_gen_abst
+arity_gen_appl
+arity_gen_appls
+arity_gen_bind
+arity_gen_cast
+arity_gen_cvoid
+arity_gen_cvoid_subst0
+arity_gen_lift
+arity_gen_lref
+arity_gen_sort
+arity_head
+arity_lift
+arity_lift1
+arity_mono
+arity_nf2_inv_all
+arity_repellent
+arity_repl
+arity_sort
+arity_sred_pr2
+arity_sred_pr3
+arity_sred_wcpr0_pr0
+arity_sred_wcpr0_pr1
+arity_subst0
+ASort
+asucc
+asucc_gen_head
+asucc_gen_sort
+asucc_inj
+asucc_repl
+B
+Bind
+bind_dec_not
+binder_dec
+C
+Cast
+cbk
+CHead
+chead_ctail
+cimp
+cimp_bind
+cimp_flat_dx
+cimp_flat_sx
+cimp_getl_conf
+cle
+clear
+clear_bind
+clear_cle
+clear_clear
+clear_ctail
+clear_flat
+clear_gen_all
+clear_gen_bind
+clear_gen_flat
+clear_gen_flat_r
+clear_gen_sort
+clear_getl_trans
+clear_mono
+clear_pc3_trans
+clear_pr2_trans
+clear_pr3_trans
+clear_trans
+clear_wf3_trans
+cle_flt_trans
+cle_head
+clen
+cle_r
+cle_trans_head
+clt
+clt_cong
+clt_head
+clt_thead
+clt_wf_ind
+clt_wf__q_ind
+cnt
+cnt_head
+cnt_lift
+cnt_sort
+CSort
+csuba
+csuba_abst
+csuba_arity
+csuba_arity_rev
+csuba_clear_conf
+csuba_clear_trans
+csuba_drop_abbr
+csuba_drop_abbr_rev
+csuba_drop_abst
+csuba_drop_abst_rev
+csuba_gen_abbr
+csuba_gen_abbr_rev
+csuba_gen_abst
+csuba_gen_abst_rev
+csuba_gen_bind
+csuba_gen_bind_rev
+csuba_gen_flat
+csuba_gen_flat_rev
+csuba_gen_void
+csuba_gen_void_rev
+csuba_getl_abbr
+csuba_getl_abbr_rev
+csuba_getl_abst
+csuba_getl_abst_rev
+csuba_head
+csuba_refl
+csuba_sort
+csuba_void
+csubc
+csubc_abst
+csubc_arity_conf
+csubc_arity_trans
+csubc_clear_conf
+csubc_csuba
+csubc_drop1_conf_rev
+csubc_drop_conf_O
+csubc_drop_conf_rev
+csubc_gen_head_l
+csubc_gen_head_r
+csubc_gen_sort_l
+csubc_gen_sort_r
+csubc_getl_conf
+csubc_head
+csubc_refl
+csubc_sort
+csubc_void
+csubst0
+csubst0_both
+csubst0_both_bind
+csubst0_clear_O
+csubst0_clear_O_back
+csubst0_clear_S
+csubst0_clear_trans
+csubst0_drop_eq
+csubst0_drop_eq_back
+csubst0_drop_gt
+csubst0_drop_gt_back
+csubst0_drop_lt
+csubst0_drop_lt_back
+csubst0_fst
+csubst0_fst_bind
+csubst0_gen_head
+csubst0_gen_S_bind_2
+csubst0_gen_sort
+csubst0_getl_ge
+csubst0_getl_ge_back
+csubst0_getl_lt
+csubst0_getl_lt_back
+csubst0_snd
+csubst0_snd_bind
+csubst1
+csubst1_bind
+csubst1_flat
+csubst1_gen_head
+csubst1_getl_ge
+csubst1_getl_ge_back
+csubst1_getl_lt
+csubst1_head
+csubst1_refl
+csubst1_sing
+csubt
+csubt_abst
+csubt_clear_conf
+csubt_csuba
+csubt_drop_abbr
+csubt_drop_abst
+csubt_drop_flat
+csubt_gen_abbr
+csubt_gen_abst
+csubt_gen_bind
+csubt_gen_flat
+csubt_getl_abbr
+csubt_getl_abst
+csubt_head
+csubt_pc3
+csubt_pr2
+csubt_refl
+csubt_sort
+csubt_ty3
+csubt_ty3_ld
+csubt_void
+csubv
+csubv_bind
+csubv_bind_same
+csubv_clear_conf
+csubv_clear_conf_void
+csubv_drop_conf
+csubv_flat
+csubv_getl_conf
+csubv_getl_conf_void
+csubv_refl
+csubv_sort
+csubv_void
+CTail
+c_tail_ind
+cweight
+dnf_dec
+dnf_dec2
+drop
+drop1
+drop1_cons
+drop1_cons_tail
+drop1_csubc_trans
+drop1_gen_pcons
+drop1_gen_pnil
+drop1_getl_trans
+drop1_nil
+drop1_skip_bind
+drop1_trans
+drop_clear
+drop_clear_O
+drop_clear_S
+drop_conf_ge
+drop_conf_lt
+drop_conf_rev
+drop_csubc_trans
+drop_ctail
+drop_drop
+drop_gen_drop
+drop_gen_refl
+drop_gen_skip_l
+drop_gen_skip_r
+drop_gen_sort
+drop_getl_trans_ge
+drop_getl_trans_le
+drop_getl_trans_lt
+drop_mono
+drop_refl
+drop_S
+drop_skip
+drop_skip_bind
+drop_skip_flat
+drop_trans_ge
+drop_trans_le
+ex1_arity
+ex1_c
+ex1__leq_sort_SS
+ex1_t
+ex1_ty3
+ex2_arity
+ex2_c
+ex2_nf2
+ex2_t
+F
+Flat
+flt
+flt_arith0
+flt_arith1
+flt_arith2
+flt_shift
+flt_thead_dx
+flt_thead_sx
+flt_trans
+flt_wf_ind
+flt_wf__q_ind
+fsubst0
+fsubst0_both
+fsubst0_fst
+fsubst0_gen_base
+fsubst0_snd
+fweight
+G
+getl
+getl_clear_bind
+getl_clear_conf
+getl_clear_trans
+getl_conf_ge_drop
+getl_conf_le
+getl_csubst1
+getl_ctail
+getl_ctail_clen
+getl_dec
+getl_drop
+getl_drop_conf_ge
+getl_drop_conf_lt
+getl_drop_conf_rev
+getl_drop_trans
+getl_flat
+getl_flt
+getl_gen_2
+getl_gen_all
+getl_gen_bind
+getl_gen_flat
+getl_gen_O
+getl_gen_S
+getl_gen_sort
+getl_gen_tail
+getl_head
+getl_intro
+getl_mono
+getl_refl
+getl_trans
+getl_wf3_trans
+gz
+iso
+iso_flats_flat_bind_false
+iso_flats_lref_bind_false
+iso_gen_head
+iso_gen_lref
+iso_gen_sort
+iso_head
+iso_lref
+iso_refl
+iso_sort
+iso_trans
+K
+leq
+leq_ahead_asucc_false
+leq_ahead_false_1
+leq_ahead_false_2
+leq_asucc
+leq_asucc_false
+leq_eq
+leq_gen_head1
+leq_gen_head2
+leq_gen_sort1
+leq_gen_sort2
+leq_head
+leq_leqz
+leq_refl
+leq_sort
+leq_sym
+leq_trans
+leqz
+leqz_head
+leqz_leq
+leqz_sort
+lift
+lift1
+lift1_bind
+lift1_cons_tail
+lift1_flat
+lift1_free
+lift1_lift1
+lift1_lref
+lift1_sort
+lift1_xhg
+lift_bind
+lift_d
+lift_flat
+lift_free
+lift_free_sym
+lift_gen_bind
+lift_gen_flat
+lift_gen_head
+lift_gen_lift
+lift_gen_lref
+lift_gen_lref_false
+lift_gen_lref_ge
+lift_gen_lref_lt
+lift_gen_sort
+lift_head
+lift_inj
+lift_lref_ge
+lift_lref_gt
+lift_lref_lt
+lift_r
+lifts
+lifts1
+lifts1_cons
+lifts1_flat
+lifts1_nil
+lifts1_xhg
+lifts_inj
+lift_sort
+lifts_tapp
+lift_tle
+lift_tlt_dx
+lift_weight
+lift_weight_add
+lift_weight_add_O
+lift_weight_map
+llt
+llt_head_dx
+llt_head_sx
+llt_repl
+llt_trans
+llt_wf_ind
+llt_wf__q_ind
+lref_map
+lweight
+lweight_repl
+minus_s_s
+mk_G
+next_plus
+next_plus_assoc
+next_plus_gz
+next_plus_lt
+next_plus_next
+nf0_dec
+nf2
+nf2_abst
+nf2_abst_shift
+nf2_appl_lref
+nf2_appls_lref
+nf2_csort_lref
+nf2_dec
+nf2_gen_abbr
+nf2_gen_abst
+nf2_gen_beta
+nf2_gen_cast
+nf2_gen_flat
+nf2_gen_lref
+nf2_gen__nf2_gen_aux
+nf2_gen_void
+nf2_iso_appls_lref
+nf2_lift
+nf2_lift1
+nf2_lref_abst
+nf2_pr3_confluence
+nf2_pr3_unfold
+nf2_sn3
+nf2_sort
+nfs2
+nfs2_tapp
+node_inh
+not_abbr_abst
+not_abbr_void
+not_abst_void
+not_void_abst
+pc1
+pc1_head
+pc1_head_1
+pc1_head_2
+pc1_pr0_r
+pc1_pr0_u
+pc1_pr0_u2
+pc1_pr0_x
+pc1_refl
+pc1_s
+pc1_t
+pc3
+pc3_abst_dec
+pc3_dec
+pc3_eta
+pc3_fsubst0
+pc3_gen_abst
+pc3_gen_abst_shift
+pc3_gen_appls_lref_abst
+pc3_gen_appls_lref_sort
+pc3_gen_appls_sort_abst
+pc3_gen_cabbr
+pc3_gen_lift
+pc3_gen_lift_abst
+pc3_gen_not_abst
+pc3_gen_sort
+pc3_gen_sort_abst
+pc3_head_1
+pc3_head_12
+pc3_head_2
+pc3_head_21
+pc3_ind_left
+pc3_ind_left__pc3_left_pc3
+pc3_ind_left__pc3_left_pr3
+pc3_ind_left__pc3_left_sym
+pc3_ind_left__pc3_left_trans
+pc3_ind_left__pc3_pc3_left
+pc3_left
+pc3_left_r
+pc3_left_ur
+pc3_left_ux
+pc3_lift
+pc3_nf2
+pc3_nf2_unfold
+pc3_pc1
+pc3_pr0_pr2_t
+pc3_pr2_fsubst0
+pc3_pr2_fsubst0_back
+pc3_pr2_pr2_t
+pc3_pr2_pr3_t
+pc3_pr2_r
+pc3_pr2_u
+pc3_pr2_u2
+pc3_pr2_x
+pc3_pr3_conf
+pc3_pr3_pc3_t
+pc3_pr3_r
+pc3_pr3_t
+pc3_pr3_x
+pc3_refl
+pc3_s
+pc3_t
+pc3_thin_dx
+pc3_wcpr0
+pc3_wcpr0__pc3_wcpr0_t_aux
+pc3_wcpr0_t
+pr0
+pr0_beta
+pr0_comp
+pr0_confluence
+pr0_confluence__pr0_cong_delta
+pr0_confluence__pr0_cong_upsilon_cong
+pr0_confluence__pr0_cong_upsilon_delta
+pr0_confluence__pr0_cong_upsilon_refl
+pr0_confluence__pr0_cong_upsilon_zeta
+pr0_confluence__pr0_delta_delta
+pr0_confluence__pr0_delta_tau
+pr0_confluence__pr0_upsilon_upsilon
+pr0_delta
+pr0_delta1
+pr0_gen_abbr
+pr0_gen_abst
+pr0_gen_appl
+pr0_gen_cast
+pr0_gen_lift
+pr0_gen_lref
+pr0_gen_sort
+pr0_gen_void
+pr0_lift
+pr0_refl
+pr0_subst0
+pr0_subst0_back
+pr0_subst0_fwd
+pr0_subst1
+pr0_subst1_back
+pr0_subst1_fwd
+pr0_tau
+pr0_upsilon
+pr0_zeta
+pr1
+pr1_comp
+pr1_confluence
+pr1_eta
+pr1_head_1
+pr1_head_2
+pr1_pr0
+pr1_refl
+pr1_sing
+pr1_strip
+pr1_t
+pr2
+pr2_cflat
+pr2_change
+pr2_confluence
+pr2_confluence__pr2_delta_delta
+pr2_confluence__pr2_free_delta
+pr2_confluence__pr2_free_free
+pr2_ctail
+pr2_delta
+pr2_delta1
+pr2_free
+pr2_gen_abbr
+pr2_gen_abst
+pr2_gen_appl
+pr2_gen_cabbr
+pr2_gen_cast
+pr2_gen_cbind
+pr2_gen_cflat
+pr2_gen_csort
+pr2_gen_ctail
+pr2_gen_lift
+pr2_gen_lref
+pr2_gen_sort
+pr2_gen_void
+pr2_head_1
+pr2_head_2
+pr2_lift
+pr2_subst1
+pr2_thin_dx
+pr3
+pr3_cflat
+pr3_confluence
+pr3_eta
+pr3_flat
+pr3_gen_abbr
+pr3_gen_abst
+pr3_gen_appl
+pr3_gen_bind
+pr3_gen_cabbr
+pr3_gen_cast
+pr3_gen_lift
+pr3_gen_lref
+pr3_gen_sort
+pr3_gen_void
+pr3_head_1
+pr3_head_12
+pr3_head_2
+pr3_head_21
+pr3_iso_appl_bind
+pr3_iso_appls_abbr
+pr3_iso_appls_appl_bind
+pr3_iso_appls_beta
+pr3_iso_appls_bind
+pr3_iso_appls_cast
+pr3_iso_beta
+pr3_lift
+pr3_pr0_pr2_t
+pr3_pr1
+pr3_pr2
+pr3_pr2_pr2_t
+pr3_pr2_pr3_t
+pr3_pr3_pr3_t
+pr3_refl
+pr3_sing
+pr3_strip
+pr3_subst1
+pr3_t
+pr3_thin_dx
+pr3_wcpr0_t
+ptrans
+r
+r_arith0
+r_arith1
+r_arith2
+r_arith3
+r_arith4
+r_arith5
+r_arith6
+r_arith7
+r_dis
+r_minus
+r_plus
+r_plus_sym
+r_S
+s
+s_arith0
+s_arith1
+sc3
+sc3_abbr
+sc3_abst
+sc3_appl
+sc3_arity
+sc3_arity_csubc
+sc3_arity_gen
+sc3_bind
+sc3_cast
+sc3_lift
+sc3_lift1
+sc3_props__sc3_sn3_abst
+sc3_repl
+sc3_sn3
+s_inc
+s_inj
+s_le
+s_le_gen
+s_lt
+s_lt_gen
+s_minus
+sn3
+sn3_abbr
+sn3_appl_abbr
+sn3_appl_appl
+sn3_appl_appls
+sn3_appl_beta
+sn3_appl_bind
+sn3_appl_cast
+sn3_appl_lref
+sn3_appls_abbr
+sn3_appls_beta
+sn3_appls_bind
+sn3_appls_cast
+sn3_appls_lref
+sn3_beta
+sn3_bind
+sn3_cast
+sn3_cdelta
+sn3_cflat
+sn3_change
+sn3_cpr3_trans
+sn3_gen_bind
+sn3_gen_cflat
+sn3_gen_def
+sn3_gen_flat
+sn3_gen_head
+sn3_gen_lift
+sn3_lift
+sn3_nf2
+sn3_pr2_intro
+sn3_pr3_trans
+sn3_shift
+sn3_sing
+sns3
+sns3_lifts
+sns3_lifts1
+s_plus
+s_plus_sym
+s_r
+s_S
+sty0
+sty0_abbr
+sty0_abst
+sty0_appl
+sty0_bind
+sty0_cast
+sty0_correct
+sty0_gen_appl
+sty0_gen_bind
+sty0_gen_cast
+sty0_gen_lref
+sty0_gen_sort
+sty0_lift
+sty0_sort
+sty1
+sty1_abbr
+sty1_appl
+sty1_bind
+sty1_cast2
+sty1_cnt
+sty1_correct
+sty1_lift
+sty1_sing
+sty1_sty0
+sty1_trans
+subst
+subst0
+subst0_both
+subst0_confluence_eq
+subst0_confluence_lift
+subst0_confluence_neq
+subst0_fst
+subst0_gen_head
+subst0_gen_lift_false
+subst0_gen_lift_ge
+subst0_gen_lift_lt
+subst0_gen_lift_rev_ge
+subst0_gen_lref
+subst0_gen_sort
+subst0_lift_ge
+subst0_lift_ge_s
+subst0_lift_ge_S
+subst0_lift_lt
+subst0_lref
+subst0_refl
+subst0_snd
+subst0_subst0
+subst0_subst0_back
+subst0_tlt
+subst0_tlt_head
+subst0_trans
+subst0_weight_le
+subst0_weight_lt
+subst1
+subst1_confluence_eq
+subst1_confluence_lift
+subst1_confluence_neq
+subst1_ex
+subst1_gen_head
+subst1_gen_lift_eq
+subst1_gen_lift_ge
+subst1_gen_lift_lt
+subst1_gen_lref
+subst1_gen_sort
+subst1_head
+subst1_lift_ge
+subst1_lift_lt
+subst1_lift_S
+subst1_refl
+subst1_single
+subst1_subst1
+subst1_subst1_back
+subst1_trans
+subst_head
+subst_lift_SO
+subst_lref_eq
+subst_lref_gt
+subst_lref_lt
+subst_sort
+subst_subst0
+T
+TApp
+TCons
+tcons_tapp_ex
+term_dec
+terms_props__bind_dec
+terms_props__flat_dec
+terms_props__kind_dec
+THead
+THeads
+theads_tapp
+thead_x_lift_y_y
+thead_x_y_y
+tle
+tle_r
+TList
+tlist_ind_rev
+TLRef
+tlt
+tlt_head_dx
+tlt_head_sx
+tlt_trans
+tlt_wf_ind
+tlt_wf__q_ind
+TNil
+trans
+tslen
+tslt
+tslt_wf_ind
+tslt_wf__q_ind
+TSort
+tweight
+tweight_lt
+ty3
+ty3_abbr
+ty3_abst
+ty3_acyclic
+ty3_appl
+ty3_arity
+ty3_bind
+ty3_cast
+ty3_conv
+ty3_correct
+ty3_cred_pr2
+ty3_cred_pr3
+ty3_csubst0
+ty3_fsubst0
+ty3_gen_abst_abst
+ty3_gen_appl
+ty3_gen_appl_nf2
+ty3_gen_bind
+ty3_gen_cabbr
+ty3_gen_cast
+ty3_gen_cvoid
+ty3_gen_lift
+ty3_gen_lref
+ty3_gen_sort
+ty3_getl_subst0
+ty3_inference
+ty3_inv_appls_lref_nf2
+ty3_inv_lref_lref_nf2
+ty3_inv_lref_nf2
+ty3_inv_lref_nf2_pc3
+ty3_lift
+ty3_nf2_gen__ty3_nf2_inv_abst_aux
+ty3_nf2_inv_abst
+ty3_nf2_inv_abst_premise
+ty3_nf2_inv_abst_premise_csort
+ty3_nf2_inv_all
+ty3_nf2_inv_sort
+ty3_predicative
+ty3_repellent
+ty3_sconv
+ty3_sconv_pc3
+ty3_shift1
+ty3_sn3
+ty3_sort
+ty3_sred_back
+ty3_sred_pr0
+ty3_sred_pr1
+ty3_sred_pr2
+ty3_sred_pr3
+ty3_sred_wcpr0_pr0
+ty3_sty0
+ty3_subst0
+ty3_tred
+ty3_typecheck
+ty3_unique
+tys3
+tys3_cons
+tys3_gen_cons
+tys3_gen_nil
+tys3_nil
+Void
+wadd
+wadd_le
+wadd_lt
+wadd_O
+wcpr0
+wcpr0_comp
+wcpr0_drop
+wcpr0_drop_back
+wcpr0_gen_head
+wcpr0_gen_sort
+wcpr0_getl
+wcpr0_getl_back
+wcpr0_refl
+weight
+weight_add_O
+weight_add_S
+weight_eq
+weight_le
+weight_map
+wf3
+wf3_bind
+wf3_clear_conf
+wf3_flat
+wf3_gen_bind1
+wf3_gen_flat1
+wf3_gen_head2
+wf3_gen_sort1
+wf3_getl_conf
+wf3_idem
+wf3_mono
+wf3_pc3_conf
+wf3_pr2_conf
+wf3_pr3_conf
+wf3_sort
+wf3_total
+wf3_ty3
+wf3_ty3_conf
+wf3_void