X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2FBasic_1.txt;h=54f20be57c3ff2f3fe6512917c421ada2e83fe73;hb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;hp=da672ace3d7a8075e790f770b914f6ed7e57aaad;hpb=720637242f8c46adef24da44f29129faa09469de;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
index da672ace3..54f20be57 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
@@ -76,19 +76,9 @@ csuba/getl csuba_getl_abbr_rev
 csuba/props csuba_refl
 csubc/arity csubc_arity_conf
 csubc/arity csubc_arity_trans
-csubc/clear csubc_clear_conf
 csubc/csuba csubc_csuba
 csubc/drop1 drop1_csubc_trans
-csubc/drop1 csubc_drop1_conf_rev
-csubc/drop csubc_drop_conf_O
 csubc/drop drop_csubc_trans
-csubc/drop csubc_drop_conf_rev
-csubc/fwd csubc_gen_sort_l
-csubc/fwd csubc_gen_head_l
-csubc/fwd csubc_gen_sort_r
-csubc/fwd csubc_gen_head_r
-csubc/getl csubc_getl_conf
-csubc/props csubc_refl
 csubt/clear csubt_clear_conf
 csubt/csuba csubt_csuba
 csubt/drop csubt_drop_flat
@@ -112,12 +102,7 @@ csubv/getl csubv_getl_conf
 csubv/getl csubv_getl_conf_void
 csubv/props csubv_bind_same
 csubv/props csubv_refl
-drop1/fwd drop1_gen_pnil
-drop1/fwd drop1_gen_pcons
-drop1/getl drop1_getl_trans
-drop1/props drop1_skip_bind
 drop1/props drop1_cons_tail
-drop1/props drop1_trans
 drop/props drop_ctail
 ex0/props aplus_gz_le
 ex0/props aplus_gz_ge
@@ -146,17 +131,19 @@ leq/props leq_sym
 leq/props leq_trans
 leq/props leq_ahead_false_1
 leq/props leq_ahead_false_2
-lift1/fwd lift1_sort
-lift1/fwd lift1_lref
-lift1/fwd lift1_bind
-lift1/fwd lift1_flat
 lift1/fwd lift1_cons_tail
+
+# check #############################################################
+
 lift1/fwd lifts1_flat
 lift1/fwd lifts1_nil
 lift1/fwd lifts1_cons
 lift1/props lift1_free
 lift/props thead_x_lift_y_y
 lift/props lifts_tapp
+
+# waiting ####################################################################
+
 lift/props lifts_inj
 llt/props lweight_repl
 llt/props llt_repl
@@ -170,6 +157,7 @@ next_plus/props next_plus_next
 next_plus/props next_plus_lt
 nf2/arity arity_nf2_inv_all
 nf2/dec nf2_dec
+
 nf2/fwd nf2_gen_lref
 nf2/fwd nf2_gen_abst
 nf2/fwd nf2_gen_cast
@@ -177,20 +165,15 @@ nf2/fwd nf2_gen_beta
 nf2/fwd nf2_gen_flat
 nf2/fwd nf2_gen__nf2_gen_aux
 nf2/fwd nf2_gen_abbr
+
 nf2/fwd nf2_gen_void
 nf2/iso nf2_iso_appls_lref
-nf2/lift1 nf2_lift1
 nf2/pr3 nf2_pr3_unfold
 nf2/pr3 nf2_pr3_confluence
-nf2/props nf2_sort
-nf2/props nf2_csort_lref
-nf2/props nf2_abst
-nf2/props nf2_abst_shift
+
 nf2/props nfs2_tapp
 nf2/props nf2_appls_lref
-nf2/props nf2_appl_lref
-nf2/props nf2_lref_abst
-nf2/props nf2_lift
+
 pc1/props pc1_pr0_r
 pc1/props pc1_pr0_x
 pc1/props pc1_refl
@@ -201,6 +184,7 @@ pc1/props pc1_head_2
 pc1/props pc1_t
 pc1/props pc1_pr0_u2
 pc1/props pc1_head
+
 pc3/dec pc3_dec
 pc3/dec pc3_abst_dec
 pc3/fsubst0 pc3_pr2_fsubst0
@@ -222,13 +206,11 @@ pc3/left pc3_ind_left
 pc3/nf2 pc3_nf2
 pc3/nf2 pc3_nf2_unfold
 pc3/pc1 pc3_pc1
-pc3/props clear_pc3_trans
 pc3/props pc3_pr2_r
 pc3/props pc3_pr2_x
 pc3/props pc3_pr3_r
 pc3/props pc3_pr3_x
 pc3/props pc3_pr3_t
