From: Ferruccio Guidi Date: Sat, 10 Mar 2012 19:03:31 +0000 (+0000) Subject: - renaming completed! X-Git-Tag: make_still_working~1863 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git - renaming completed! - one more property of context-sensitive computation - improved Makefile (from former commit) --- diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 49e7e1b23..119eafc5b 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 Apps_2 +PACKAGES = ground_2 basic_2 apps_2 all: diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma index aefa1576d..e2c802c51 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Ground_2/tri.ma". -include "Basic_2/substitution/lift.ma". -include "Apps_2/functional/notation.ma". +include "ground_2/tri.ma". +include "basic_2/substitution/lift.ma". +include "apps_2/functional/notation.ma". (* RELOCATION ***************************************************************) diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma index 845e8a04d..c7acff72e 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_vector.ma". -include "Basic_2/grammar/genv.ma". +include "basic_2/grammar/term_vector.ma". +include "basic_2/grammar/genv.ma". (* REDUCTION AND TYPE MACHINE ***********************************************) diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma index 5b2a4eb2c..f67d9dc1f 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Apps_2/functional/rtm.ma". +include "apps_2/functional/rtm.ma". (* REDUCTION AND TYPE MACHINE ***********************************************) diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma index 6aa75625d..bbeeb10f4 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/delift_lift.ma". -include "Apps_2/functional/lift.ma". +include "basic_2/unfold/delift_lift.ma". +include "apps_2/functional/lift.ma". (* CORE SUBSTITUTION ********************************************************) 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 bc4582ede..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/Basic_1.txt +++ /dev/null @@ -1,388 +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/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 -csubv/getl csubv_getl_conf -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 -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_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 -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/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 -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 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/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 -pr2/fwd pr2_gen_void -pr2/props pr2_ctail -pr2/subst1 pr2_gen_cabbr - -pr3/fwd pr3_gen_abst -pr3/fwd pr3_gen_lref -pr3/fwd pr3_gen_void -pr3/fwd pr3_gen_appl -pr3/fwd pr3_gen_bind -pr3/iso pr3_iso_appls_abbr -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/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_flat -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_lref -sn3/props sn3_appl_abbr -sn3/props sn3_appl_cast -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_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 -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 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 -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 - -# check ###################################################################### 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..633e77f54 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -0,0 +1,386 @@ +# 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/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 +csubv/getl csubv_getl_conf +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 +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_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 +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/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 +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 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/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 +pr2/fwd pr2_gen_void +pr2/props pr2_ctail +pr2/subst1 pr2_gen_cabbr + +pr3/fwd pr3_gen_lref +pr3/fwd pr3_gen_void +pr3/fwd pr3_gen_bind +pr3/iso pr3_iso_appls_abbr +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/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_flat +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_lref +sn3/props sn3_appl_abbr +sn3/props sn3_appl_cast +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_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 +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 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 +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 + +# check ###################################################################### diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma index 8be75a31f..dc046b094 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/ldrops.ma". +include "basic_2/unfold/ldrops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma index 1cab5d4b8..190a595cf 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/lifts_lifts.ma". -include "Basic_2/unfold/ldrops_ldrops.ma". -include "Basic_2/static/aaa_lifts.ma". -include "Basic_2/static/aaa_aaa.ma". -include "Basic_2/computation/lsubc_ldrops.ma". +include "basic_2/unfold/lifts_lifts.ma". +include "basic_2/unfold/ldrops_ldrops.ma". +include "basic_2/static/aaa_lifts.ma". +include "basic_2/static/aaa_aaa.ma". +include "basic_2/computation/lsubc_ldrops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma index 6eb71054b..c300d19de 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/aarity.ma". -include "Basic_2/unfold/gr2_gr2.ma". -include "Basic_2/unfold/lifts_lift_vector.ma". -include "Basic_2/unfold/ldrops_ldrop.ma". -include "Basic_2/computation/acp.ma". +include "basic_2/grammar/aarity.ma". +include "basic_2/unfold/gr2_gr2.ma". +include "basic_2/unfold/lifts_lift_vector.ma". +include "basic_2/unfold/ldrops_ldrop.ma". +include "basic_2/computation/acp.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma index 12cd0791f..e01515313 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma index 16c1a6256..47ec400c8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cpr_lift.ma". -include "Basic_2/reducibility/cpr_cpr.ma". -include "Basic_2/reducibility/lcpr_cpr.ma". -include "Basic_2/computation/cprs_lcpr.ma". +include "basic_2/reducibility/cpr_lift.ma". +include "basic_2/reducibility/cpr_cpr.ma". +include "basic_2/reducibility/lcpr_cpr.ma". +include "basic_2/computation/cprs_lcpr.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma index 7816989a7..14bcfd5c4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/ltpr_tps.ma". -include "Basic_2/reducibility/cpr_ltpss.ma". -include "Basic_2/reducibility/lcpr.ma". -include "Basic_2/computation/cprs.ma". +include "basic_2/reducibility/ltpr_tps.ma". +include "basic_2/reducibility/cpr_ltpss.ma". +include "basic_2/reducibility/lcpr.ma". +include "basic_2/computation/cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma index 6d4f5ec8c..1c9e28ad8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/computation/cprs_cprs.ma". -include "Basic_2/computation/lcprs_lcprs.ma". +include "basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/lcprs_lcprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma index ccff2f1fe..5ee21be85 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma @@ -12,11 +12,22 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cpr_lift.ma". -include "Basic_2/computation/cprs.ma". +include "basic_2/reducibility/cpr_lift.ma". +include "basic_2/computation/cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was: pr3_gen_abst *) +lemma cprs_inv_abst1: ∀I,W,L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡* U2 → + ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 & + U2 = ⓛV2. T2. +#I #W #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/ +#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct +elim (cpr_inv_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ +qed-. + (* Relocation properties ****************************************************) (* Basic_1: was: pr3_lift *) @@ -40,3 +51,4 @@ lemma cprs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → -HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1 elim (cpr_inv_lift … HLK … HTU … HU2) -U -HLK /3 width=5/ qed. + diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma index e623c7b90..cbbf170f9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/tstc.ma". +include "basic_2/grammar/tstc.ma". (* -include "Basic_2/reducibility/cpr_lift.ma". -include "Basic_2/reducibility/lcpr_cpr.ma". +include "basic_2/reducibility/cpr_lift.ma". +include "basic_2/reducibility/lcpr_cpr.ma". *) -include "Basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/cprs_cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma index 3e6f4a20d..2d6362045 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/tstc_vector.ma". -include "Basic_2/substitution/lift_vector.ma". -include "Basic_2/computation/cprs_tstc.ma". +include "basic_2/grammar/tstc_vector.ma". +include "basic_2/substitution/lift_vector.ma". +include "basic_2/computation/cprs_tstc.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma index 043fa9a27..868e8c1d2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cpr.ma". -include "Basic_2/reducibility/cnf.ma". +include "basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/cnf.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma index 421a3a7f7..112e2d4b7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/computation/acp_aaa.ma". -include "Basic_2/computation/csn_lcpr_vector.ma". +include "basic_2/computation/acp_aaa.ma". +include "basic_2/computation/csn_lcpr_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma index 11647e9dc..fba583c78 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cpr_cpr.ma". -include "Basic_2/computation/csn.ma". +include "basic_2/reducibility/cpr_cpr.ma". +include "basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma index bf6683d3c..530fde74c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/computation/cprs.ma". -include "Basic_2/computation/csn.ma". +include "basic_2/computation/cprs.ma". +include "basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma index 303be5997..28b9245ca 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/tstc_tstc.ma". -include "Basic_2/computation/cprs_cprs.ma". -include "Basic_2/computation/csn_lift.ma". -include "Basic_2/computation/csn_cpr.ma". -include "Basic_2/computation/csn_cprs.ma". +include "basic_2/grammar/tstc_tstc.ma". +include "basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/csn_lift.ma". +include "basic_2/computation/csn_cpr.ma". +include "basic_2/computation/csn_cprs.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma index 4ff8c039b..fc8901950 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "Basic_2/computation/acp_cr.ma". -include "Basic_2/computation/cprs_tstc_vector.ma". -include "Basic_2/computation/csn_lcpr.ma". -include "Basic_2/computation/csn_vector.ma". +include "basic_2/computation/acp_cr.ma". +include "basic_2/computation/cprs_tstc_vector.ma". +include "basic_2/computation/csn_lcpr.ma". +include "basic_2/computation/csn_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma index 01d983c0c..b658f9bc8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cnf_lift.ma". -include "Basic_2/computation/acp.ma". -include "Basic_2/computation/csn.ma". +include "basic_2/reducibility/cnf_lift.ma". +include "basic_2/computation/acp.ma". +include "basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma index bddaaa89d..b4a087a1a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_vector.ma". -include "Basic_2/computation/csn.ma". +include "basic_2/grammar/term_vector.ma". +include "basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) @@ -39,7 +39,7 @@ qed. lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts. /2 width=3/ qed-. -include "Basic_2/computation/csn_cpr.ma". +include "basic_2/computation/csn_cpr.ma". lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T. #L #T #Vs elim Vs -Vs /2 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma index 627a0f58d..312ededfa 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/lcpr.ma". +include "basic_2/reducibility/lcpr.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma index a45e8ee9f..2a33e92e7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/lcpr_cpr.ma". -include "Basic_2/computation/cprs.ma". -include "Basic_2/computation/lcprs.ma". +include "basic_2/reducibility/lcpr_cpr.ma". +include "basic_2/computation/cprs.ma". +include "basic_2/computation/lcprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma index 935b83d24..03e85b8db 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/computation/lcprs_cprs.ma". +include "basic_2/computation/lcprs_cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma index e61c2081d..d7094600c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/static/aaa.ma". -include "Basic_2/computation/acp_cr.ma". +include "basic_2/static/aaa.ma". +include "basic_2/computation/acp_cr.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma index 03ea7b628..838986a8f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/static/aaa_lift.ma". -include "Basic_2/computation/acp_cr.ma". -include "Basic_2/computation/lsubc.ma". +include "basic_2/static/aaa_lift.ma". +include "basic_2/computation/acp_cr.ma". +include "basic_2/computation/lsubc.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma index 95879a234..a61272c73 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/computation/lsubc_ldrop.ma". +include "basic_2/computation/lsubc_ldrop.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma index 41c906285..e50551086 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/static/lsuba.ma". -include "Basic_2/computation/acp_aaa.ma". +include "basic_2/static/lsuba.ma". +include "basic_2/computation/acp_aaa.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma index e3058349b..ed64873ef 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma index b4920c35c..dcea07a8b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/conversion/cpc.ma". +include "basic_2/conversion/cpc.ma". (* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma index 6004ee539..58e53ed78 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/conversion/cpc.ma". +include "basic_2/conversion/cpc.ma". (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma index 15418582b..f71f2d62e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma @@ -21,8 +21,8 @@ * [ suggested invocation to start formal specifications with ] *) -include "Ground_2/star.ma". -include "Basic_2/notation.ma". +include "ground_2/star.ma". +include "basic_2/notation.ma". (* ATOMIC ARITY *************************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma index 3a259cecf..ea82bde3c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/lenv.ma". +include "basic_2/grammar/lenv.ma". (* SHIFT OF A CLOSURE *******************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma index 925b84a34..af3b3496b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/lenv_weight.ma". -include "Basic_2/grammar/cl_shift.ma". +include "basic_2/grammar/lenv_weight.ma". +include "basic_2/grammar/cl_shift.ma". (* WEIGHT OF A CLOSURE ******************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma index 349f8708a..30b5dfd2a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Ground_2/list.ma". -include "Basic_2/grammar/term.ma". +include "ground_2/list.ma". +include "basic_2/grammar/term.ma". (* GLOBAL ENVIRONMENTS ******************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma index 7e4ee3839..deeaf047f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Ground_2/arith.ma". -include "Basic_2/notation.ma". +include "ground_2/arith.ma". +include "basic_2/notation.ma". (* ITEMS ********************************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma index 5aacaf57c..dc2c643b9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term.ma". +include "basic_2/grammar/term.ma". (* LOCAL ENVIRONMENTS *******************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma index 357301333..780edc161 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/lenv.ma". +include "basic_2/grammar/lenv.ma". (* LENGTH OF A LOCAL ENVIRONMENT ********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma index 414d3f1ab..bc8ffce87 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_weight.ma". -include "Basic_2/grammar/lenv.ma". +include "basic_2/grammar/term_weight.ma". +include "basic_2/grammar/lenv.ma". (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************) 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 2c27f0f9e..ed8404355 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lsubs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lsubs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/lenv_length.ma". +include "basic_2/grammar/lenv_length.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma index 6e8370d49..44e303691 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/item.ma". +include "basic_2/grammar/item.ma". (* TERMS ********************************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma index 9b6c08270..b51523544 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term.ma". +include "basic_2/grammar/term.ma". (* SIMPLE (NEUTRAL) TERMS ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma index 2b3f8880e..c2ad0f835 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Ground_2/list.ma". -include "Basic_2/grammar/term.ma". +include "ground_2/list.ma". +include "basic_2/grammar/term.ma". (* TERMS ********************************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma index 1cf414b38..00050032d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term.ma". +include "basic_2/grammar/term.ma". (* WEIGHT OF A TERM *********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma index 364a530e1..bb32a5365 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_simple.ma". +include "basic_2/grammar/term_simple.ma". (* SAME HEAD TERM FORMS *****************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma index c4c44c9f3..a4117b596 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_simple.ma". +include "basic_2/grammar/term_simple.ma". (* SAME TOP TERM CONSTRUCTOR ************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma index a32d045b5..df6fe3729 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/tstc.ma". +include "basic_2/grammar/tstc.ma". (* SAME TOP TERM CONSTRUCTOR ************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma index a3b38fcbf..0b7895923 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_vector.ma". -include "Basic_2/grammar/tstc.ma". +include "basic_2/grammar/term_vector.ma". +include "basic_2/grammar/tstc.ma". (* SAME TOP TERM CONSTRUCTOR ************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma index 39ac692cd..b97150df7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma index b492eb9af..43007c98a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/cpr_lift.ma". -include "Basic_2/reducibility/cnf.ma". +include "basic_2/reducibility/cpr_lift.ma". +include "basic_2/reducibility/cnf.ma". (* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma index 0ad09e4b4..220f8a648 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/cl_shift.ma". -include "Basic_2/unfold/tpss.ma". -include "Basic_2/reducibility/tpr.ma". +include "basic_2/grammar/cl_shift.ma". +include "basic_2/unfold/tpss.ma". +include "basic_2/reducibility/tpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma index 92db70f0f..4fa94673e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/tpr_tpr.ma". -include "Basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/tpr_tpr.ma". +include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma index 032ff4638..fd4940b7c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/tpss_lift.ma". -include "Basic_2/reducibility/tpr_lift.ma". -include "Basic_2/reducibility/cpr.ma". +include "basic_2/unfold/tpss_lift.ma". +include "basic_2/reducibility/tpr_lift.ma". +include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma index fcf4de993..72b714a62 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/tpr_tpss.ma". -include "Basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/tpr_tpss.ma". +include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma index 148a29645..26e045848 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/ltpss_tpss.ma". -include "Basic_2/reducibility/cpr.ma". +include "basic_2/unfold/ltpss_tpss.ma". +include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma index 80d14a2e5..51028c240 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/ltpss.ma". -include "Basic_2/reducibility/ltpr.ma". +include "basic_2/unfold/ltpss.ma". +include "basic_2/reducibility/ltpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma index 7abe34742..08f63e87f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/ltpss_ltpss.ma". -include "Basic_2/reducibility/cpr.ma". -include "Basic_2/reducibility/lcpr.ma". +include "basic_2/unfold/ltpss_ltpss.ma". +include "basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/lcpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma index 8e834b2da..8009cbeb7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/tpr.ma". +include "basic_2/reducibility/tpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma index 090e8cfbf..bb9195138 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/tpr_lift.ma". -include "Basic_2/reducibility/ltpr.ma". +include "basic_2/reducibility/tpr_lift.ma". +include "basic_2/reducibility/ltpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma index 91b30b014..bcf566f26 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/ltpr_ldrop.ma". +include "basic_2/reducibility/ltpr_ldrop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma index 5b89755a7..d3e010818 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/trf.ma". +include "basic_2/reducibility/trf.ma". (* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma index 5a7205cc0..a5f2e4407 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/tpr.ma". +include "basic_2/reducibility/tpr.ma". (* CONTEXT-FREE NORMAL TERMS ************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma index 2888ff9d6..ef9ecca4c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps_lift.ma". -include "Basic_2/reducibility/tif.ma". -include "Basic_2/reducibility/tnf.ma". +include "basic_2/substitution/tps_lift.ma". +include "basic_2/reducibility/tif.ma". +include "basic_2/reducibility/tnf.ma". (* CONTEXT-FREE NORMAL TERMS ************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma index 0edd15211..db2e187c2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps.ma". +include "basic_2/substitution/tps.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma index be40639a8..c55894034 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps_lift.ma". -include "Basic_2/reducibility/tpr.ma". +include "basic_2/substitution/tps_lift.ma". +include "basic_2/reducibility/tpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma index b1e3f3c1b..fefd6023d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/reducibility/tpr_tpss.ma". +include "basic_2/reducibility/tpr_tpss.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma index cf52701b5..2b36d1018 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/ltpss_ltpss.ma". -include "Basic_2/reducibility/ltpr_ldrop.ma". +include "basic_2/unfold/ltpss_ltpss.ma". +include "basic_2/reducibility/ltpr_ldrop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma index 3ae5bfd17..83306d2de 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_simple.ma". +include "basic_2/grammar/term_simple.ma". (* CONTEXT-FREE REDUCIBLE TERMS *********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma index 90598b1e7..687893b90 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/tshf.ma". -include "Basic_2/reducibility/tpr.ma". +include "basic_2/grammar/tshf.ma". +include "basic_2/reducibility/tpr.ma". (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma index ecf6b6833..097d24d60 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/aarity.ma". -include "Basic_2/substitution/ldrop.ma". +include "basic_2/grammar/aarity.ma". +include "basic_2/substitution/ldrop.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma index 4f9bb7dc3..ef00bfeeb 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ldrop_ldrop.ma". -include "Basic_2/static/aaa.ma". +include "basic_2/substitution/ldrop_ldrop.ma". +include "basic_2/static/aaa.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma index edf08147e..2d62640ad 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ldrop_ldrop.ma". -include "Basic_2/static/aaa.ma". +include "basic_2/substitution/ldrop_ldrop.ma". +include "basic_2/static/aaa.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma index 156e75c9d..cc1803672 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/ldrops.ma". -include "Basic_2/static/aaa_lift.ma". +include "basic_2/unfold/ldrops.ma". +include "basic_2/static/aaa_lift.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma index 5d087c93c..b3ca5d41b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/static/aaa.ma". +include "basic_2/static/aaa.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma index a6a9c3fae..4f45ce712 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/static/aaa_aaa.ma". -include "Basic_2/static/lsuba_ldrop.ma". +include "basic_2/static/aaa_aaa.ma". +include "basic_2/static/lsuba_ldrop.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma index 522252ae1..f055c01f5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/static/lsuba.ma". +include "basic_2/static/lsuba.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma index 24da36ccd..9fae68633 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/static/lsuba_aaa.ma". +include "basic_2/static/lsuba_aaa.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma index 7edbfd2af..4eeac01b8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Ground_2/arith.ma". +include "ground_2/arith.ma". (* SORT HIERARCHY ***********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma index eb4bd4865..218389e1c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/genv.ma". +include "basic_2/grammar/genv.ma". (* GLOBAL ENVIRONMENT SLICING ***********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma index 640c36c78..0bc1a40d5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/gdrop.ma". +include "basic_2/substitution/gdrop.ma". (* GLOBAL ENVIRONMENT SLICING ***********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma index c00819a74..e667c7cde 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/lenv_weight.ma". -include "Basic_2/grammar/lsubs.ma". -include "Basic_2/substitution/lift.ma". +include "basic_2/grammar/lenv_weight.ma". +include "basic_2/grammar/lsubs.ma". +include "basic_2/substitution/lift.ma". (* LOCAL ENVIRONMENT SLICING ************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma index 90f724ad3..17b40f947 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift_lift.ma". -include "Basic_2/substitution/ldrop.ma". +include "basic_2/substitution/lift_lift.ma". +include "basic_2/substitution/ldrop.ma". (* DROPPING *****************************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma index cb8aac3a0..5dfca806a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_weight.ma". -include "Basic_2/grammar/term_simple.ma". +include "basic_2/grammar/term_weight.ma". +include "basic_2/grammar/term_simple.ma". (* BASIC TERM RELOCATION ****************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma index 30bf8886e..74edd2ea2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift.ma". +include "basic_2/substitution/lift.ma". (* BASIC TERM RELOCATION ****************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma index cfb7b9250..cdc11129d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift_lift.ma". -include "Basic_2/substitution/lift_vector.ma". +include "basic_2/substitution/lift_lift.ma". +include "basic_2/substitution/lift_vector.ma". (* BASIC TERM VECTOR RELOCATION *********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma index aa0a30f95..d812f1cda 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_vector.ma". -include "Basic_2/substitution/lift.ma". +include "basic_2/grammar/term_vector.ma". +include "basic_2/substitution/lift.ma". (* BASIC TERM VECTOR RELOCATION *********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma index 4f30025d3..b1d435368 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps.ma". +include "basic_2/substitution/tps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma index bf4e1f711..e94aec40c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ltps.ma". +include "basic_2/substitution/ltps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma index e8dfe59af..9627335ec 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps_lift.ma". -include "Basic_2/substitution/ltps_ldrop.ma". +include "basic_2/substitution/tps_lift.ma". +include "basic_2/substitution/ltps_ldrop.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma index 11edc90b1..df09b9f20 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/cl_weight.ma". -include "Basic_2/substitution/ldrop.ma". +include "basic_2/grammar/cl_weight.ma". +include "basic_2/substitution/ldrop.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma index e453c4099..3481d7a1c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ldrop_ldrop.ma". -include "Basic_2/substitution/tps.ma". +include "basic_2/substitution/ldrop_ldrop.ma". +include "basic_2/substitution/tps.ma". (* PARTIAL SUBSTITUTION ON TERMS ********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma index 17346f53a..3155fe64f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps_lift.ma". +include "basic_2/substitution/tps_lift.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma index ec2d6c373..851e3d996 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/tpss.ma". +include "basic_2/unfold/tpss.ma". (* DELIFT ON TERMS **********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma index a02d3db2c..5ae82271d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/tpss_lift.ma". -include "Basic_2/unfold/delift.ma". +include "basic_2/unfold/tpss_lift.ma". +include "basic_2/unfold/delift.ma". (* DELIFT ON TERMS **********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma index 0896b6ba3..b8dab57ae 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_vector.ma". +include "basic_2/grammar/term_vector.ma". (* GENERIC RELOCATION WITH PAIRS ********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma index 438605e85..f7e42e334 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/gr2.ma". +include "basic_2/unfold/gr2.ma". (* GENERIC RELOCATION WITH PAIRS ********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma index 5e3144c93..5287e0f66 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/gr2.ma". +include "basic_2/unfold/gr2.ma". (* GENERIC RELOCATION WITH PAIRS ********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma index 938f955b9..6d66f0dab 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/gr2.ma". +include "basic_2/unfold/gr2.ma". (* GENERIC RELOCATION WITH PAIRS ********************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma index 28b9a8c7e..70c09b1f5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ldrop.ma". -include "Basic_2/unfold/gr2_minus.ma". -include "Basic_2/unfold/lifts.ma". +include "basic_2/substitution/ldrop.ma". +include "basic_2/unfold/gr2_minus.ma". +include "basic_2/unfold/lifts.ma". (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma index de8a1fef6..fe11428dc 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ldrop_ldrop.ma". -include "Basic_2/unfold/ldrops.ma". +include "basic_2/substitution/ldrop_ldrop.ma". +include "basic_2/unfold/ldrops.ma". (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma index 1bb40cb5d..1cb1724fd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/ldrops_ldrop.ma". +include "basic_2/unfold/ldrops_ldrop.ma". (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma index 6a3c647a0..492ffdcbe 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift.ma". -include "Basic_2/unfold/gr2_plus.ma". +include "basic_2/substitution/lift.ma". +include "basic_2/unfold/gr2_plus.ma". (* GENERIC TERM RELOCATION **************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma index 3f63d2eb8..23a488072 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift_lift.ma". -include "Basic_2/unfold/gr2_minus.ma". -include "Basic_2/unfold/lifts.ma". +include "basic_2/substitution/lift_lift.ma". +include "basic_2/unfold/gr2_minus.ma". +include "basic_2/unfold/lifts.ma". (* GENERIC TERM RELOCATION **************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma index 0d279c6da..bbd3b1d8b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift_lift_vector.ma". -include "Basic_2/unfold/lifts_lift.ma". -include "Basic_2/unfold/lifts_vector.ma". +include "basic_2/substitution/lift_lift_vector.ma". +include "basic_2/unfold/lifts_lift.ma". +include "basic_2/unfold/lifts_vector.ma". (* GENERIC RELOCATION *******************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma index 6062f89b1..0ea0a2186 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/lifts_lift.ma". +include "basic_2/unfold/lifts_lift.ma". (* GENERIC RELOCATION *******************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma index 2bd579d01..b757b9cb7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift_vector.ma". -include "Basic_2/unfold/lifts.ma". +include "basic_2/substitution/lift_vector.ma". +include "basic_2/unfold/lifts.ma". (* GENERIC TERM VECTOR RELOCATION *******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma index 207bfc60f..c445f6890 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ltps.ma". -include "Basic_2/unfold/tpss.ma". +include "basic_2/substitution/ltps.ma". +include "basic_2/unfold/tpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma index b52cedae7..59269ef11 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ltps_ldrop.ma". -include "Basic_2/unfold/ltpss.ma". +include "basic_2/substitution/ltps_ldrop.ma". +include "basic_2/unfold/ltpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma index 7091e0803..370de3e6e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/ltpss_tpss.ma". +include "basic_2/unfold/ltpss_tpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma index 24f1a595e..3e4dba50d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/unfold/tpss_ltps.ma". -include "Basic_2/unfold/ltpss.ma". +include "basic_2/unfold/tpss_ltps.ma". +include "basic_2/unfold/ltpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma index 16a0d3e4d..707e46959 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps.ma". +include "basic_2/substitution/tps.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma index 748efd827..f12e38877 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps_lift.ma". -include "Basic_2/unfold/tpss.ma". +include "basic_2/substitution/tps_lift.ma". +include "basic_2/unfold/tpss.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma index 58b63cd01..efaf3f54c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ltps_tps.ma". -include "Basic_2/unfold/tpss_tpss.ma". +include "basic_2/substitution/ltps_tps.ma". +include "basic_2/unfold/tpss_tpss.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma index 981402a24..b0d28be56 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/tps_tps.ma". -include "Basic_2/unfold/tpss_lift.ma". +include "basic_2/substitution/tps_tps.ma". +include "basic_2/unfold/tpss_lift.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma index 39d28c959..0bdcd748f 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "arithmetics/nat.ma". -include "Ground_2/star.ma". +include "ground_2/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) diff --git a/matita/matita/contribs/lambda_delta/ground_2/list.ma b/matita/matita/contribs/lambda_delta/ground_2/list.ma index 0a6e69bbe..010c49f2b 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/list.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/list.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Ground_2/arith.ma". +include "ground_2/arith.ma". (* LISTS ********************************************************************) diff --git a/matita/matita/contribs/lambda_delta/ground_2/star.ma b/matita/matita/contribs/lambda_delta/ground_2/star.ma index ed3580642..c183111dd 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/star.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/star.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basics/star.ma". -include "Ground_2/xoa_props.ma". -include "Ground_2/notation.ma". +include "ground_2/xoa_props.ma". +include "ground_2/notation.ma". (* PROPERTIES OF RELATIONS **************************************************) diff --git a/matita/matita/contribs/lambda_delta/ground_2/tri.ma b/matita/matita/contribs/lambda_delta/ground_2/tri.ma index 005806c11..4fc619565 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/tri.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/tri.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Ground_2/arith.ma". +include "ground_2/arith.ma". (* TRICOTOMY FUNCTION *******************************************************) diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml index 2a2da2a5c..d18d4192a 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml @@ -10,7 +10,7 @@ -->
- contribs/lambda_delta/Ground_2/ + contribs/lambda_delta/ground_2/ xoa xoa_notation basics/pts.ma diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma index 121eb7e74..e212a60e5 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Ground_2/xoa_notation.ma". -include "Ground_2/xoa.ma". +include "ground_2/xoa_notation.ma". +include "ground_2/xoa.ma". lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0. #A0 #P0 #P1 * /2 width=3/