From bd7183da46c7cb0f389cda40955b270c03b57a4b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 17 Mar 2013 17:43:13 +0000 Subject: [PATCH] lsubs renamed as lsubr --- .../lambdadelta/basic_2/computation/cprs.ma | 2 +- .../basic_2/computation/cprs_cprs.ma | 4 +- .../lambdadelta/basic_2/dynamic/lsubsv.ma | 8 +-- .../basic_2/dynamic/lsubsv_cpcs.ma | 2 +- .../lambdadelta/basic_2/dynamic/snv_ltpr.ma | 2 +- .../basic_2/dynamic/snv_ssta_ltpr.ma | 2 +- .../basic_2/equivalence/cpcs_cpcs.ma | 6 +- .../lambdadelta/basic_2/equivalence/lsubss.ma | 6 +- .../basic_2/equivalence/lsubss_cpcs.ma | 2 +- .../basic_2/reducibility/cnf_cif.ma | 2 +- .../lambdadelta/basic_2/reducibility/cpr.ma | 4 +- .../basic_2/reducibility/cpr_cpr.ma | 2 +- .../basic_2/reducibility/cpr_lift.ma | 12 ++-- .../basic_2/reducibility/ltpr_aaa.ma | 2 +- .../basic_2/reducibility/tpr_tpss.ma | 8 +-- .../lambdadelta/basic_2/substitution/ldrop.ma | 4 +- .../basic_2/substitution/ldrop_sfr.ma | 4 +- .../substitution/{lsubs.ma => lsubr.ma} | 64 +++++++++---------- .../{lsubs_sfr.ma => lsubr_sfr.ma} | 16 ++--- .../lambdadelta/basic_2/substitution/tps.ma | 8 +-- .../basic_2/substitution/tps_tps.ma | 20 +++--- .../lambdadelta/basic_2/unfold/delift.ma | 6 +- .../lambdadelta/basic_2/unfold/delift_alt.ma | 8 +-- .../lambdadelta/basic_2/unfold/delift_lift.ma | 2 +- .../basic_2/unfold/ltpss_dx_ltpss_dx.ma | 4 +- .../basic_2/unfold/ltpss_sn_ltpss_sn.ma | 4 +- .../basic_2/unfold/ltpss_sn_tpss.ma | 4 +- .../lambdadelta/basic_2/unfold/tpss.ma | 6 +- .../lambdadelta/basic_2/unfold/tpss_alt.ma | 8 +-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 30 files changed, 112 insertions(+), 112 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/substitution/{lsubs.ma => lsubr.ma} (74%) rename matita/matita/contribs/lambdadelta/basic_2/substitution/{lsubs_sfr.ma => lsubr_sfr.ma} (84%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index e20ce0559..ccfa79011 100644 --- 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 c89fab769..75f74caad 100644 --- 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 089dbed26..8df6fb710 100644 --- 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 15acdc943..750c71fdc 100644 --- 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 79ca41081..17ae5d326 100644 --- 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 1cd5ead77..d7a40613e 100644 --- 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 a31853a7f..cbc1ea3da 100644 --- 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 5898d4ecf..ac8f5373c 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_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 cfb7372a4..cbddc65e9 100644 --- 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 8ee507cc1..5a1ae5a5b 100644 --- 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 56e10d392..2317250cc 100644 --- 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 d0738e4c4..039dc29e0 100644 --- 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 (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 → +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 lsubs_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d → +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 lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → +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 lsubs_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/ ] qed. -lemma TC_lsubs_trans: ∀S,R. lsubs_trans S R → lsubs_trans S (λL. (TC … (R L))). +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 @@ -78,7 +78,7 @@ qed. (* Basic inversion lemmas ***************************************************) -fact lsubs_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,11 +89,11 @@ fact lsubs_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ → ] qed. -lemma lsubs_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 lsubs_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. #L1 #L2 #d #e * -L1 -L2 -d -e @@ -108,11 +108,11 @@ fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] qed. -lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d → +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 lsubs_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,11 +123,11 @@ fact lsubs_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ → ] qed. -lemma lsubs_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 lsubs_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. #L1 #L2 #d #e * -L1 -L2 -d -e @@ -140,11 +140,11 @@ fact lsubs_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] qed. -lemma lsubs_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e → +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 lsubs_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. #L1 #L2 #d #e * -L1 -L2 -d -e @@ -159,13 +159,13 @@ fact lsubs_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] qed. -lemma lsubs_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ≼ [d, e] K2.ⓑ{I2}V2 → 0 < d → +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 lsubs_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 lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] qed. -lemma lsubs_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 lsubs_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 lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] qed. -lemma lsubs_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/lsubs_sfr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma similarity index 84% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma index b71f25e51..e35a371bc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs_sfr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_sfr.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lsubs.ma". +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 … (lsubs d e) (lsubs d e …). + λd,e. NF_sn … (lsubr d e) (lsubr d e …). interpretation "local environment full refinement (substitution)" @@ -28,7 +28,7 @@ interpretation lemma sfr_atom: ∀d,e. ≽ [d, e] ⋆. #d #e #L #H -elim (lsubs_inv_atom2 … H) -H +elim (lsubr_inv_atom2 … H) -H [ #H destruct // | * #H1 #H2 destruct // ] @@ -39,7 +39,7 @@ lemma sfr_OO: ∀L. ≽ [0, 0] L. 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 // 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 a99b352ab..7e146c21e 100644 --- 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 cde529122..e0c736440 100644 --- 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 1b82f79e3..10657d3c3 100644 --- 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 7a654023a..eb3dc1f28 100644 --- 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 ab281b92b..74b898d69 100644 --- 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 dfcd35c73..67c287e2b 100644 --- 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 d23c1a255..007613cf9 100644 --- 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 ba88f64e9..d2ce11a36 100644 --- 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 8f77dd0d0..8adea69bc 100644 --- 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 00db0e50b..4139f7344 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" * } { - [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ] + [ "lsubr ( ? ≼[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ] } ] [ { "restricted structural predecessor for closures" * } { -- 2.39.2