---

Step * of Lemma eclass2-program-eq-hdf

∀[Info,B,C:Type].
  ∀[Xpr1,Xpr2:Id ─→ hdataflow(Info;B ─→ bag(C))]. ∀[Ypr1,Ypr2:Id ─→ hdataflow(Info;B)].
    (Xpr1 o Ypr1 = Xpr2 o Ypr2 ∈ (Id ─→ hdataflow(Info;C))) supposing 
       ((Xpr1 = Xpr2 ∈ (Id ─→ hdataflow(Info;B ─→ bag(C)))) and 
       (Ypr1 = Ypr2 ∈ (Id ─→ hdataflow(Info;B)))) 
  supposing valueall-type(C)
BY
{ (Auto THEN RepUR ``eclass2-program`` 0 THEN EqCD THEN Auto) }

---

Latex:

---

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


By

---

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

---

Home Index