notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / cpys_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
index d69de694e279bb1b82f7e9348b504a0e9578ac27..d21e9cce0ffd1ebf8a6c597fbac18c4d1fa0e1bc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
@@ -21,8 +21,8 @@ include "basic_2/multiple/cpys.ma".
 
 lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e.
                   d ≤ yinj i → i < d + e →
-                  â\87©[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ⫰(d+e-i)] U1 →
-                  â\88\80U2. â\87§[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] U2.
+                  â¬\87[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ⫰(d+e-i)] U1 →
+                  â\88\80U2. â¬\86[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] U2.
 #I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind … H) -U1
 [ /3 width=5 by cpy_cpys, cpy_subst/
 | #U #U1 #_ #HU1 #IHU #U2 #HU12
@@ -38,8 +38,8 @@ qed.
 
 lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d.
                      d ≤ yinj i →
-                     â\87©[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ∞] U1 →
-                     â\88\80U2. â\87§[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, ∞] U2.
+                     â¬\87[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ∞] U1 →
+                     â\88\80U2. â¬\86[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, ∞] U2.
 #I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12
 @(cpys_subst … HLK … HU12) >yminus_Y_inj //
 qed.
@@ -49,9 +49,9 @@ qed.
 lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*[d, e] T2 →
                       T2 = ⓪{I} ∨
                       ∃∃J,K,V1,V2,i. d ≤ yinj i & i < d + e &
-                                    â\87©[i] L ≡ K.ⓑ{J}V1 &
+                                    â¬\87[i] L ≡ K.ⓑ{J}V1 &
                                      ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 &
-                                     â\87§[O, i+1] V2 ≡ T2 &
+                                     â¬\86[O, i+1] V2 ≡ T2 &
                                      I = LRef i.
 #I #G #L #T2 #d #e #H @(cpys_ind … H) -T2
 [ /2 width=1 by or_introl/
@@ -70,24 +70,24 @@ qed-.
 lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 →
                       T2 = #i ∨
                       ∃∃I,K,V1,V2. d ≤ i & i < d + e &
-                                   â\87©[i] L ≡ K.ⓑ{I}V1 &
+                                   â¬\87[i] L ≡ K.ⓑ{I}V1 &
                                    ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 &
-                                   â\87§[O, i+1] V2 ≡ T2.
+                                   â¬\86[O, i+1] V2 ≡ T2.
 #G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/
 * #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/
 qed-.
 
 lemma cpys_inv_lref1_Y2: ∀G,L,T2,i,d. ⦃G, L⦄ ⊢ #i ▶*[d, ∞] T2 →
                          T2 = #i ∨
-                         â\88\83â\88\83I,K,V1,V2. d â\89¤ i & â\87©[i] L ≡ K.ⓑ{I}V1 &
-                                      â¦\83G, Kâ¦\84 â\8a¢ V1 â\96¶*[0, â\88\9e] V2 & â\87§[O, i+1] V2 ≡ T2.
+                         â\88\83â\88\83I,K,V1,V2. d â\89¤ i & â¬\87[i] L ≡ K.ⓑ{I}V1 &
+                                      â¦\83G, Kâ¦\84 â\8a¢ V1 â\96¶*[0, â\88\9e] V2 & â¬\86[O, i+1] V2 ≡ T2.
 #G #L #T2 #i #d #H elim (cpys_inv_lref1 … H) -H /2 width=1 by or_introl/
 * >yminus_Y_inj /3 width=7 by or_intror, ex4_4_intro/
 qed-.
 
 lemma cpys_inv_lref1_drop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 →
-                            â\88\80I,K,V1. â\87©[i] L ≡ K.ⓑ{I}V1 →
-                            â\88\80V2. â\87§[O, i+1] V2 ≡ T2 →
+                            â\88\80I,K,V1. â¬\87[i] L ≡ K.ⓑ{I}V1 →
+                            â\88\80V2. â¬\86[O, i+1] V2 ≡ T2 →
                             ∧∧ ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2
                              & d ≤ i
                              & i < d + e.
@@ -103,8 +103,8 @@ qed-.
 (* Properties on relocation *************************************************)
 
 lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 →
-                    â\88\80L,U1,s,d,e. dt + et â\89¤ yinj d â\86\92 â\87©[s, d, e] L ≡ K →
-                    â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87§[d, e] T2 ≡ U2 →
+                    â\88\80L,U1,s,d,e. dt + et â\89¤ yinj d â\86\92 â¬\87[s, d, e] L ≡ K →
+                    â¬\86[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â¬\86[d, e] T2 ≡ U2 →
                     ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2.
 #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
@@ -117,8 +117,8 @@ qed-.
 
 lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 →
                     ∀L,U1,s,d,e. dt ≤ yinj d → d ≤ dt + et →
-                    â\87©[s, d, e] L â\89¡ K â\86\92 â\87§[d, e] T1 ≡ U1 →
-                    â\88\80U2. â\87§[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[dt, et + e] U2.
+                    â¬\87[s, d, e] L â\89¡ K â\86\92 â¬\86[d, e] T1 ≡ U1 →
+                    â\88\80U2. â¬\86[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[dt, et + e] U2.
 #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
@@ -129,8 +129,8 @@ lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 →
 qed-.
 
 lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 →
-                    â\88\80L,U1,s,d,e. yinj d â\89¤ dt â\86\92 â\87©[s, d, e] L ≡ K →
-                    â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87§[d, e] T2 ≡ U2 →
+                    â\88\80L,U1,s,d,e. yinj d â\89¤ dt â\86\92 â¬\87[s, d, e] L ≡ K →
+                    â¬\86[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â¬\86[d, e] T2 ≡ U2 →
                     ⦃G, L⦄ ⊢ U1 ▶*[dt+e, et] U2.
 #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
@@ -144,9 +144,9 @@ qed-.
 (* Inversion lemmas for relocation ******************************************)
 
 lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
-                         â\88\80K,s,d,e. â\87©[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â\87§[d, e] T1 ≡ U1 →
+                         â\88\80K,s,d,e. â¬\87[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â¬\86[d, e] T1 ≡ U1 →
                          dt + et ≤ d →
-                         â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt, et] T2 & â\87§[d, e] T2 ≡ U2.
+                         â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt, et] T2 & â¬\86[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -155,9 +155,9 @@ lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 
 qed-.
 
 lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
-                         â\88\80K,s,d,e. â\87©[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â\87§[d, e] T1 ≡ U1 →
+                         â\88\80K,s,d,e. â¬\87[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â¬\86[d, e] T1 ≡ U1 →
                          dt ≤ d → yinj d + e ≤ dt + et →
-                         â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt, et - e] T2 & â\87§[d, e] T2 ≡ U2.
+                         â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt, et - e] T2 & â¬\86[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -166,9 +166,9 @@ lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 
 qed-.
 
 lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
-                         â\88\80K,s,d,e. â\87©[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â\87§[d, e] T1 ≡ U1 →
+                         â\88\80K,s,d,e. â¬\87[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â¬\86[d, e] T1 ≡ U1 →
                          yinj d + e ≤ dt →
-                         â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt - e, et] T2 & â\87§[d, e] T2 ≡ U2.
+                         â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt - e, et] T2 & â¬\86[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -179,10 +179,10 @@ qed-.
 (* Advanced inversion lemmas on relocation **********************************)
 
 lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
-                            â\88\80K,s,d,e. â\87©[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â\87§[d, e] T1 ≡ U1 →
+                            â\88\80K,s,d,e. â¬\87[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â¬\86[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 &
-                                 â\87§[d, e] T2 ≡ U2.
+                                 â¬\86[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -191,9 +191,9 @@ lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U
 qed-.
 
 lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
-                            â\88\80K,s,d,e. â\87©[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â\87§[d, e] T1 ≡ U1 →
+                            â\88\80K,s,d,e. â¬\87[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â¬\86[d, e] T1 ≡ U1 →
                             dt ≤ d → dt + et ≤ yinj d + e →
-                            â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt, d - dt] T2 & â\87§[d, e] T2 ≡ U2.
+                            â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt, d - dt] T2 & â¬\86[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -202,9 +202,9 @@ lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U
 qed-.
 
 lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
-                            â\88\80K,s,d,e. â\87©[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â\87§[d, e] T1 ≡ U1 →
+                            â\88\80K,s,d,e. â¬\87[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â¬\86[d, e] T1 ≡ U1 →
                             dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e →
-                            â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt, d - dt] T2 & â\87§[d, e] T2 ≡ U2.
+                            â\88\83â\88\83T2. â¦\83G, Kâ¦\84 â\8a¢ T1 â\96¶*[dt, d - dt] T2 & â¬\86[d, e] T2 ≡ U2.
 #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -213,9 +213,9 @@ lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U
 qed-.
 
 lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,d,e. ⦃G, L⦄ ⊢ W1 ▶*[d, e] W2 →
-                            â\88\80K,V1,i. â\87©[i+1] L â\89¡ K â\86\92 â\87§[O, i+1] V1 ≡ W1 → 
+                            â\88\80K,V1,i. â¬\87[i+1] L â\89¡ K â\86\92 â¬\86[O, i+1] V1 ≡ W1 → 
                             d ≤ yinj i → i < d + e →
-                            â\88\83â\88\83V2.  â¦\83G, Kâ¦\84 â\8a¢ V1 â\96¶*[O, â«°(d+e-i)] V2 & â\87§[O, i+1] V2 ≡ W2.
+                            â\88\83â\88\83V2.  â¦\83G, Kâ¦\84 â\8a¢ V1 â\96¶*[O, â«°(d+e-i)] V2 & â¬\86[O, i+1] V2 ≡ W2.
 #G #L #W1 #W2 #d #e #HW12 #K #V1 #i #HLK #HVW1 #Hdi #Hide
 elim (cpys_inv_lift1_ge_up … HW12 … HLK … HVW1 ? ? ?) //
 >yplus_O1 <yplus_inj >yplus_SO2