X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fbasic_1.txt;h=544232544fbe7a7bfafc5db1005da0365e3738c1;hb=ea83c19f4cac864dd87eb059d8aeb2343eba480f;hp=5370377e61f77a679460b2d8278829b6927a56ce;hpb=bbac36729dab046d61019081c1523af06d876103;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 5370377e6..544232544 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -47,9 +47,7 @@ asucc/fwd asucc_gen_head cnt/props cnt_lift C/props clt_wf__q_ind C/props clt_wf_ind -C/props chead_ctail -C/props clt_thead (ctail) -C/props c_tail_ind + csuba/arity csuba_arity csuba/arity csuba_arity_rev csuba/arity arity_appls_appl @@ -74,27 +72,16 @@ csuba/getl csuba_getl_abst csuba/getl csuba_getl_abst_rev csuba/getl csuba_getl_abbr_rev csuba/props csuba_refl + csubc/arity csubc_arity_conf csubc/arity csubc_arity_trans -csubc/csuba csubc_csuba csubc/drop1 drop1_csubc_trans csubc/drop drop_csubc_trans -csubt/clear csubt_clear_conf + csubt/csuba csubt_csuba -csubt/drop csubt_drop_flat -csubt/drop csubt_drop_abbr -csubt/drop csubt_drop_abst csubt/fwd csubt_gen_abbr csubt/fwd csubt_gen_abst -csubt/fwd csubt_gen_flat -csubt/fwd csubt_gen_bind -csubt/getl csubt_getl_abbr -csubt/getl csubt_getl_abst -csubt/pc3 csubt_pr2 -csubt/pc3 csubt_pc3 -csubt/props csubt_refl -csubt/ty3 csubt_ty3 -csubt/ty3 csubt_ty3_ld + csubv/clear csubv_clear_conf csubv/clear csubv_clear_conf_void csubv/drop csubv_drop_conf @@ -103,7 +90,6 @@ csubv/getl csubv_getl_conf_void csubv/props csubv_bind_same csubv/props csubv_refl drop1/props drop1_cons_tail -drop/props drop_ctail ex0/props aplus_gz_le ex0/props aplus_gz_ge ex0/props next_plus_gz @@ -114,7 +100,6 @@ ex1/props ex1_arity ex1/props ex1_ty3 ex2/props ex2_nf2 ex2/props ex2_arity -fsubst0/fwd fsubst0_gen_base leq/asucc asucc_repl leq/asucc asucc_inj leq/asucc leq_asucc @@ -132,18 +117,10 @@ leq/props leq_trans leq/props leq_ahead_false_1 leq/props leq_ahead_false_2 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 @@ -156,8 +133,6 @@ next_plus/props next_plus_assoc 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 @@ -165,15 +140,9 @@ 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/pr3 nf2_pr3_unfold -nf2/pr3 nf2_pr3_confluence - nf2/props nfs2_tapp nf2/props nf2_appls_lref - pc1/props pc1_pr0_r pc1/props pc1_pr0_x pc1/props pc1_refl @@ -187,54 +156,17 @@ pc1/props pc1_head pc3/dec pc3_dec pc3/dec pc3_abst_dec -pc3/fsubst0 pc3_pr2_fsubst0 -pc3/fsubst0 pc3_pr2_fsubst0_back -pc3/fsubst0 pc3_fsubst0 -pc3/fwd pc3_gen_sort -pc3/fwd pc3_gen_abst -pc3/fwd pc3_gen_abst_shift -pc3/fwd pc3_gen_lift pc3/fwd pc3_gen_not_abst pc3/fwd pc3_gen_lift_abst -pc3/fwd pc3_gen_sort_abst -pc3/left pc3_ind_left__pc3_left_pr3 -pc3/left pc3_ind_left__pc3_left_trans -pc3/left pc3_ind_left__pc3_left_sym -pc3/left pc3_ind_left__pc3_left_pc3 -pc3/left pc3_ind_left__pc3_pc3_left -pc3/left pc3_ind_left pc3/nf2 pc3_nf2 pc3/nf2 pc3_nf2_unfold pc3/pc1 pc3_pc1 -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_s -pc3/props pc3_thin_dx -pc3/props pc3_head_1 -pc3/props pc3_head_2 -pc3/props pc3_pr2_u -pc3/props pc3_t -pc3/props pc3_pr2_u2 -pc3/props pc3_pr3_conf -pc3/props pc3_head_12 -pc3/props pc3_head_21 -pc3/props pc3_pr0_pr2_t pc3/props pc3_pr2_pr2_t pc3/props pc3_pr2_pr3_t pc3/props pc3_pr3_pc3_t -pc3/props pc3_lift pc3/props pc3_eta -pc3/subst1 pc3_gen_cabbr -pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux -pc3/wcpr0 pc3_wcpr0_t -pc3/wcpr0 pc3_wcpr0 -pr0/fwd pr0_gen_void - -# check ############################################################# +pr0/fwd pr0_gen_void pr0/dec nf0_dec pr0/subst1 pr0_subst1_back pr0/subst1 pr0_subst1_fwd @@ -246,39 +178,11 @@ pr1/props pr1_head_1 pr1/props pr1_head_2 pr1/props pr1_comp pr1/props pr1_eta -pr2/clen pr2_gen_ctail pr2/fwd pr2_gen_void -pr2/props pr2_ctail -pr2/subst1 pr2_gen_cabbr pr3/fwd pr3_gen_void pr3/pr1 pr3_pr1 - -pr3/pr3 pr3_strip -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_eta -pr3/subst1 pr3_subst1 -pr3/subst1 pr3_gen_cabbr -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_appl_appls -sn3/props sn3_appls_lref sn3/props sns3_lifts - -sty0/fwd sty0_gen_sort -sty0/fwd sty0_gen_lref -sty0/fwd sty0_gen_bind -sty0/fwd sty0_gen_appl -sty0/fwd sty0_gen_cast -sty0/props sty0_lift -sty0/props sty0_correct sty1/cnt sty1_cnt sty1/props sty1_trans sty1/props sty1_bind @@ -307,14 +211,7 @@ ty3/arity_props ty3_repellent ty3/arity_props ty3_acyclic ty3/arity_props ty3_sn3 ty3/dec ty3_inference -ty3/fsubst0 ty3_fsubst0 -ty3/fsubst0 ty3_csubst0 -ty3/fsubst0 ty3_subst0 -ty3/fwd ty3_gen_sort -ty3/fwd ty3_gen_lref -ty3/fwd ty3_gen_bind ty3/fwd ty3_gen_appl -ty3/fwd ty3_gen_cast ty3/fwd tys3_gen_nil ty3/fwd tys3_gen_cons ty3/fwd_nf2 ty3_gen_appl_nf2 @@ -339,15 +236,10 @@ ty3/pr3_props ty3_tred ty3/pr3_props ty3_sconv_pc3 ty3/pr3_props ty3_sred_back ty3/pr3_props ty3_sconv -ty3/props ty3_lift -ty3/props ty3_correct -ty3/props ty3_unique ty3/props ty3_gen_abst_abst -ty3/props ty3_typecheck -ty3/props ty3_getl_subst0 ty3/sty0 ty3_sty0 -ty3/subst1 ty3_gen_cabbr ty3/subst1 ty3_gen_cvoid + wf3/clear wf3_clear_conf wf3/clear clear_wf3_trans wf3/fwd wf3_gen_sort1