From: Ferruccio Guidi Date: Tue, 11 Oct 2011 17:27:11 +0000 (+0000) Subject: - cpr_lsubs_conf proved! (was pr2_change) X-Git-Tag: make_still_working~2209 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b0dce88ff4c55b5f811ce9e183418479f7d34d2a;p=helm.git - cpr_lsubs_conf proved! (was pr2_change) - some "-" removed :) --- diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic-1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic-1.txt deleted file mode 100644 index b45870449..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic-1.txt +++ /dev/null @@ -1,468 +0,0 @@ -# waiting #################################################################### - -aplus/props aplus_reg_r -aplus/props aplus_assoc -aplus/props aplus_asucc -aplus/props aplus_sort_O_S_simpl -aplus/props aplus_sort_S_S_simpl -aplus/props aplus_asort_O_simpl -aplus/props aplus_asort_le_simpl -aplus/props aplus_asort_simpl -aplus/props aplus_ahead_simpl -aplus/props aplus_asucc_false -aplus/props aplus_inj -aprem/fwd aprem_gen_sort -aprem/fwd aprem_gen_head_O -aprem/fwd aprem_gen_head_S -aprem/props aprem_repl -aprem/props aprem_asucc -arity/aprem arity_aprem -arity/cimp arity_cimp_conf -arity/fwd arity_gen_sort -arity/fwd arity_gen_lref -arity/fwd arity_gen_bind -arity/fwd arity_gen_abst -arity/fwd arity_gen_appl -arity/fwd arity_gen_cast -arity/fwd arity_gen_appls -arity/fwd arity_gen_lift -arity/lift1 arity_lift1 -arity/pr3 arity_sred_wcpr0_pr0 -arity/pr3 arity_sred_wcpr0_pr1 -arity/pr3 arity_sred_pr2 -arity/pr3 arity_sred_pr3 -arity/props node_inh -arity/props arity_lift -arity/props arity_mono -arity/props arity_repellent -arity/props arity_appls_cast -arity/props arity_appls_abbr -arity/props arity_appls_bind -arity/subst0 arity_gen_cvoid_subst0 -arity/subst0 arity_gen_cvoid -arity/subst0 arity_fsubst0 -arity/subst0 arity_subst0 -asucc/fwd asucc_gen_sort -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 -csuba/clear csuba_clear_conf -csuba/clear csuba_clear_trans -csuba/drop csuba_drop_abbr -csuba/drop csuba_drop_abst -csuba/drop csuba_drop_abst_rev -csuba/drop csuba_drop_abbr_rev -csuba/fwd csuba_gen_abbr -csuba/fwd csuba_gen_void -csuba/fwd csuba_gen_abst -csuba/fwd csuba_gen_flat -csuba/fwd csuba_gen_bind -csuba/fwd csuba_gen_abst_rev -csuba/fwd csuba_gen_void_rev -csuba/fwd csuba_gen_abbr_rev -csuba/fwd csuba_gen_flat_rev -csuba/fwd csuba_gen_bind_rev -csuba/getl csuba_getl_abbr -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/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 -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 -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 -ex0/props next_plus_gz -ex0/props leqz_leq -ex0/props leq_leqz -ex1/props ex1__leq_sort_SS -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 -leq/asucc leq_ahead_asucc_false -leq/asucc leq_asucc_false -leq/fwd leq_gen_sort1 -leq/fwd leq_gen_head1 -leq/fwd leq_gen_sort2 -leq/fwd leq_gen_head2 -leq/props ahead_inj_snd -leq/props leq_refl -leq/props leq_eq -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 -lift1/fwd lifts1_flat -lift1/fwd lifts1_nil -lift1/fwd lifts1_cons -lift1/props lift1_lift1 -lift1/props lift1_xhg -lift1/props lifts1_xhg -lift1/props lift1_free -lift/props thead_x_lift_y_y -lift/props lifts_tapp -lift/props lifts_inj -llt/props lweight_repl -llt/props llt_repl -llt/props llt_trans -llt/props llt_head_sx -llt/props llt_head_dx -llt/props llt_wf__q_ind -llt/props llt_wf_ind -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 -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 -pc1/props pc1_pr0_u -pc1/props pc1_s -pc1/props pc1_head_1 -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 -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 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 -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 -pr0/dec nf0_dec -pr0/subst1 pr0_subst1_back -pr0/subst1 pr0_subst1_fwd -pr1/pr1 pr1_strip -pr1/pr1 pr1_confluence -pr1/props pr1_pr0 -pr1/props pr1_t -pr1/props pr1_head_1 -pr1/props pr1_head_2 -pr1/props pr1_comp -pr1/props pr1_eta -pr2/clen pr2_gen_ctail - -# check ###################################################################### - -pr2/fwd pr2_gen_void -pr2/props pr2_ctail - - -# waiting #################################################################### - -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 -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_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 -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 -sty1/props sty1_appl -sty1/props sty1_lift -sty1/props sty1_correct -sty1/props sty1_abbr -sty1/props sty1_cast2 -subst0/dec dnf_dec2 -subst0/dec dnf_dec -subst1/props subst1_ex -subst/fwd subst_sort -subst/fwd subst_lref_lt -subst/fwd subst_lref_eq -subst/fwd subst_lref_gt -subst/fwd subst_head -subst/props subst_lift_SO -subst/props subst_subst0 -T/dec terms_props__bind_dec -T/dec bind_dec_not -T/dec terms_props__flat_dec -T/dec terms_props__kind_dec -T/dec term_dec -T/dec binder_dec -T/dec abst_dec -tlist/props tslt_wf__q_ind -tlist/props tslt_wf_ind -tlist/props theads_tapp -tlist/props tcons_tapp_ex -tlist/props tlist_ind_rev -T/props not_abbr_abst -T/props not_void_abst -T/props not_abbr_void -T/props not_abst_void -T/props thead_x_y_y -T/props tweight_lt -ty3/arity ty3_arity -ty3/arity_props ty3_predicative -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 -ty3/fwd_nf2 ty3_inv_lref_nf2_pc3 -ty3/fwd_nf2 ty3_inv_lref_nf2 -ty3/fwd_nf2 ty3_inv_appls_lref_nf2 -ty3/fwd_nf2 ty3_inv_lref_lref_nf2 -ty3/nf2 ty3_nf2_inv_abst_premise_csort -ty3/nf2 ty3_nf2_inv_all -ty3/nf2 ty3_nf2_inv_sort -ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux -ty3/nf2 ty3_nf2_inv_abst -ty3/pr3 ty3_sred_wcpr0_pr0 -ty3/pr3 ty3_sred_pr0 -ty3/pr3 ty3_sred_pr1 -ty3/pr3 ty3_sred_pr2 -ty3/pr3 ty3_sred_pr3 -ty3/pr3_props ty3_cred_pr2 -ty3/pr3_props ty3_cred_pr3 -ty3/pr3_props ty3_gen_lift -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 -wf3/fwd wf3_gen_bind1 -wf3/fwd wf3_gen_flat1 -wf3/fwd wf3_gen_head2 -wf3/getl wf3_getl_conf -wf3/getl getl_wf3_trans -wf3/props wf3_mono -wf3/props wf3_total -wf3/props ty3_shift1 -wf3/props wf3_idem -wf3/props wf3_ty3 -wf3/ty3 wf3_pr2_conf -wf3/ty3 wf3_pr3_conf -wf3/ty3 wf3_pc3_conf -wf3/ty3 wf3_ty3_conf diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt new file mode 100644 index 000000000..b45870449 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -0,0 +1,468 @@ +# waiting #################################################################### + +aplus/props aplus_reg_r +aplus/props aplus_assoc +aplus/props aplus_asucc +aplus/props aplus_sort_O_S_simpl +aplus/props aplus_sort_S_S_simpl +aplus/props aplus_asort_O_simpl +aplus/props aplus_asort_le_simpl +aplus/props aplus_asort_simpl +aplus/props aplus_ahead_simpl +aplus/props aplus_asucc_false +aplus/props aplus_inj +aprem/fwd aprem_gen_sort +aprem/fwd aprem_gen_head_O +aprem/fwd aprem_gen_head_S +aprem/props aprem_repl +aprem/props aprem_asucc +arity/aprem arity_aprem +arity/cimp arity_cimp_conf +arity/fwd arity_gen_sort +arity/fwd arity_gen_lref +arity/fwd arity_gen_bind +arity/fwd arity_gen_abst +arity/fwd arity_gen_appl +arity/fwd arity_gen_cast +arity/fwd arity_gen_appls +arity/fwd arity_gen_lift +arity/lift1 arity_lift1 +arity/pr3 arity_sred_wcpr0_pr0 +arity/pr3 arity_sred_wcpr0_pr1 +arity/pr3 arity_sred_pr2 +arity/pr3 arity_sred_pr3 +arity/props node_inh +arity/props arity_lift +arity/props arity_mono +arity/props arity_repellent +arity/props arity_appls_cast +arity/props arity_appls_abbr +arity/props arity_appls_bind +arity/subst0 arity_gen_cvoid_subst0 +arity/subst0 arity_gen_cvoid +arity/subst0 arity_fsubst0 +arity/subst0 arity_subst0 +asucc/fwd asucc_gen_sort +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 +csuba/clear csuba_clear_conf +csuba/clear csuba_clear_trans +csuba/drop csuba_drop_abbr +csuba/drop csuba_drop_abst +csuba/drop csuba_drop_abst_rev +csuba/drop csuba_drop_abbr_rev +csuba/fwd csuba_gen_abbr +csuba/fwd csuba_gen_void +csuba/fwd csuba_gen_abst +csuba/fwd csuba_gen_flat +csuba/fwd csuba_gen_bind +csuba/fwd csuba_gen_abst_rev +csuba/fwd csuba_gen_void_rev +csuba/fwd csuba_gen_abbr_rev +csuba/fwd csuba_gen_flat_rev +csuba/fwd csuba_gen_bind_rev +csuba/getl csuba_getl_abbr +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/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 +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 +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 +ex0/props next_plus_gz +ex0/props leqz_leq +ex0/props leq_leqz +ex1/props ex1__leq_sort_SS +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 +leq/asucc leq_ahead_asucc_false +leq/asucc leq_asucc_false +leq/fwd leq_gen_sort1 +leq/fwd leq_gen_head1 +leq/fwd leq_gen_sort2 +leq/fwd leq_gen_head2 +leq/props ahead_inj_snd +leq/props leq_refl +leq/props leq_eq +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 +lift1/fwd lifts1_flat +lift1/fwd lifts1_nil +lift1/fwd lifts1_cons +lift1/props lift1_lift1 +lift1/props lift1_xhg +lift1/props lifts1_xhg +lift1/props lift1_free +lift/props thead_x_lift_y_y +lift/props lifts_tapp +lift/props lifts_inj +llt/props lweight_repl +llt/props llt_repl +llt/props llt_trans +llt/props llt_head_sx +llt/props llt_head_dx +llt/props llt_wf__q_ind +llt/props llt_wf_ind +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 +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 +pc1/props pc1_pr0_u +pc1/props pc1_s +pc1/props pc1_head_1 +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 +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 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 +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 +pr0/dec nf0_dec +pr0/subst1 pr0_subst1_back +pr0/subst1 pr0_subst1_fwd +pr1/pr1 pr1_strip +pr1/pr1 pr1_confluence +pr1/props pr1_pr0 +pr1/props pr1_t +pr1/props pr1_head_1 +pr1/props pr1_head_2 +pr1/props pr1_comp +pr1/props pr1_eta +pr2/clen pr2_gen_ctail + +# check ###################################################################### + +pr2/fwd pr2_gen_void +pr2/props pr2_ctail + + +# waiting #################################################################### + +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 +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_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 +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 +sty1/props sty1_appl +sty1/props sty1_lift +sty1/props sty1_correct +sty1/props sty1_abbr +sty1/props sty1_cast2 +subst0/dec dnf_dec2 +subst0/dec dnf_dec +subst1/props subst1_ex +subst/fwd subst_sort +subst/fwd subst_lref_lt +subst/fwd subst_lref_eq +subst/fwd subst_lref_gt +subst/fwd subst_head +subst/props subst_lift_SO +subst/props subst_subst0 +T/dec terms_props__bind_dec +T/dec bind_dec_not +T/dec terms_props__flat_dec +T/dec terms_props__kind_dec +T/dec term_dec +T/dec binder_dec +T/dec abst_dec +tlist/props tslt_wf__q_ind +tlist/props tslt_wf_ind +tlist/props theads_tapp +tlist/props tcons_tapp_ex +tlist/props tlist_ind_rev +T/props not_abbr_abst +T/props not_void_abst +T/props not_abbr_void +T/props not_abst_void +T/props thead_x_y_y +T/props tweight_lt +ty3/arity ty3_arity +ty3/arity_props ty3_predicative +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 +ty3/fwd_nf2 ty3_inv_lref_nf2_pc3 +ty3/fwd_nf2 ty3_inv_lref_nf2 +ty3/fwd_nf2 ty3_inv_appls_lref_nf2 +ty3/fwd_nf2 ty3_inv_lref_lref_nf2 +ty3/nf2 ty3_nf2_inv_abst_premise_csort +ty3/nf2 ty3_nf2_inv_all +ty3/nf2 ty3_nf2_inv_sort +ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux +ty3/nf2 ty3_nf2_inv_abst +ty3/pr3 ty3_sred_wcpr0_pr0 +ty3/pr3 ty3_sred_pr0 +ty3/pr3 ty3_sred_pr1 +ty3/pr3 ty3_sred_pr2 +ty3/pr3 ty3_sred_pr3 +ty3/pr3_props ty3_cred_pr2 +ty3/pr3_props ty3_cred_pr3 +ty3/pr3_props ty3_gen_lift +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 +wf3/fwd wf3_gen_bind1 +wf3/fwd wf3_gen_flat1 +wf3/fwd wf3_gen_head2 +wf3/getl wf3_getl_conf +wf3/getl getl_wf3_trans +wf3/props wf3_mono +wf3/props wf3_total +wf3/props ty3_shift1 +wf3/props wf3_idem +wf3/props wf3_ty3 +wf3/ty3 wf3_pr2_conf +wf3/ty3 wf3_pr3_conf +wf3/ty3 wf3_pc3_conf +wf3/ty3 wf3_ty3_conf diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma index 93afc607a..83169d811 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma @@ -62,3 +62,35 @@ lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d → qed. (* Basic inversion lemmas ***************************************************) + +(* Basic forward lemmas ***************************************************) + +fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → + d = 0 → e = |L1| → |L1| ≤ |L2|. +#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize +[ // +| /2/ +| /3/ +| /3/ +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H + elim (plus_S_eq_O_false … H) +] +qed. + +lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|. +/2 width=5/ qed. + +fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → + d = 0 → e = |L2| → |L2| ≤ |L1|. +#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize +[ // +| /2/ +| /3/ +| /3/ +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H + elim (plus_S_eq_O_false … H) +] +qed. + +lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma index 03a500cf4..3d1280a65 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma @@ -50,6 +50,14 @@ lemma cpr_cast: ∀L,V,T1,T2. #L #V #T1 #T2 * /3/ qed. +(* Note: it does not hold replacing |L1| with |L2| *) +(* Basic_1: was only: pr2_change *) +lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → + ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ⇒ T2. +#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 +lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 HL12 /3/ +qed. + (* Basic inversion lemmas ***************************************************) (* Basic_1: was: pr2_gen_csort *) @@ -85,7 +93,6 @@ qed. (* pr2/fwd pr2_gen_appl pr2/fwd pr2_gen_abbr -pr2/props pr2_change pr2/subst1 pr2_subst1 pr2/subst1 pr2_gen_cabbr *) diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 77f49615d..9a7cdc1ec 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -2,10 +2,10 @@ H = @ XOA_DIR = ../../../components/binaries/xoa XOA = xoa.native -CONF = Ground-2/xoa.conf.xml -TARGETS = Ground-2/xoa_natation.ma Ground-2/xoa.ma +CONF = Ground_2/xoa.conf.xml +TARGETS = Ground_2/xoa_natation.ma Ground_2/xoa.ma -PACKAGES = Ground-2 Basic-2 +PACKAGES = Ground_2 Basic_2 all: