X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fcpy_lift.ma;h=991d4db29badad333a60668aeb46eb1a1a19058b;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=78318917befb3801cfd6b55eb37eea554edcf100;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma index 78318917b..991d4db29 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma @@ -21,8 +21,8 @@ include "basic_2/substitution/cpy.ma". (* Basic_1: was: subst1_lift_lt *) lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 → - ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → - ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → + ∀L,U1,U2,s,d,e. ⬇[s, d, e] L ≡ K → + ⬆[d, e] T1 ≡ U1 → ⬆[d, e] T2 ≡ U2 → dt + et ≤ d → ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et [ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ @@ -47,8 +47,8 @@ lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 → qed-. lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 → - ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → - ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → + ∀L,U1,U2,s,d,e. ⬇[s, d, e] L ≡ K → + ⬆[d, e] T1 ≡ U1 → ⬆[d, e] T2 ≡ U2 → dt ≤ d → d ≤ dt + et → ⦃G, L⦄ ⊢ U1 ▶[dt, et + e] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et [ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ #_ @@ -81,8 +81,8 @@ qed-. (* Basic_1: was: subst1_lift_ge *) lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 → - ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → - ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → + ∀L,U1,U2,s,d,e. ⬇[s, d, e] L ≡ K → + ⬆[d, e] T1 ≡ U1 → ⬆[d, e] T2 ≡ U2 → d ≤ dt → ⦃G, L⦄ ⊢ U1 ▶[dt+e, et] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et [ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ @@ -109,9 +109,9 @@ qed-. (* Basic_1: was: subst1_gen_lift_lt *) lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → dt + et ≤ d → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et [ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ @@ -138,9 +138,9 @@ lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → qed-. lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → dt ≤ d → yinj d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, et-e] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, et-e] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et [ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ @@ -178,9 +178,9 @@ qed-. (* Basic_1: was: subst1_gen_lift_ge *) lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → yinj d + e ≤ dt → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt-e, et] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt-e, et] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et [ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ @@ -215,9 +215,9 @@ qed-. (* Advanced inversion lemmas on relocation ***********************************) lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[d, dt + et - (yinj d + e)] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (cpy_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2 lapply (cpy_weak … HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1 @@ -226,9 +226,9 @@ elim (cpy_inv_lift1_ge … HU2 … HLK … HTU1) -U -L /2 width=3 by ex2_intro/ qed-. lemma cpy_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → dt ≤ d → dt + et ≤ yinj d + e → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, d-dt] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, d-dt] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde lapply (cpy_weak … HU12 dt (d+e-dt) ? ?) -HU12 // [ >ymax_pre_sn_comm /2 width=1 by yle_plus_dx1_trans/ ] -Hdetde #HU12 @@ -236,9 +236,9 @@ elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) -U1 -L /2 width=3 by ex2_intro qed-. lemma cpy_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → - ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + ∀K,s,d,e. ⬇[s, d, e] L ≡ K → ∀T1. ⬆[d, e] T1 ≡ U1 → dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, d - dt] T2 & ⬆[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde elim (cpy_split_up … HU12 d) -HU12 // #U #HU1 #HU2 elim (cpy_inv_lift1_le … HU1 … HLK … HTU1) -U1