λG,L,T1,T2. ∃c. ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2.
interpretation
- "uncounted context-sensitive parallel reduction (term)"
+ "uncounted context-sensitive parallel rt-transition (term)"
'PRedTy h G L T1 T2 = (cpx h G L T1 T2).
(* Basic properties *********************************************************)
-lemma cpx_atom: ∀h,I,G,L. ⦃G, L⦄ ⊢ ⓪{I} ⬈[h] ⓪{I}.
-/2 width=2 by cpg_atom, ex_intro/ qed.
-
(* Basic_2A1: was: cpx_st *)
lemma cpx_ess: ∀h,G,L,s. ⦃G, L⦄ ⊢ ⋆s ⬈[h] ⋆(next h s).
/2 width=2 by cpg_ess, ex_intro/ qed.
qed.
lemma cpx_bind: ∀h,p,I,G,L,V1,V2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
- ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] ⓑ{p,I}V2.T2.
+ ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
+ ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] ⓑ{p,I}V2.T2.
#h #p #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
/3 width=2 by cpg_bind, ex_intro/
qed.
lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
- ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2.
+ ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
+ ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2.
#h #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
/3 width=2 by cpg_flat, ex_intro/
qed.
/3 width=4 by cpg_theta, ex_intro/
qed.
+(* Basic_2A1: includes: cpx_atom *)
lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L).
/2 width=2 by ex_intro/ qed.