---

Step * of Lemma parallel-class-program-eq

∀[Info,B:Type].
  ∀[X,Y:EClass(B)]. ∀[Xpr1,Xpr2:LocalClass(X)]. ∀[Ypr1,Ypr2:LocalClass(Y)].
    (Xpr1 || Ypr1 = Xpr2 || Ypr2 ∈ (Id ⟶ hdataflow(Info;B))) supposing 
       ((Xpr1 = Xpr2 ∈ (Id ⟶ hdataflow(Info;B))) and 
       (Ypr1 = Ypr2 ∈ (Id ⟶ hdataflow(Info;B)))) 
  supposing valueall-type(B)
BY
{ (Auto
   THEN SubsumeC LocalClass(X || Y)⋅
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN EqTypeCD
   THEN Auto
   THEN OnMaybeHyp 6 (\h. (D h THEN Complete (Auto)))) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].
    \mforall{}[X,Y:EClass(B)].  \mforall{}[Xpr1,Xpr2:LocalClass(X)].  \mforall{}[Ypr1,Ypr2:LocalClass(Y)].
        (Xpr1  ||  Ypr1  =  Xpr2  ||  Ypr2)  supposing  ((Xpr1  =  Xpr2)  and  (Ypr1  =  Ypr2)) 
    supposing  valueall-type(B)


By

---

Latex:
(Auto
  THEN  SubsumeC  LocalClass(X  ||  Y)\mcdot{}
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  EqTypeCD
  THEN  Auto
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto))))

---

Home Index