From a8c166f1e1baeeae04553058bd179420ada8bbe7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 10 Mar 2012 19:03:31 +0000 Subject: [PATCH] - renaming completed! - one more property of context-sensitive computation - improved Makefile (from former commit) --- matita/matita/contribs/lambda_delta/Makefile | 6 +++--- .../lambda_delta/apps_2/functional/lift.ma | 6 +++--- .../lambda_delta/apps_2/functional/rtm.ma | 4 ++-- .../lambda_delta/apps_2/functional/rtm_step.ma | 2 +- .../lambda_delta/apps_2/functional/subst.ma | 4 ++-- .../basic_2/{Basic_1.txt => basic_1.txt} | 2 -- .../lambda_delta/basic_2/computation/acp.ma | 2 +- .../lambda_delta/basic_2/computation/acp_aaa.ma | 10 +++++----- .../lambda_delta/basic_2/computation/acp_cr.ma | 10 +++++----- .../lambda_delta/basic_2/computation/cprs.ma | 2 +- .../basic_2/computation/cprs_cprs.ma | 8 ++++---- .../basic_2/computation/cprs_lcpr.ma | 8 ++++---- .../basic_2/computation/cprs_lcprs.ma | 4 ++-- .../basic_2/computation/cprs_lift.ma | 16 ++++++++++++++-- .../basic_2/computation/cprs_tstc.ma | 8 ++++---- .../basic_2/computation/cprs_tstc_vector.ma | 6 +++--- .../lambda_delta/basic_2/computation/csn.ma | 4 ++-- .../lambda_delta/basic_2/computation/csn_aaa.ma | 4 ++-- .../lambda_delta/basic_2/computation/csn_cpr.ma | 4 ++-- .../lambda_delta/basic_2/computation/csn_cprs.ma | 4 ++-- .../lambda_delta/basic_2/computation/csn_lcpr.ma | 10 +++++----- .../basic_2/computation/csn_lcpr_vector.ma | 8 ++++---- .../lambda_delta/basic_2/computation/csn_lift.ma | 6 +++--- .../basic_2/computation/csn_vector.ma | 6 +++--- .../lambda_delta/basic_2/computation/lcprs.ma | 2 +- .../basic_2/computation/lcprs_cprs.ma | 6 +++--- .../basic_2/computation/lcprs_lcprs.ma | 2 +- .../lambda_delta/basic_2/computation/lsubc.ma | 4 ++-- .../basic_2/computation/lsubc_ldrop.ma | 6 +++--- .../basic_2/computation/lsubc_ldrops.ma | 2 +- .../basic_2/computation/lsubc_lsuba.ma | 4 ++-- .../lambda_delta/basic_2/conversion/cpc.ma | 2 +- .../lambda_delta/basic_2/conversion/cpc_cpc.ma | 2 +- .../lambda_delta/basic_2/equivalence/cpcs.ma | 2 +- .../lambda_delta/basic_2/grammar/aarity.ma | 4 ++-- .../lambda_delta/basic_2/grammar/cl_shift.ma | 2 +- .../lambda_delta/basic_2/grammar/cl_weight.ma | 4 ++-- .../lambda_delta/basic_2/grammar/genv.ma | 4 ++-- .../lambda_delta/basic_2/grammar/item.ma | 4 ++-- .../lambda_delta/basic_2/grammar/lenv.ma | 2 +- .../lambda_delta/basic_2/grammar/lenv_length.ma | 2 +- .../lambda_delta/basic_2/grammar/lenv_weight.ma | 4 ++-- .../lambda_delta/basic_2/grammar/lsubs.ma | 2 +- .../lambda_delta/basic_2/grammar/term.ma | 2 +- .../lambda_delta/basic_2/grammar/term_simple.ma | 2 +- .../lambda_delta/basic_2/grammar/term_vector.ma | 4 ++-- .../lambda_delta/basic_2/grammar/term_weight.ma | 2 +- .../lambda_delta/basic_2/grammar/tshf.ma | 2 +- .../lambda_delta/basic_2/grammar/tstc.ma | 2 +- .../lambda_delta/basic_2/grammar/tstc_tstc.ma | 2 +- .../lambda_delta/basic_2/grammar/tstc_vector.ma | 4 ++-- .../lambda_delta/basic_2/reducibility/cnf.ma | 2 +- .../basic_2/reducibility/cnf_lift.ma | 4 ++-- .../lambda_delta/basic_2/reducibility/cpr.ma | 6 +++--- .../lambda_delta/basic_2/reducibility/cpr_cpr.ma | 4 ++-- .../basic_2/reducibility/cpr_lift.ma | 6 +++--- .../basic_2/reducibility/cpr_ltpr.ma | 4 ++-- .../basic_2/reducibility/cpr_ltpss.ma | 4 ++-- .../lambda_delta/basic_2/reducibility/lcpr.ma | 4 ++-- .../basic_2/reducibility/lcpr_cpr.ma | 6 +++--- .../lambda_delta/basic_2/reducibility/ltpr.ma | 2 +- .../basic_2/reducibility/ltpr_ldrop.ma | 4 ++-- .../basic_2/reducibility/ltpr_tps.ma | 2 +- .../lambda_delta/basic_2/reducibility/tif.ma | 2 +- .../lambda_delta/basic_2/reducibility/tnf.ma | 2 +- .../lambda_delta/basic_2/reducibility/tnf_tif.ma | 6 +++--- .../lambda_delta/basic_2/reducibility/tpr.ma | 2 +- .../basic_2/reducibility/tpr_lift.ma | 4 ++-- .../lambda_delta/basic_2/reducibility/tpr_tpr.ma | 2 +- .../basic_2/reducibility/tpr_tpss.ma | 4 ++-- .../lambda_delta/basic_2/reducibility/trf.ma | 2 +- .../lambda_delta/basic_2/reducibility/twhnf.ma | 4 ++-- .../contribs/lambda_delta/basic_2/static/aaa.ma | 4 ++-- .../lambda_delta/basic_2/static/aaa_aaa.ma | 4 ++-- .../lambda_delta/basic_2/static/aaa_lift.ma | 4 ++-- .../lambda_delta/basic_2/static/aaa_lifts.ma | 4 ++-- .../lambda_delta/basic_2/static/lsuba.ma | 2 +- .../lambda_delta/basic_2/static/lsuba_aaa.ma | 4 ++-- .../lambda_delta/basic_2/static/lsuba_ldrop.ma | 2 +- .../lambda_delta/basic_2/static/lsuba_lsuba.ma | 2 +- .../contribs/lambda_delta/basic_2/static/sh.ma | 2 +- .../lambda_delta/basic_2/substitution/gdrop.ma | 2 +- .../basic_2/substitution/gdrop_gdrop.ma | 2 +- .../lambda_delta/basic_2/substitution/ldrop.ma | 6 +++--- .../basic_2/substitution/ldrop_ldrop.ma | 4 ++-- .../lambda_delta/basic_2/substitution/lift.ma | 4 ++-- .../basic_2/substitution/lift_lift.ma | 2 +- .../basic_2/substitution/lift_lift_vector.ma | 4 ++-- .../basic_2/substitution/lift_vector.ma | 4 ++-- .../lambda_delta/basic_2/substitution/ltps.ma | 2 +- .../basic_2/substitution/ltps_ldrop.ma | 2 +- .../basic_2/substitution/ltps_tps.ma | 4 ++-- .../lambda_delta/basic_2/substitution/tps.ma | 4 ++-- .../basic_2/substitution/tps_lift.ma | 4 ++-- .../lambda_delta/basic_2/substitution/tps_tps.ma | 2 +- .../lambda_delta/basic_2/unfold/delift.ma | 2 +- .../lambda_delta/basic_2/unfold/delift_lift.ma | 4 ++-- .../contribs/lambda_delta/basic_2/unfold/gr2.ma | 2 +- .../lambda_delta/basic_2/unfold/gr2_gr2.ma | 2 +- .../lambda_delta/basic_2/unfold/gr2_minus.ma | 2 +- .../lambda_delta/basic_2/unfold/gr2_plus.ma | 2 +- .../lambda_delta/basic_2/unfold/ldrops.ma | 6 +++--- .../lambda_delta/basic_2/unfold/ldrops_ldrop.ma | 4 ++-- .../lambda_delta/basic_2/unfold/ldrops_ldrops.ma | 2 +- .../lambda_delta/basic_2/unfold/lifts.ma | 4 ++-- .../lambda_delta/basic_2/unfold/lifts_lift.ma | 6 +++--- .../basic_2/unfold/lifts_lift_vector.ma | 6 +++--- .../lambda_delta/basic_2/unfold/lifts_lifts.ma | 2 +- .../lambda_delta/basic_2/unfold/lifts_vector.ma | 4 ++-- .../lambda_delta/basic_2/unfold/ltpss.ma | 4 ++-- .../lambda_delta/basic_2/unfold/ltpss_ldrop.ma | 4 ++-- .../lambda_delta/basic_2/unfold/ltpss_ltpss.ma | 2 +- .../lambda_delta/basic_2/unfold/ltpss_tpss.ma | 4 ++-- .../contribs/lambda_delta/basic_2/unfold/tpss.ma | 2 +- .../lambda_delta/basic_2/unfold/tpss_lift.ma | 4 ++-- .../lambda_delta/basic_2/unfold/tpss_ltps.ma | 4 ++-- .../lambda_delta/basic_2/unfold/tpss_tpss.ma | 4 ++-- .../contribs/lambda_delta/ground_2/arith.ma | 2 +- .../contribs/lambda_delta/ground_2/list.ma | 2 +- .../contribs/lambda_delta/ground_2/star.ma | 4 ++-- .../matita/contribs/lambda_delta/ground_2/tri.ma | 2 +- .../contribs/lambda_delta/ground_2/xoa.conf.xml | 2 +- .../contribs/lambda_delta/ground_2/xoa_props.ma | 4 ++-- 123 files changed, 238 insertions(+), 228 deletions(-) rename matita/matita/contribs/lambda_delta/basic_2/{Basic_1.txt => basic_1.txt} (99%) 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 similarity index 99% rename from matita/matita/contribs/lambda_delta/basic_2/Basic_1.txt rename to matita/matita/contribs/lambda_delta/basic_2/basic_1.txt index bc4582ede..633e77f54 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -251,10 +251,8 @@ 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 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/ -- 2.39.2