-pc3/props pc3_refl
 pc3/props pc3_s
 pc3/props pc3_thin_dx
 pc3/props pc3_head_1
@@ -250,6 +232,9 @@ pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
 pc3/wcpr0 pc3_wcpr0_t
 pc3/wcpr0 pc3_wcpr0
 pr0/fwd pr0_gen_void
+
+# check #############################################################
+
 pr0/dec nf0_dec
 pr0/subst1 pr0_subst1_back
 pr0/subst1 pr0_subst1_fwd
@@ -265,17 +250,14 @@ pr2/clen pr2_gen_ctail
 pr2/fwd pr2_gen_void
 pr2/props pr2_ctail
 pr2/subst1 pr2_gen_cabbr
-pr3/fwd pr3_gen_sort
+
 pr3/fwd pr3_gen_abst
-pr3/fwd pr3_gen_cast
-pr3/fwd pr3_gen_lift
 pr3/fwd pr3_gen_lref
 pr3/fwd pr3_gen_void
 pr3/fwd pr3_gen_abbr
 pr3/fwd pr3_gen_appl
 pr3/fwd pr3_gen_bind
 pr3/iso pr3_iso_appls_abbr
-pr3/iso pr3_iso_appls_cast
 pr3/iso pr3_iso_appl_bind
 pr3/iso pr3_iso_appls_appl_bind
 pr3/iso pr3_iso_appls_bind
@@ -283,73 +265,35 @@ pr3/iso pr3_iso_beta
 pr3/iso pr3_iso_appls_beta
 pr3/pr1 pr3_pr1
 pr3/pr3 pr3_strip
-pr3/pr3 pr3_confluence
-pr3/props clear_pr3_trans
-pr3/props pr3_pr2
-pr3/props pr3_t
 pr3/props pr3_thin_dx
 pr3/props pr3_head_1
 pr3/props pr3_head_2
 pr3/props pr3_head_21
 pr3/props pr3_head_12
-pr3/props pr3_cflat
 pr3/props pr3_flat
-pr3/props pr3_pr0_pr2_t
-pr3/props pr3_pr2_pr2_t
-pr3/props pr3_pr2_pr3_t
 pr3/props pr3_pr3_pr3_t
-pr3/props pr3_lift
 pr3/props pr3_eta
 pr3/subst1 pr3_subst1
 pr3/subst1 pr3_gen_cabbr
 pr3/wcpr0 pr3_wcpr0_t
-sc3/arity sc3_arity_csubc
-sc3/arity sc3_arity
-sc3/props sc3_arity_gen
-sc3/props sc3_repl
-sc3/props sc3_lift
-sc3/props sc3_lift1
-sc3/props sc3_abbr
-sc3/props sc3_cast
-sc3/props sc3_props__sc3_sn3_abst
-sc3/props sc3_sn3
-sc3/props sc3_abst
-sc3/props sc3_bind
-sc3/props sc3_appl
-sn3/fwd sn3_gen_bind
-sn3/fwd sn3_gen_flat
-sn3/fwd sn3_gen_head
-sn3/fwd sn3_gen_cflat
-sn3/fwd sn3_gen_lift
-sn3/lift1 sns3_lifts1
-sn3/nf2 sn3_nf2
-sn3/nf2 nf2_sn3
-sn3/props sn3_pr3_trans
-sn3/props sn3_pr2_intro
-sn3/props sn3_cast
-sn3/props sn3_cflat
+sn3/props sn3_cpr3_trans
+
 sn3/props sn3_shift
 sn3/props sn3_change
 sn3/props sn3_gen_def
 sn3/props sn3_cdelta
-sn3/props sn3_cpr3_trans
-sn3/props sn3_bind
-sn3/props sn3_beta
 sn3/props sn3_appl_lref
 sn3/props sn3_appl_abbr
 sn3/props sn3_appl_cast
-sn3/props sn3_appl_bind
-sn3/props sn3_appl_appl
 sn3/props sn3_appl_beta
 sn3/props sn3_appl_appls
 sn3/props sn3_appls_lref
 sn3/props sn3_appls_cast
 sn3/props sn3_appls_bind
 sn3/props sn3_appls_beta
-sn3/props sn3_lift
-sn3/props sn3_abbr
 sn3/props sn3_appls_abbr
 sn3/props sns3_lifts
+
 sty0/fwd sty0_gen_sort
 sty0/fwd sty0_gen_lref
 sty0/fwd sty0_gen_bind