From faae92d508117105572e028aa454db8ba8be5291 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 17 Mar 2013 19:51:19 +0000 Subject: [PATCH] notational change for lsubr: now looks like the other refinements for local environments --- .../lambdadelta/basic_2/computation/cprs.ma | 2 +- .../lambdadelta/basic_2/dynamic/lsubsv.ma | 4 +- .../basic_2/equivalence/cpcs_cpcs.ma | 2 +- .../lambdadelta/basic_2/equivalence/lsubss.ma | 4 +- .../contribs/lambdadelta/basic_2/notation.ma | 2 +- .../lambdadelta/basic_2/reducibility/cpr.ma | 2 +- .../lambdadelta/basic_2/substitution/ldrop.ma | 4 +- .../lambdadelta/basic_2/substitution/lsubr.ma | 64 +++++++++---------- .../lambdadelta/basic_2/substitution/tps.ma | 2 +- .../lambdadelta/basic_2/unfold/delift.ma | 2 +- .../lambdadelta/basic_2/unfold/delift_alt.ma | 2 +- .../lambdadelta/basic_2/unfold/tpss.ma | 2 +- .../lambdadelta/basic_2/unfold/tpss_alt.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 14 files changed, 48 insertions(+), 48 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index ccfa79011..228f9450c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -60,7 +60,7 @@ lemma cprs_strap2: ∀L,T1,T,T2. (* Note: it does not hold replacing |L1| with |L2| *) lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 → - ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2. + ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index 8df6fb710..fe0359314 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -101,11 +101,11 @@ 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_lsubr1: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L1|] L2. +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_lsubr2: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L2|] L2. +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-. 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 cbc1ea3da..5d0643879 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma @@ -165,7 +165,7 @@ lemma cpcs_beta_dx_tpr_rev: ∀a,L,V1,V2,W,T1,T2. (* Note: it does not hold replacing |L1| with |L2| *) lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 → - ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ 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_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma index ac8f5373c..364f06ade 100644 --- 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_lsubr1: ∀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_lsubr2: ∀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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 8745932e9..de8221468 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -146,7 +146,7 @@ notation "hvbox( ⇧ [ term 46 d , break term 46 e ] break term 46 T1 ≡ break non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. -notation "hvbox( T1 break ≼ [ term 46 d , break term 46 e ] break term 46 T2 )" +notation "hvbox( T1 break ⊑ [ term 46 d , break term 46 e ] break term 46 T2 )" non associative with precedence 45 for @{ 'SubEq $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma index 2317250cc..d82299c38 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma @@ -55,7 +55,7 @@ qed. (* Note: it does not hold replacing |L1| with |L2| *) (* Basic_1: was only: pr2_change *) lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 → - ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2. + ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2. #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma index 7e7ac3c54..f1bc18f7d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma @@ -186,10 +186,10 @@ lemma ldrop_O1_lt: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V. ] qed. -lemma ldrop_lsubr_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 & + ∃∃K1. K1 ⊑ [0, d + e - i - 1] K2 & ⇩[0, i] L1 ≡ K1. ⓓV. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e [ #d #e #K1 #V #i #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma index 2a4e43271..89359533a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma @@ -33,35 +33,35 @@ interpretation 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. + ∀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. +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. +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. +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. +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. +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. +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/ @@ -78,7 +78,7 @@ qed. (* Basic inversion lemmas ***************************************************) -fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ → +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/ @@ -89,13 +89,13 @@ fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ → ] qed. -lemma lsubr_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 → +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 → +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. + ∃∃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 @@ -108,11 +108,11 @@ fact lsubr_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] 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. +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 = ⋆ → +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/ @@ -123,13 +123,13 @@ fact lsubr_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ → ] qed. -lemma lsubr_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ → +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 → +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. + ∃∃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 @@ -140,13 +140,13 @@ fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] 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. +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 → +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. + ∃∃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 @@ -159,13 +159,13 @@ fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] 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. +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 → +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 [ // @@ -176,10 +176,10 @@ fact lsubr_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] qed. -lemma lsubr_fwd_length_full1: ∀L1,L2. L1 ≼ [0, |L1|] L2 → |L1| ≤ |L2|. +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 → +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 [ // @@ -190,5 +190,5 @@ fact lsubr_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] qed. -lemma lsubr_fwd_length_full2: ∀L1,L2. L1 ≼ [0, |L2|] L2 → |L2| ≤ |L1|. +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/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma index ebce56c24..af450e34d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma @@ -34,7 +34,7 @@ interpretation "parallel substritution (term)" (* Basic properties *********************************************************) lemma tps_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 → - ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ 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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma index e0c736440..95284abc7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma @@ -32,7 +32,7 @@ lemma delift_refl_O2: ∀L,T,d. L ⊢ ▼*[d, 0] T ≡ T. /2 width=3/ qed. lemma delift_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 → - ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2. + ∀L2. L2 ⊑ [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2. #L1 #T1 #T2 #d #e * /3 width=3/ qed. 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 10657d3c3..b9322cd1e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma @@ -39,7 +39,7 @@ interpretation "inverse basic relocation (term) alternative" (* Basic properties *********************************************************) lemma delifta_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 → - ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼▼*[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_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma index d2ce11a36..1fdae13f4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma @@ -52,7 +52,7 @@ lemma tpss_strap2: ∀L,T1,T,T2,d,e. /2 width=3/ qed. lemma tpss_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 → - ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2. + ∀L2. L2 ⊑ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2. /3 width=3/ qed. lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T. 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 8adea69bc..6fe188a7c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma @@ -36,7 +36,7 @@ interpretation "parallel unfold (term) alternative" (* Basic properties *********************************************************) lemma tpssa_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 → - ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ 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 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 4139f7344..7ebbbca7f 100644 --- 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" * } { - [ "lsubr ( ? ≼[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ] + [ "lsubr ( ? ⊑[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ] } ] [ { "restricted structural predecessor for closures" * } { -- 2.39.2