include "ground_2/steps/rtc_max.ma".
include "ground_2/steps/rtc_plus.ma".
include "basic_2/notation/relations/predty_7.ma".
-include "static_2/syntax/sort.ma".
+include "static_2/syntax/sh.ma".
include "static_2/syntax/lenv.ma".
include "static_2/syntax/genv.ma".
include "static_2/relocation/lifts.ma".
(* avtivate genv *)
inductive cpg (Rt:relation rtc) (h): rtc → relation4 genv lenv term term ≝
| cpg_atom : ∀I,G,L. cpg Rt h (𝟘𝟘) G L (⓪{I}) (⓪{I})
-| cpg_ess : ∀G,L,s. cpg Rt h (𝟘𝟙) G L (⋆s) (⋆(next h s))
+| cpg_ess : ∀G,L,s. cpg Rt h (𝟘𝟙) G L (⋆s) (⋆(⫯[h]s))
| cpg_delta: ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 →
⬆*[1] V2 ≘ W2 → cpg Rt h c G (L.ⓓV1) (#0) W2
| cpg_ell : ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 →
fact cpg_inv_atom1_aux: ∀Rt,c,h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈[Rt,c,h] T2 → ∀J. T1 = ⓪{J} →
∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘
- | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
+ | ∃∃s. J = Sort s & T2 = ⋆(⫯[h]s) & c = 𝟘𝟙
| ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 &
L = K.ⓓV1 & J = LRef 0 & c = cV
| ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 &
lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ⬈[Rt,c,h] T2 →
∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘
- | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
+ | ∃∃s. J = Sort s & T2 = ⋆(⫯[h]s) & c = 𝟘𝟙
| ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 &
L = K.ⓓV1 & J = LRef 0 & c = cV
| ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 &
/2 width=3 by cpg_inv_atom1_aux/ qed-.
lemma cpg_inv_sort1: ∀Rt,c,h,G,L,T2,s. ⦃G,L⦄ ⊢ ⋆s ⬈[Rt,c,h] T2 →
- ∨∨ T2 = ⋆s ∧ c = 𝟘𝟘 | T2 = ⋆(next h s) ∧ c = 𝟘𝟙.
+ ∨∨ T2 = ⋆s ∧ c = 𝟘𝟘 | T2 = ⋆(⫯[h]s) ∧ c = 𝟘𝟙.
#Rt #c #h #G #L #T2 #s #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
[ #s0 #H destruct /3 width=1 by or_intror, conj/