---

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

∀[Info,A,B:Type].
  ∀[xpr1,xpr2:Id ─→ hdataflow(Info;A)]. ∀[ypr1,ypr2:A ─→ Id ─→ hdataflow(Info;B)].
    (xpr1 >>= ypr1 = xpr2 >>= ypr2 ∈ (Id ─→ hdataflow(Info;B))) supposing 
       ((xpr1 = xpr2 ∈ (Id ─→ hdataflow(Info;A))) and 
       (ypr1 = ypr2 ∈ (A ─→ Id ─→ hdataflow(Info;B)))) 
  supposing valueall-type(B)
BY
{ (Auto THEN RepUR ``bind-class-program`` 0 THEN Repeat ((EqCD THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].
    \mforall{}[xpr1,xpr2:Id  {}\mrightarrow{}  hdataflow(Info;A)].  \mforall{}[ypr1,ypr2:A  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;B)].
        (xpr1  >>=  ypr1  =  xpr2  >>=  ypr2)  supposing  ((xpr1  =  xpr2)  and  (ypr1  =  ypr2)) 
    supposing  valueall-type(B)


By

---

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

---

Home Index