(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝
- λh,g,l1,l2,G,L,T1,T2.
- ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T.
+ λh,g,d1,d2,G,L,T1,T2.
+ ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, g, d2] T.
interpretation "stratified decomposed parallel equivalence (term)"
- 'DPConvStar h g l1 l2 G L T1 T2 = (scpes h g l1 l2 G L T1 T2).
+ 'DPConvStar h g d1 d2 G L T1 T2 = (scpes h g d1 d2 G L T1 T2).
(* Basic properties *********************************************************)
-lemma scpds_div: ∀h,g,G,L,T1,T2,T,l1,l2.
- ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T →
- ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+lemma scpds_div: ∀h,g,G,L,T1,T2,T,d1,d2.
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, g, d2] T →
+ ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d1, d2] T2.
/2 width=3 by ex2_intro/ qed.
-lemma scpes_sym: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
- ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l1] T1.
-#h #g #G #L #T1 #T2 #L1 #l2 * /2 width=3 by scpds_div/
+lemma scpes_sym: ∀h,g,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d1, d2] T2 →
+ ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, d2, d1] T1.
+#h #g #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_div/
qed-.