lsubs renamed as lsubr

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index e20ce0559c9639a07234ac19a1f0511533883e13..ccfa7901101fbe13f2de5f735ff41e3403ad812f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -59,7 +59,7 @@ lemma cprs_strap2: ∀L,T1,T,T2.
 /2 width=3/ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
-lemma cprs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
+lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
                         ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
 /3 width=3/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
index c89fab769f10b4da8df8b40ff3bace410a64c383..75f74caad725a84a3c556c4b423d3378de6c298b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
@@ -99,7 +99,7 @@ qed.
 lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 →
                  ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
 #L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a #I @(cprs_ind … HV12) -V2
-[ lapply (cprs_lsubs_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
+[ lapply (cprs_lsubr_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
 | #V0 #V2 #_ #HV02 #IHV01
   @(cprs_trans … IHV01) -V1 /2 width=2/
 ]
@@ -146,7 +146,7 @@ lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2.
 #L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #a @(cprs_ind … HT12) -T2
 [ /3 width=1/
 | -HV12 #T #T2 #_ #HT2 #IHT1
-  lapply (cpr_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+  lapply (cpr_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
   @(cprs_trans … IHT1) -V1 -W -T1 /3 width=1/
 ]
 qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
index 089dbed26c81657eb8c2c14225adfc8ba422c856..8df6fb7108c6cb26903451744c15d2422248aa00 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
@@ -101,12 +101,12 @@ lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → h ⊢ L1 •⊑[
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/
 qed-.
 
-lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L1|] L2.
-/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs1/
+lemma lsubsv_fwd_lsubr1: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L1|] L2.
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr1/
 qed-.
 
-lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L2|] L2.
-/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs2/
+lemma lsubsv_fwd_lsubr2: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L2|] L2.
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr2/
 qed-.
 
 (* Basic properties *********************************************************)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
index 15acdc94387de66b82cdd914d3b54d433b0cef10..750c71fdc5ad28345cf1cc21f4ea1d7fd7f79e9b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
@@ -21,5 +21,5 @@ include "basic_2/dynamic/lsubsv.ma".
 
 lemma lsubsv_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
                          ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
-/3 width=5 by lsubsv_fwd_lsubs2, cpcs_lsubs_trans/
+/3 width=5 by lsubsv_fwd_lsubr2, cpcs_lsubr_trans/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
index 79ca41081e153de610dccdc5f99b8f2265fabbf9..17ae5d32666977b7d79e957acc3a4b18478da76a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
@@ -41,7 +41,7 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
   elim (snv_inv_bind … H1) -H1 #HV1 #HT1
   elim (tpr_inv_bind1 … H2) -H2 *
   [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
+    lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
     lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
     lapply (snv_ltpr_cpr_aux … HT1  (L2.ⓑ{I}V2) … T2 ?) -HT1
     [ /3 width=5 by cpr_intro, tps_tpss/ | /2 width=1/ | /3 width=1/ ] -IH1 -T0 /2 width=1/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
index 1cd5ead77b522b5eb197c183a437a17c08d6148c..d7a40613ec5c60e0ff4232dafa6b8af135e5668f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
@@ -57,7 +57,7 @@ fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0.
   elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
   elim (tpr_inv_bind1 … H3) -H3 *
   [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
-    lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02
+    lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02
     elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1
     [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12
     lapply (cpcs_bind2 … V1 … HU12 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
index a31853a7f301c6533ddf382ed0d19be0936dfc83..cbc1ea3dae57f36f43bd54e43fbdd6b83d2f1c58 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -154,7 +154,7 @@ lemma cpcs_beta_dx: ∀a,L,V1,V2,W,T1,T2.
 #a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
 lapply (cprs_beta_dx … HV12 HT1 a) -HV12 -HT1 #HT1
-lapply (cprs_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+lapply (cprs_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
 @(cprs_div … HT1) /2 width=1/
 qed.
 
@@ -164,11 +164,11 @@ lemma cpcs_beta_dx_tpr_rev: ∀a,L,V1,V2,W,T1,T2.
 /4 width=1/ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpcs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
+lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
                         ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
 #L1 #T1 #T2 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12
-/3 width=5 by cprs_div, cprs_lsubs_trans/ (**) (* /3 width=5/ is a bit slow *)
+/3 width=5 by cprs_div, cprs_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *)
 qed.
 
 (* Basic_1: was: pc3_lift *)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
index 5898d4ecfaf019032d9496be95f5992fae9069d9..ac8f5373cd7163fad79c7ad61cc429f92cc8c92d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma
@@ -94,11 +94,11 @@ lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 •⊑[g] K2. ⓑ{I} W2 →
 
 (* Basic_forward lemmas *****************************************************)
 
-lemma lsubss_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2.
+lemma lsubss_fwd_lsubr1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
-lemma lsubss_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2.
+lemma lsubss_fwd_lsubr2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
@@ -110,5 +110,5 @@ qed.
 
 lemma lsubss_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
                          ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-/3 width=5 by lsubss_fwd_lsubs2, cprs_lsubs_trans/
+/3 width=5 by lsubss_fwd_lsubr2, cprs_lsubr_trans/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss_cpcs.ma
index cfb7372a46648f14b48065b40064442474f9cb01..cbddc65e9da71d3f714647242f02afaf76ef1eb8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss_cpcs.ma
@@ -21,5 +21,5 @@ include "basic_2/equivalence/lsubss.ma".
 
 lemma lsubss_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
                          ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
-/3 width=5 by lsubss_fwd_lsubs2, cpcs_lsubs_trans/
+/3 width=5 by lsubss_fwd_lsubr2, cpcs_lsubr_trans/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
index 8ee507cc14c1fa421326b2982f258bf56d0c79e3..5a1ae5a5b69050614d3ebbed20c1000ded88d228 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
@@ -50,7 +50,7 @@ lemma tpr_cif_eq: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ 𝐈⦃T1⦄ → T1 = T2.
   elim (cif_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
 | #a * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #L #H
-  [ lapply (tps_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+  [ lapply (tps_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
     elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct
     lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
     lapply (IHT1 … HT1) -IHT1 #H destruct

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
index 56e10d39298ba758cdcda4a13a14c29df62424a5..2317250cccbb17c8e5c37041c2828a5c6b942f86 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
@@ -54,10 +54,10 @@ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
 (* Basic_1: was only: pr2_change *)
-lemma cpr_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
+lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
                        ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
 #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
-lapply (tpss_lsubs_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
+lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
 qed.
 
 (* Basic inversion lemmas ***************************************************)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
index d0738e4c40722b47def8552e7f26bac835866eeb..039dc29e0ba352111a63c39466271b66ca9e04ef 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma
@@ -30,7 +30,7 @@ lemma cpr_bind_dx: ∀a,I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T
                    L ⊢ ⓑ{a,I} V1. T1 ➡ ⓑ{a,I} V2. T2.
 #a #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_lsubs_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
+lapply (tpss_lsubr_trans … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
 lapply (tpss_inv_SO2 … HT0) -HT0 #HT0
 @ex2_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
 qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
index b59a3e6ed02628a85c99f82ed8c23e0e3cea5709..5206f43ce742a3714cf8b67905177e1af37938eb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
@@ -32,7 +32,7 @@ lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡ T2
                           ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡ ⓑ{a,I}V2. T2.
 #L #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02 #a #I
 lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02
-lapply (tpss_lsubs_trans … HT02 (L.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
+lapply (tpss_lsubr_trans … HT02 (L.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
 @(ex2_intro … (ⓑ{a,I}V0.T0)) /2 width=1/ (* explicit constructors *)
 qed.
 
@@ -40,7 +40,7 @@ lemma cpr_beta: ∀a,L,V1,V2,W,T1,T2.
                 L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ➡ ⓓ{a}V2.T2.
 #a #L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2
 lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
-lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+lapply (tpss_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
 @(ex2_intro … (ⓓ{a}V.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too slow *)
 qed.
 
@@ -74,9 +74,9 @@ lemma cpr_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡ U2 →
 elim (tpr_inv_abbr1 … H1) -H1 *
 [ #V #T #T0 #HV1 #HT1 #HT0 #H destruct
   elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT02 #H destruct
-  lapply (tps_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
+  lapply (tps_lsubr_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
   lapply (tps_weak_all … HT0) -HT0 #HT0
-  lapply (tpss_lsubs_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
+  lapply (tpss_lsubr_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
   lapply (tpss_weak_all … HT02) -HT02 #HT02
   lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/
 | #T2 #HT12 #HXT2 #H destruct
@@ -92,7 +92,7 @@ lemma cpr_inv_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡ U2 → ∀I,W.
 #a #L #V1 #T1 #Y * #X #H1 #H2 #I #W
 elim (tpr_inv_abst1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
 elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
-lapply (tpss_lsubs_trans … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
+lapply (tpss_lsubr_trans … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
 qed-.
 
 (* Basic_1: was pr2_gen_appl *)
@@ -143,7 +143,7 @@ lemma cpr_fwd_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1.T1 ➡ U2 → ∀b,I,W.
 #a #L #V1 #T1 #U2 * #U #H #HU2 #b #I #W
 elim (tpr_fwd_abst1 … H b I W) -H #V #T #HT1 #H destruct
 elim (tpss_inv_bind1 … HU2) -HU2 #V2 #T2 #_ #HT2
-lapply (tpss_lsubs_trans … HT2 (L.ⓑ{I}W) ?) -HT2 /2 width=1/ /4 width=5/
+lapply (tpss_lsubr_trans … HT2 (L.ⓑ{I}W) ?) -HT2 /2 width=1/ /4 width=5/
 qed-.
 
 (* Relocation properties ****************************************************)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
index a8b117fec9b1c2029f4c9f2ec88af534911f4174..5208a64051ca975c82ac18093e100044aa2bc91b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma
@@ -38,7 +38,7 @@ lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 →
 | elim (aaa_inv_abbr … H1) -H1 #B #HB #HA
   elim (tpr_inv_abbr1 … H2) -H2 *
   [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
-    lapply (tps_lsubs_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+    lapply (tps_lsubr_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
     lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
     lapply (IH … HA … (L2.ⓓV2) … HT1) -IH -HA -HT1 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
   | -B #T #HT1 #HXT #H destruct

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
index ff5cfb6a161b11f3f6c8dccb2d43a7367baaf45f..597fe64ebe2b2df09e4ae608d450756672b24b2b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma
@@ -36,16 +36,16 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
   elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
   elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
   elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
-  lapply (tpss_lsubs_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
+  lapply (tpss_lsubr_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
 | #a #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
   elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2
   elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
   elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2
-  lapply (tps_lsubs_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
+  lapply (tps_lsubr_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
   elim (ltpss_dx_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23
-  lapply (tps_lsubs_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
-  lapply (tpss_lsubs_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
+  lapply (tps_lsubr_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
+  lapply (tpss_lsubr_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
   lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/
 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
index 87d83b3472819ccaea16949e8b61ab8afb4352d1..7e7ac3c5402105189a651cbc26844198c360c1e8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/grammar/cl_weight.ma".
 include "basic_2/substitution/lift.ma".
-include "basic_2/substitution/lsubs.ma".
+include "basic_2/substitution/lsubr.ma".
 
 (* LOCAL ENVIRONMENT SLICING ************************************************)
 
@@ -186,7 +186,7 @@ lemma ldrop_O1_lt: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
 ]
 qed.
 
-lemma ldrop_lsubs_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+lemma ldrop_lsubr_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
                                ∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
                                d ≤ i → i < d + e →
                                ∃∃K1. K1 ≼ [0, d + e - i - 1] K2 &

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
index 83c157a5af97bbc90e0830d30089cc2377da67eb..9d4cc31086962f9cd679f3884f1c4b3be8f1c715 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_sfr.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lsubs_sfr.ma".
+include "basic_2/substitution/lsubr_sfr.ma".
 include "basic_2/substitution/ldrop_ldrop.ma".
 
 (* DROPPING *****************************************************************)
@@ -30,7 +30,7 @@ lemma sfr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ≽ [d
   [ -IHL #H1 #H2 #d #e #HL #Hdi #Hide destruct
     lapply (le_n_O_to_eq … Hdi) -Hdi #H destruct
     lapply (HL … (L.ⓓW) ?) -HL /2 width=1/ #H
-    elim (lsubs_inv_abbr2 … H ?) -H // -Hide #K #_ #H destruct //
+    elim (lsubr_inv_abbr2 … H ?) -H // -Hide #K #_ #H destruct //
   | #Hi #HLK #d @(nat_ind_plus … d) -d
     [ #e #H #_ #Hide
       elim (sfr_inv_bind … H ?) -H [2: /2 width=2/ ] #HL #H destruct

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
new file mode 100644 (file)
index 0000000..2a4e432
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
@@ -0,0 +1,194 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+inductive lsubr: nat → nat → relation lenv ≝
+| lsubr_sort: ∀d,e. lsubr d e (⋆) (⋆)
+| lsubr_OO:   ∀L1,L2. lsubr 0 0 L1 L2
+| lsubr_abbr: ∀L1,L2,V,e. lsubr 0 e L1 L2 →
+              lsubr 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
+| lsubr_abst: ∀L1,L2,I,V1,V2,e. lsubr 0 e L1 L2 →
+              lsubr 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2)
+| lsubr_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
+              lsubr d e L1 L2 → lsubr (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
+.
+
+interpretation
+  "local environment refinement (substitution)"
+  'SubEq L1 d e L2 = (lsubr d e L1 L2).
+
+definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+                        ∀L2,s1,s2. R L2 s1 s2 →
+                        ∀L1,d,e. L1 ≼ [d, e] L2 → R L1 s1 s2.
+
+(* Basic properties *********************************************************)
+
+lemma lsubr_bind_eq: ∀L1,L2,e. L1 ≼ [0, e] L2 → ∀I,V.
+                     L1. ⓑ{I} V ≼ [0, e + 1] L2.ⓑ{I} V.
+#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
+qed.
+
+lemma lsubr_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+                     L1. ⓓV ≼ [0, e] L2.ⓓV.
+#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
+qed.
+
+lemma lsubr_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+                     L1. ⓑ{I}V1 ≼ [0, e] L2. ⓛV2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
+qed.
+
+lemma lsubr_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d →
+                     ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ≼ [d, e] L2. ⓑ{I2} V2.
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
+qed.
+
+lemma lsubr_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
+                     L1. ⓓV ≼ [0, e] L2. ⓑ{I}V.
+* /2 width=1/ qed.
+
+lemma lsubr_refl: ∀d,e,L. L ≼ [d, e] L.
+#d elim d -d
+[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
+| #d #IHd #e #L elim L -L // /2 width=1/
+]
+qed.
+
+lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (λL. (TC … (R L))).
+#S #R #HR #L1 #s1 #s2 #H elim H -s2
+[ /3 width=5/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
+  lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ →
+                          L2 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubr_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 →
+                       L2 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubr_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                          ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
+                          ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #I1 #K1 #V1 #H destruct
+| #L1 #L2 #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+]
+qed.
+
+lemma lsubr_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
+                       ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=5/ qed-.
+
+fact lsubr_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
+                          L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubr_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
+                       L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                          ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
+                          ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #K1 #V #H destruct
+| #L1 #L2 #K1 #V #_ #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/
+| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubr_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e →
+                       ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
+/2 width=5/ qed-.
+
+fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                          ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
+                          ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #I1 #K1 #V1 #H destruct
+| #L1 #L2 #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+]
+qed.
+
+lemma lsubr_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ≼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
+                       ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
+/2 width=5/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+fact lsubr_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                                 d = 0 → e = |L1| → |L1| ≤ |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
+[ //
+| /2 width=1/
+| /3 width=1/
+| /3 width=1/
+| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubr_fwd_length_full1: ∀L1,L2. L1 ≼ [0, |L1|] L2 → |L1| ≤ |L2|.
+/2 width=5/ qed-.
+
+fact lsubr_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                                 d = 0 → e = |L2| → |L2| ≤ |L1|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
+[ //
+| /2 width=1/
+| /3 width=1/
+| /3 width=1/
+| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma lsubr_fwd_length_full2: ∀L1,L2. L1 ≼ [0, |L2|] L2 → |L2| ≤ |L1|.
+/2 width=5/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma
new file mode 100644 (file)
index 0000000..e35a371
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma
@@ -0,0 +1,73 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/substitution/lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+(* bottom element of the refinement *)
+definition sfr: nat → nat → predicate lenv ≝
+   λd,e. NF_sn … (lsubr d e) (lsubr d e …).
+
+interpretation
+   "local environment full refinement (substitution)"
+   'SubEqBottom d e L = (sfr d e L).
+
+(* Basic properties *********************************************************)
+
+lemma sfr_atom: ∀d,e. ≽ [d, e] ⋆.
+#d #e #L #H
+elim (lsubr_inv_atom2 … H) -H
+[ #H destruct //
+| * #H1 #H2 destruct //
+]
+qed.
+
+lemma sfr_OO: ∀L. ≽ [0, 0] L.
+// qed.
+
+lemma sfr_abbr: ∀L,V,e. ≽ [0, e] L → ≽ [0, e + 1] L.ⓓV.
+#L #V #e #HL #K #H
+elim (lsubr_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
+lapply (HL … HLX) -HL -HLX /2 width=1/
+qed.
+
+lemma sfr_abbr_O: ∀L,V. ≽[0,1] L.ⓓV.
+#L #V
+@(sfr_abbr … 0) //
+qed.
+
+lemma sfr_skip: ∀I,L,V,d,e. ≽ [d, e] L → ≽ [d + 1, e] L.ⓑ{I}V.
+#I #L #V #d #e #HL #K #H
+elim (lsubr_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
+lapply (HL … HLX) -HL -HLX /2 width=1/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma sfr_inv_bind: ∀I,L,V,e. ≽ [0, e] L.ⓑ{I}V → 0 < e →
+                    ≽ [0, e - 1] L ∧ I = Abbr.
+#I #L #V #e #HL #He
+lapply (HL (L.ⓓV) ?) /2 width=1/ #H
+elim (lsubr_inv_abbr2 … H ?) -H // #K #_ #H destruct
+@conj // #L #HKL
+lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
+elim (lsubr_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
+qed-.
+
+lemma sfr_inv_skip: ∀I,L,V,d,e. ≽ [d, e] L.ⓑ{I}V → 0 < d → ≽ [d - 1, e] L.
+#I #L #V #d #e #HL #Hd #K #HLK
+lapply (HL (K.ⓑ{I}V) ?) -HL /2 width=1/ -HLK #H
+elim (lsubr_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma
deleted file mode 100644 (file)
index 1c0756c..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma
+++ /dev/null
@@ -1,194 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/grammar/lenv_length.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
-
-inductive lsubs: nat → nat → relation lenv ≝
-| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
-| lsubs_OO:   ∀L1,L2. lsubs 0 0 L1 L2
-| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
-              lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
-| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
-              lsubs 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2)
-| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
-              lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
-.
-
-interpretation
-  "local environment refinement (substitution)"
-  'SubEq L1 d e L2 = (lsubs d e L1 L2).
-
-definition lsubs_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
-                        ∀L2,s1,s2. R L2 s1 s2 →
-                        ∀L1,d,e. L1 ≼ [d, e] L2 → R L1 s1 s2.
-
-(* Basic properties *********************************************************)
-
-lemma lsubs_bind_eq: ∀L1,L2,e. L1 ≼ [0, e] L2 → ∀I,V.
-                     L1. ⓑ{I} V ≼ [0, e + 1] L2.ⓑ{I} V.
-#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
-qed.
-
-lemma lsubs_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
-                     L1. ⓓV ≼ [0, e] L2.ⓓV.
-#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
-qed.
-
-lemma lsubs_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
-                     L1. ⓑ{I}V1 ≼ [0, e] L2. ⓛV2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
-qed.
-
-lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d →
-                     ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ≼ [d, e] L2. ⓑ{I2} V2.
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
-qed.
-
-lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
-                     L1. ⓓV ≼ [0, e] L2. ⓑ{I}V.
-* /2 width=1/ qed.
-
-lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
-#d elim d -d
-[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
-| #d #IHd #e #L elim L -L // /2 width=1/
-]
-qed.
-
-lemma TC_lsubs_trans: ∀S,R. lsubs_trans S R → lsubs_trans S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -s2
-[ /3 width=5/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
-  lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/
-]
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubs_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ →
-                          L2 = ⋆ ∨ (d = 0 ∧ e = 0).
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ /2 width=1/
-| /3 width=1/
-| #L1 #L2 #W #e #_ #H destruct
-| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
-| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
-]
-qed.
-
-lemma lsubs_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 →
-                       L2 = ⋆ ∨ (d = 0 ∧ e = 0).
-/2 width=3/ qed-.
-
-fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                          ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
-                          ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ #d #e #I1 #K1 #V1 #H destruct
-| #L1 #L2 #I1 #K1 #V1 #_ #H
-  elim (lt_zero_false … H)
-| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
-  elim (lt_zero_false … H)
-| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
-  elim (lt_zero_false … H)
-| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
-]
-qed.
-
-lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
-                       ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
-/2 width=5/ qed-.
-
-fact lsubs_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
-                          L1 = ⋆ ∨ (d = 0 ∧ e = 0).
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ /2 width=1/
-| /3 width=1/
-| #L1 #L2 #W #e #_ #H destruct
-| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
-| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
-]
-qed.
-
-lemma lsubs_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
-                       L1 = ⋆ ∨ (d = 0 ∧ e = 0).
-/2 width=3/ qed-.
-
-fact lsubs_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                          ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
-                          ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ #d #e #K1 #V #H destruct
-| #L1 #L2 #K1 #V #_ #_ #H
-  elim (lt_zero_false … H)
-| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/
-| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct
-| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubs_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e →
-                       ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
-/2 width=5/ qed-.
-
-fact lsubs_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                          ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
-                          ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ #d #e #I1 #K1 #V1 #H destruct
-| #L1 #L2 #I1 #K1 #V1 #_ #H
-  elim (lt_zero_false … H)
-| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
-  elim (lt_zero_false … H)
-| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
-  elim (lt_zero_false … H)
-| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
-]
-qed.
-
-lemma lsubs_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ≼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
-                       ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
-/2 width=5/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                                 d = 0 → e = |L1| → |L1| ≤ |L2|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
-[ //
-| /2 width=1/
-| /3 width=1/
-| /3 width=1/
-| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubs_fwd_length_full1: ∀L1,L2. L1 ≼ [0, |L1|] L2 → |L1| ≤ |L2|.
-/2 width=5/ qed-.
-
-fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                                 d = 0 → e = |L2| → |L2| ≤ |L1|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
-[ //
-| /2 width=1/
-| /3 width=1/
-| /3 width=1/
-| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubs_fwd_length_full2: ∀L1,L2. L1 ≼ [0, |L2|] L2 → |L2| ≤ |L1|.
-/2 width=5/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma
deleted file mode 100644 (file)
index b71f25e..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma
+++ /dev/null
@@ -1,73 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/substitution/lsubs.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
-
-(* bottom element of the refinement *)
-definition sfr: nat → nat → predicate lenv ≝
-   λd,e. NF_sn … (lsubs d e) (lsubs d e …).
-
-interpretation
-   "local environment full refinement (substitution)"
-   'SubEqBottom d e L = (sfr d e L).
-
-(* Basic properties *********************************************************)
-
-lemma sfr_atom: ∀d,e. ≽ [d, e] ⋆.
-#d #e #L #H
-elim (lsubs_inv_atom2 … H) -H
-[ #H destruct //
-| * #H1 #H2 destruct //
-]
-qed.
-
-lemma sfr_OO: ∀L. ≽ [0, 0] L.
-// qed.
-
-lemma sfr_abbr: ∀L,V,e. ≽ [0, e] L → ≽ [0, e + 1] L.ⓓV.
-#L #V #e #HL #K #H
-elim (lsubs_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
-lapply (HL … HLX) -HL -HLX /2 width=1/
-qed.
-
-lemma sfr_abbr_O: ∀L,V. ≽[0,1] L.ⓓV.
-#L #V
-@(sfr_abbr … 0) //
-qed.
-
-lemma sfr_skip: ∀I,L,V,d,e. ≽ [d, e] L → ≽ [d + 1, e] L.ⓑ{I}V.
-#I #L #V #d #e #HL #K #H
-elim (lsubs_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
-lapply (HL … HLX) -HL -HLX /2 width=1/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma sfr_inv_bind: ∀I,L,V,e. ≽ [0, e] L.ⓑ{I}V → 0 < e →
-                    ≽ [0, e - 1] L ∧ I = Abbr.
-#I #L #V #e #HL #He
-lapply (HL (L.ⓓV) ?) /2 width=1/ #H
-elim (lsubs_inv_abbr2 … H ?) -H // #K #_ #H destruct
-@conj // #L #HKL
-lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
-elim (lsubs_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
-qed-.
-
-lemma sfr_inv_skip: ∀I,L,V,d,e. ≽ [d, e] L.ⓑ{I}V → 0 < d → ≽ [d - 1, e] L.
-#I #L #V #d #e #HL #Hd #K #HLK
-lapply (HL (K.ⓑ{I}V) ?) -HL /2 width=1/ -HLK #H
-elim (lsubs_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
-qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
index 2efd002981b2a0080d24f72a2ed60c1dc8741c4e..ebce56c24e30c900fe9c043215a667dcb834d20f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
@@ -33,12 +33,12 @@ interpretation "parallel substritution (term)"
 
 (* Basic properties *********************************************************)
 
-lemma tps_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
+lemma tps_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
                        ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶ [d, e] T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
-  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
+  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -113,7 +113,7 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀i. d ≤ i →
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
   elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
   -Hdi -Hide >arith_c1x #T #HT1 #HT2
-  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+  lapply (tps_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
   -Hdi -Hide /3 width=5/
@@ -136,7 +136,7 @@ lemma tps_split_down: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
   elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
   -Hdi -Hide >arith_c1x #T #HT1 #HT2
-  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+  lapply (tps_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
   -Hdi -Hide /3 width=5/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
index a99b352ab60695dae784b9cfb31315aaa3cf50be..7e146c21ec4e4eb9a2cb8818ee4339101272fa72 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma
@@ -33,11 +33,11 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶ [d1, e1] T1 →
   ]
 | #L #a #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubr_trans … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
   elim (IHV01 … HV02) -V0 #V #HV1 #HV2
   elim (IHT01 … HT02) -T0 #T #HT1 #HT2
-  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
-  lapply (tps_lsubs_trans … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
+  lapply (tps_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+  lapply (tps_lsubr_trans … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
 | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   elim (IHV01 … HV02) -V0
@@ -71,8 +71,8 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 ▶ [d1, e1] T1 →
   elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2
   elim (IHT01 … HT02 ?) -T0
   [ -H #T #HT1 #HT2
-    lapply (tps_lsubs_trans … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
-    lapply (tps_lsubs_trans … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
+    lapply (tps_lsubr_trans … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
+    lapply (tps_lsubr_trans … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
   | -HV1 -HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %); elim H -H #H
     [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3 / is too slow *)
   ]
@@ -100,9 +100,9 @@ theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 ▶ [d, e] T0 →
   <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2 width=4/
 | #L #a #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
   elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
-  lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubr_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
   lapply (IHT10 … HT02 He) -T0 #HT12
-  lapply (tps_lsubs_trans … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
+  lapply (tps_lsubr_trans … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
 | #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
   elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1/
 ]
@@ -119,11 +119,11 @@ theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶ [d1, e1] T0 →
   <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /3 width=8/
 | #L #a #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  lapply (tps_lsubs_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubr_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
   elim (IHV10 … HV02 ?) -IHV10 -HV02 // #V
   elim (IHT10 … HT02 ?) -T0 /2 width=1/ #T #HT1 #HT2
-  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
-  lapply (tps_lsubs_trans … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
+  lapply (tps_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+  lapply (tps_lsubr_trans … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
 | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   elim (IHV10 … HV02 ?) -V0 //

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
index cde52912280c1f68471cf5aea095728ce69b5239..e0c736440f4503e41a284c6bad0b138a6bbb7d29 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma
@@ -31,7 +31,7 @@ lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 →
 lemma delift_refl_O2: ∀L,T,d. L ⊢ ▼*[d, 0] T ≡ T.
 /2 width=3/ qed.
 
-lemma delift_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 →
+lemma delift_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 →
                           ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2.
 #L1 #T1 #T2 #d #e * /3 width=3/
 qed.
@@ -52,7 +52,7 @@ lemma delift_bind: ∀a,I,L,V1,V2,T1,T2,d,e.
                    L ⊢ ▼*[d, e] V1 ≡ V2 → L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 →
                    L ⊢ ▼*[d, e] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
 #a #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
-lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubr_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
 qed.
 
 lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e.
@@ -82,7 +82,7 @@ lemma delift_inv_bind1: ∀a,I,L,V1,T1,U2,d,e. L ⊢ ▼*[d, e] ⓑ{a,I} V1. T1
 #a #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
 elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct
 elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2
-lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubr_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
 qed-.
 
 lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ▼*[d, e] ⓕ{I} V1. T1 ≡ U2 →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
index 1b82f79e3fa75294ba48c98c2baba4da04fa3abe..10657d3c343bfac077eaa49f5e5f1209d6715f09 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
@@ -38,11 +38,11 @@ interpretation "inverse basic relocation (term) alternative"
 
 (* Basic properties *********************************************************)
 
-lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
+lemma delifta_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
                            ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
 [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -60,10 +60,10 @@ lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼
   ]
 | * [ #a ] #I #V1 #T1 #Hn #X #d #e #H
   [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-    lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
+    lapply (delift_lsubr_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
     lapply (IH … HV12) -HV12 // #HV12
     lapply (IH … HT12) -IH -HT12 /2 width=1/ #HT12
-    lapply (delifta_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+    lapply (delifta_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
   | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
     lapply (IH … HV12) -HV12 //
     lapply (IH … HT12) -IH -HT12 // /2 width=1/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
index 7a654023a10ec9ff16c59d77447784d672b37fed..eb3dc1f28010f62d1000fb3d8a7c39813f2a4503 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
@@ -51,7 +51,7 @@ lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
 | #a #I #V1 #T1 #H #d #e #Hde #HL destruct
   elim (IH … V1 … Hde HL) // #V2 #HV12
   elim (IH (L.ⓑ{I}V1) T1 … (d+1) e ??) -IH // [2,3: /2 width=1/ ] -Hde -HL #T2 #HT12
-  lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
+  lapply (delift_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
 | #I #V1 #T1 #H #d #e #Hde #HL destruct
   elim (IH … V1 … Hde HL) // #V2 #HV12
   elim (IH … T1 … Hde HL) -IH -Hde -HL // /3 width=2/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
index ab281b92b97cb51f6146f238bc826301260f431a..74b898d69f8fbb293dc11ccf1d8aebe4f760b558 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
@@ -58,10 +58,10 @@ lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
   [ normalize /2 width=1/ | /2 width=6/ ]
 | * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
   [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
-    lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+    lapply (tpss_lsubr_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
     lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
     lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
-    lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+    lapply (tpss_lsubr_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
   | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
     lapply (IH … HVW2 … HL0) -HVW2 //
     lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
index dfcd35c73711860d3980013b8a28f4bc7c56674f..67c287e2bac0488a0fa5d3932918bbcdf06810f8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma
@@ -32,10 +32,10 @@ lemma ltpss_sn_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
   lapply (tpss_trans_eq … HV01 HV12) -V1 /2 width=6/
 | * [ #a ] #I #V2 #T2 #Hn #X #d #e #H #L0 #HL0 destruct
   [ elim (tpss_inv_bind1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
-    lapply (tpss_lsubs_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
+    lapply (tpss_lsubr_trans … HTU2 (L1. ⓑ{I} V2) ?) -HTU2 /2 width=1/ #HTU2
     lapply (IH … HVW2 … HL0) -HVW2 [ /2 width=2/ ] #HVW2
     lapply (IH … HTU2 (L0. ⓑ{I} V2) ?) -IH -HTU2 // /2 width=2/ -HL0 #HTU2
-    lapply (tpss_lsubs_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
+    lapply (tpss_lsubr_trans … HTU2 (L0. ⓑ{I} W2) ?) -HTU2 /2 width=1/
   | elim (tpss_inv_flat1 … H) -H #W2 #U2 #HVW2 #HTU2 #H destruct
     lapply (IH … HVW2 … HL0) -HVW2 //
     lapply (IH … HTU2 … HL0) -IH -HTU2 // -HL0 /2 width=1/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
index d23c1a255bac16a8d0cc7989733f6c52dc857d59..007613cf9562d1f69c5e4768b5f7365f0cde819d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma
@@ -52,7 +52,7 @@ lemma ltpss_sn_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
 | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
   elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
   elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 #T #HT2 #H
-  lapply (tpss_lsubs_trans … H (L0.ⓑ{I}V) ?) -H /2 width=1/ /3 width=5/
+  lapply (tpss_lsubr_trans … H (L0.ⓑ{I}V) ?) -H /2 width=1/ /3 width=5/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
   elim (IHVW2 … HL01) -IHVW2
   elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
@@ -93,7 +93,7 @@ lemma ltpss_sn_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
 | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
   elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
   elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 #T #HT2 #H
-  lapply (tpss_lsubs_trans … H (L1.ⓑ{I}W2) ?) -H /2 width=1/ /3 width=5/
+  lapply (tpss_lsubr_trans … H (L1.ⓑ{I}W2) ?) -H /2 width=1/ /3 width=5/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
   elim (IHVW2 … HL10) -IHVW2
   elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
index ba88f64e993e94c98beb5421b11fc4b93ec5d866..d2ce11a36e44219a0030b89e3ed7f27a1947a362 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -51,7 +51,7 @@ lemma tpss_strap2: ∀L,T1,T,T2,d,e.
                    L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
 /2 width=3/ qed.
 
-lemma tpss_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
+lemma tpss_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
                         ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
 /3 width=3/ qed.
 
@@ -67,7 +67,7 @@ lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 ▶* [d, e] V2 →
   | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
   ]
 | #V #V2 #_ #HV12 #IHV #a #I #T1 #T2 #HT12
-  lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
+  lapply (tpss_lsubr_trans … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
   lapply (IHV a … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
 ]
 qed.
@@ -144,7 +144,7 @@ lemma tpss_inv_bind1: ∀d,e,L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* [d, e] U
 [ /2 width=5/
 | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
   elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
-  lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+  lapply (tpss_lsubr_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
 ]
 qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
index 8f77dd0d0d8e3115a3dd805428e1b1d76ac5ed0e..8adea69bc85923fa5beb183f04753632b65ea823 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
@@ -35,12 +35,12 @@ interpretation "parallel unfold (term) alternative"
 
 (* Basic properties *********************************************************)
 
-lemma tpssa_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
+lemma tpssa_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
                          ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -62,10 +62,10 @@ lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 ▶▶* [d, e] T →
   elim (tps_inv_lift1_be … H … H0LK … HVW2 ? ?) -H -H0LK -HVW2 // /3 width=6/
 | #L #a #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
   elim (tps_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
-  lapply (tps_lsubs_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
+  lapply (tps_lsubr_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
   lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
   lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
-  lapply (tpssa_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+  lapply (tpssa_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
 | #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
   elim (tps_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1/
 ]

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 00db0e50b9eaad0b7cfbfa0a96ddb900651865b3..4139f7344348c7090470b74ad3a9daebffb7c187 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -239,7 +239,7 @@ table {
           }
         ]
         [ { "local env. ref. for substitution" * } {
-             [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ]
+             [ "lsubr ( ? ≼[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ]
           }
         ]
         [ { "restricted structural predecessor for closures" * } {