---

Step * of Lemma bind-nxt_wf

∀[A,B,C:Type]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[p:hdataflow(A;B) × bag(hdataflow(A;C))]. ∀[a:A].
  bind-nxt(Y;p;a) ∈ hdataflow(A;B) × bag(hdataflow(A;C)) × bag(C) supposing valueall-type(C)
BY
{ ProveWfLemmaAux (Try (Complete Auto)) }

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[Y:B  {}\mrightarrow{}  hdataflow(A;C)].  \mforall{}[p:hdataflow(A;B)  \mtimes{}  bag(hdataflow(A;C))].  \mforall{}[a:A].
    bind-nxt(Y;p;a)  \mmember{}  hdataflow(A;B)  \mtimes{}  bag(hdataflow(A;C))  \mtimes{}  bag(C)  supposing  valueall-type(C)


By

ProveWfLemmaAux  (Try  (Complete  Auto))

---

Home Index