---

Step * of Lemma parallel-class-program-eq-hdf

∀[Info,B:Type].
  ∀[Xpr1,Xpr2,Ypr1,Ypr2:Id ─→ hdataflow(Info;B)].
    (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 RepUR ``parallel-class-program`` 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].
    \mforall{}[Xpr1,Xpr2,Ypr1,Ypr2:Id  {}\mrightarrow{}  hdataflow(Info;B)].
        (Xpr1  ||  Ypr1  =  Xpr2  ||  Ypr2)  supposing  ((Xpr1  =  Xpr2)  and  (Ypr1  =  Ypr2)) 
    supposing  valueall-type(B)


By

---

Latex:
(Auto  THEN  RepUR  ``parallel-class-program``  0  THEN  EqCD  THEN  Auto)

---

Home Index