include "ground/steps/rtc_ist_shift.ma".
include "ground/steps/rtc_ist_plus.ma".
include "ground/steps/rtc_ist_max.ma".
include "ground/steps/rtc_ist_shift.ma".
include "ground/steps/rtc_ist_plus.ma".
include "ground/steps/rtc_ist_max.ma".
include "basic_2/notation/relations/pty_6.ma".
include "basic_2/rt_transition/cpg.ma".
(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
definition cpt (h) (G) (L) (n): relation2 term term ≝
include "basic_2/notation/relations/pty_6.ma".
include "basic_2/rt_transition/cpg.ma".
(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
definition cpt (h) (G) (L) (n): relation2 term term ≝
- λT1,T2. ∃∃c. 𝐓❪n,c❫ & ❪G,L❫ ⊢ T1 ⬈[eq …,c,h] T2.
+ λT1,T2. ∃∃c. 𝐓❪n,c❫ & ❪G,L❫ ⊢ T1 ⬈[sh_is_next h,eq …,c] T2.
lemma cpt_ess (h) (G) (L):
∀s. ❪G,L❫ ⊢ ⋆s ⬆[h,1] ⋆(⫯[h]s).
lemma cpt_ess (h) (G) (L):
∀s. ❪G,L❫ ⊢ ⋆s ⬆[h,1] ⋆(⫯[h]s).
lemma cpt_delta (h) (n) (G) (K):
∀V1,V2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 →
lemma cpt_delta (h) (n) (G) (K):
∀V1,V2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 →
#h #n #J #G #L #X2 * #c #Hc #H
elim (cpg_inv_atom1 … H) -H *
[ #H1 #H2 destruct /3 width=1 by or5_intro0, conj/
#h #n #J #G #L #X2 * #c #Hc #H
elim (cpg_inv_atom1 … H) -H *
[ #H1 #H2 destruct /3 width=1 by or5_intro0, conj/
| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
/4 width=6 by or5_intro2, ex4_3_intro, ex2_intro/
| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
/4 width=6 by or5_intro2, ex4_3_intro, ex2_intro/
| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
#h #n #G #L #s #X2 * #c #Hc #H
elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
#h #n #G #L #s #X2 * #c #Hc #H
elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct