include "ground_2/steps/rtc_shift.ma".
include "ground_2/steps/rtc_plus.ma".
-include "basic_2/notation/relations/pred_6.ma".
+include "basic_2/notation/relations/predty_6.ma".
include "basic_2/grammar/lenv.ma".
include "basic_2/grammar/genv.ma".
include "basic_2/relocation/lifts.ma".
interpretation
"counted context-sensitive parallel rt-transition (term)"
- 'PRed c h G L T1 T2 = (cpg h c G L T1 T2).
+ 'PRedTy c h G L T1 T2 = (cpg h c G L T1 T2).
(* Basic properties *********************************************************)
(* Note: this is "∀h,g,L. reflexive … (cpg h (𝟘𝟘) L)" *)
-lemma cpg_refl: â\88\80h,G,T,L. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡[𝟘𝟘, h] T.
+lemma cpg_refl: â\88\80h,G,T,L. â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[𝟘𝟘, h] T.
#h #G #T elim T -T // * /2 width=1 by cpg_bind, cpg_flat/
qed.
-lemma cpg_pair_sn: â\88\80c,h,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[c, h] V2 →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â\9e¡[↓c, h] ②{I}V2.T.
+lemma cpg_pair_sn: â\88\80c,h,I,G,L,V1,V2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[c, h] V2 →
+ â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ â\91¡{I}V1.T â¬\88[↓c, h] ②{I}V2.T.
#c #h * /2 width=1 by cpg_bind, cpg_flat/
qed.
(* Basic inversion lemmas ***************************************************)
-fact cpg_inv_atom1_aux: â\88\80c,h,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[c, h] T2 → ∀J. T1 = ⓪{J} →
+fact cpg_inv_atom1_aux: â\88\80c,h,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[c, h] T2 → ∀J. T1 = ⓪{J} →
∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘
| ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & J = LRef 0 & c = cV
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
- | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 &
+ | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[c, h] T & ⬆*[1] T ≡ T2 &
L = K.ⓑ{I}V & J = LRef (⫯i).
#c #h #G #L #T1 #T2 * -c -G -L -T1 -T2
[ #I #G #L #J #H destruct /3 width=1 by or5_intro0, conj/
]
qed-.
-lemma cpg_inv_atom1: â\88\80c,h,J,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{J} â\9e¡[c, h] T2 →
+lemma cpg_inv_atom1: â\88\80c,h,J,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93ª{J} â¬\88[c, h] T2 →
∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘
| ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & J = LRef 0 & c = cV
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
- | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 &
+ | â\88\83â\88\83I,K,V,T,i. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[c, h] T & ⬆*[1] T ≡ T2 &
L = K.ⓑ{I}V & J = LRef (⫯i).
/2 width=3 by cpg_inv_atom1_aux/ qed-.
-lemma cpg_inv_sort1: â\88\80c,h,G,L,T2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â\9e¡[c, h] T2 →
+lemma cpg_inv_sort1: â\88\80c,h,G,L,T2,s. â¦\83G, Lâ¦\84 â\8a¢ â\8b\86s â¬\88[c, h] T2 →
(T2 = ⋆s ∧ c = 𝟘𝟘) ∨ (T2 = ⋆(next h s) ∧ c = 𝟘𝟙).
#c #h #G #L #T2 #s #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
]
qed-.
-lemma cpg_inv_zero1: â\88\80c,h,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #0 â\9e¡[c, h] T2 →
+lemma cpg_inv_zero1: â\88\80c,h,G,L,T2. â¦\83G, Lâ¦\84 â\8a¢ #0 â¬\88[c, h] T2 →
∨∨ (T2 = #0 ∧ c = 𝟘𝟘)
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & c = cV
- | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | â\88\83â\88\83cV,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & c = (↓cV)+𝟘𝟙.
#c #h #G #L #T2 #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/
]
qed-.
-lemma cpg_inv_lref1: â\88\80c,h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i â\9e¡[c, h] T2 →
+lemma cpg_inv_lref1: â\88\80c,h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i â¬\88[c, h] T2 →
(T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨
- â\88\83â\88\83I,K,V,T. â¦\83G, Kâ¦\84 â\8a¢ #i â\9e¡[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
+ â\88\83â\88\83I,K,V,T. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
#c #h #G #L #T2 #i #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
[ #s #H destruct
]
qed-.
-lemma cpg_inv_gref1: â\88\80c,h,G,L,T2,l. â¦\83G, Lâ¦\84 â\8a¢ §l â\9e¡[c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
+lemma cpg_inv_gref1: â\88\80c,h,G,L,T2,l. â¦\83G, Lâ¦\84 â\8a¢ §l â¬\88[c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
#c #h #G #L #T2 #l #H
elim (cpg_inv_atom1 … H) -H * /2 width=1 by conj/
[ #s #H destruct
]
qed-.
-fact cpg_inv_bind1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡[c, h] U2 →
+fact cpg_inv_bind1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â¬\88[c, h] U2 →
∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → (
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\91{J}V1â¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\91{J}V1â¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓑ{p,J}V2.T2 & c = (↓cV)+cT
) ∨
- â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ U1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+ â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ U1 â¬\88[cT, h] T & ⬆*[1] U2 ≡ T &
p = true & J = Abbr & c = (↓cT)+𝟙𝟘.
#c #h #G #L #U #U2 * -c -G -L -U -U2
[ #I #G #L #q #J #W #U1 #H destruct
]
qed-.
-lemma cpg_inv_bind1: â\88\80c,h,p,I,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[c, h] U2 → (
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_bind1: â\88\80c,h,p,I,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[c, h] U2 → (
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\91{I}V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U2 = ⓑ{p,I}V2.T2 & c = (↓cV)+cT
) ∨
- â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+ â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T & ⬆*[1] U2 ≡ T &
p = true & I = Abbr & c = (↓cT)+𝟙𝟘.
/2 width=3 by cpg_inv_bind1_aux/ qed-.
-lemma cpg_inv_abbr1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 â\9e¡[c, h] U2 → (
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_abbr1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V1.T1 â¬\88[c, h] U2 → (
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U2 = ⓓ{p}V2.T2 & c = (↓cV)+cT
) ∨
- â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T & ⬆*[1] U2 ≡ T &
+ â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[cT, h] T & ⬆*[1] U2 ≡ T &
p = true & c = (↓cT)+𝟙𝟘.
#c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
/3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/
qed-.
-lemma cpg_inv_abst1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 â\9e¡[c, h] U2 →
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, L.â\93\9bV1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_abst1: â\88\80c,h,p,G,L,V1,T1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p}V1.T1 â¬\88[c, h] U2 →
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, L.â\93\9bV1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U2 = ⓛ{p}V2.T2 & c = (↓cV)+cT.
#c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
[ /3 width=8 by ex4_4_intro/
]
qed-.
-fact cpg_inv_flat1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â\9e¡[c, h] U2 →
+fact cpg_inv_flat1_aux: â\88\80c,h,G,L,U,U2. â¦\83G, Lâ¦\84 â\8a¢ U â¬\88[c, h] U2 →
∀J,V1,U1. U = ⓕ{J}V1.U1 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓕ{J}V2.T2 & c = (↓cV)+cT
- | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & J = Cast & c = (↓cT)+𝟙𝟘
- | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & J = Cast & c = (↓cV)+𝟘𝟙
- | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & J = Cast & c = (↓cT)+𝟙𝟘
+ | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] U2 & J = Cast & c = (↓cV)+𝟘𝟙
+ | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
- | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
#c #h #G #L #U #U2 * -c -G -L -U -U2
[ #I #G #L #J #W #U1 #H destruct
]
qed-.
-lemma cpg_inv_flat1: â\88\80c,h,I,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 â\9e¡[c, h] U2 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_flat1: â\88\80c,h,I,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 â¬\88[c, h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓕ{I}V2.T2 & c = (↓cV)+cT
- | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & I = Cast & c = (↓cT)+𝟙𝟘
- | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & I = Cast & c = (↓cV)+𝟘𝟙
- | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & I = Cast & c = (↓cT)+𝟙𝟘
+ | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] U2 & I = Cast & c = (↓cV)+𝟘𝟙
+ | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
- | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
/2 width=3 by cpg_inv_flat1_aux/ qed-.
-lemma cpg_inv_appl1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.U1 â\9e¡[c, h] U2 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_appl1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.U1 â¬\88[c, h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓐV2.T2 & c = (↓cV)+cT
- | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
- | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â\9e¡[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+ | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V & â¬\86*[1] V â\89¡ V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &
U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
#c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
[ /3 width=8 by or3_intro0, ex4_4_intro/
]
qed-.
-lemma cpg_inv_cast1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.U1 â\9e¡[c, h] U2 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_cast1: â\88\80c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.U1 â¬\88[c, h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] T2 &
U2 = ⓝV2.T2 & c = (↓cV)+cT
- | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â\9e¡[cT, h] U2 & c = (↓cT)+𝟙𝟘
- | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] U2 & c = (↓cV)+𝟘𝟙.
+ | â\88\83â\88\83cT. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[cT, h] U2 & c = (↓cT)+𝟙𝟘
+ | â\88\83â\88\83cV. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] U2 & c = (↓cV)+𝟘𝟙.
#c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
[ /3 width=8 by or3_intro0, ex4_4_intro/
|2,3: /3 width=3 by or3_intro1, or3_intro2, ex2_intro/
(* Basic forward lemmas *****************************************************)
-lemma cpg_fwd_bind1_minus: â\88\80c,h,I,G,L,V1,T1,T. â¦\83G, Lâ¦\84 â\8a¢ -â\93\91{I}V1.T1 â\9e¡[c, h] T → ∀p.
- â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡[c, h] ⓑ{p,I}V2.T2 &
+lemma cpg_fwd_bind1_minus: â\88\80c,h,I,G,L,V1,T1,T. â¦\83G, Lâ¦\84 â\8a¢ -â\93\91{I}V1.T1 â¬\88[c, h] T → ∀p.
+ â\88\83â\88\83V2,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\91{p,I}V1.T1 â¬\88[c, h] ⓑ{p,I}V2.T2 &
T = -ⓑ{I}V2.T2.
#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/