---

Step * of Lemma fix_wf_dataflow

∀[A,B:Type]. ∀[F:⋂P:Type. (P ⟶ A ⟶ (P × B))].  (fix(F) ∈ dataflow(A;B))
BY
{ (Auto THEN Unfold `dataflow` 0 THEN BLemma `fix_wf_corec` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[F:\mcap{}P:Type.  (P  {}\mrightarrow{}  A  {}\mrightarrow{}  (P  \mtimes{}  B))].    (fix(F)  \mmember{}  dataflow(A;B))


By

---

Latex:
(Auto  THEN  Unfold  `dataflow`  0  THEN  BLemma  `fix\_wf\_corec`  THEN  Auto)

---

Home Index