- first results on cpx (dericed from those on cpg)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpg.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
index 22c671d90e4aeb3afeb82a2ff73b5bcd34905a8a..5dab2812e3d6bc5c4945551f446b6fcce8698787 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
@@ -20,14 +20,14 @@ include "basic_2/grammar/genv.ma".
 include "basic_2/relocation/lifts.ma".
 include "basic_2/static/sh.ma".
 
-(* CONTEXT-SENSITIVE GENERIC PARALLEL RT-TRANSITION FOR TERMS ***************)
+(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
 
 (* avtivate genv *)
 inductive cpg (h): rtc → relation4 genv lenv term term ≝
 | cpg_atom : ∀I,G,L. cpg h (𝟘𝟘) G L (⓪{I}) (⓪{I})
 | cpg_ess  : ∀G,L,s. cpg h (𝟘𝟙) G L (⋆s) (⋆(next h s))
 | cpg_delta: ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
-             ⬆*[1] V2 ≡ W2 → cpg h (↓c) G (L.ⓓV1) (#0) W2
+             ⬆*[1] V2 ≡ W2 → cpg h c G (L.ⓓV1) (#0) W2
 | cpg_ell  : ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
              ⬆*[1] V2 ≡ W2 → cpg h ((↓c)+𝟘𝟙) G (L.ⓛV1) (#0) W2
 | cpg_lref : ∀c,I,G,L,V,T,U,i. cpg h c G L (#i) T → 
@@ -52,7 +52,7 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝
 .
 
 interpretation
-   "context-sensitive generic parallel rt-transition (term)"
+   "counted context-sensitive parallel rt-transition (term)"
    'PRed c h G L T1 T2 = (cpg h c G L T1 T2).
 
 (* Basic properties *********************************************************)
@@ -73,7 +73,7 @@ fact cpg_inv_atom1_aux: ∀c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[c, h] T2 → ∀
                         ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
                          | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
                          | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
-                                         L = K.ⓓV1 & J = LRef 0 & c = ↓cV
+                                         L = K.ⓓV1 & J = LRef 0 & c = cV
                          | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                          L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
                          | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[c, h] T & ⬆*[1] T ≡ T2 &
@@ -98,7 +98,7 @@ lemma cpg_inv_atom1: ∀c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[c, h] T2 →
                      ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
                       | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
                       | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
-                                      L = K.ⓓV1 & J = LRef 0 & c = ↓cV
+                                      L = K.ⓓV1 & J = LRef 0 & c = cV
                       | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
                       | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[c, h] T & ⬆*[1] T ≡ T2 &
@@ -118,7 +118,7 @@ qed-.
 lemma cpg_inv_zero1: ∀c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[c, h] T2 →
                      ∨∨ (T2 = #0 ∧ c = 𝟘𝟘)
                       | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
-                                      L = K.ⓓV1 & c = ↓cV
+                                      L = K.ⓓV1 & c = cV
                       | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓛV1 & c = (↓cV)+𝟘𝟙.
 #c #h #G #L #T2 #H
@@ -266,10 +266,10 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma cpg_fwd_bind1_minus: ∀c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[c, h] T → ∀b.
-                           ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,I}V1.T1 ➡[c, h] ⓑ{b,I}V2.T2 &
+lemma cpg_fwd_bind1_minus: ∀c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[c, h] T → ∀p.
+                           ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[c, h] ⓑ{p,I}V2.T2 &
                                     T = -ⓑ{I}V2.T2.
-#c #h #I #G #L #V1 #T1 #T #H #b elim (cpg_inv_bind1 … H) -H *
+#c #h #I #G #L #V1 #T1 #T #H #p elim (cpg_inv_bind1 … H) -H *
 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct /3 width=4 by cpg_bind, ex2_2_intro/
 | #c #T2 #_ #_ #H destruct
 ]