---

Step * of Lemma fix_wf_dataflow_w_state

∀[A,B,S:Type]. ∀[s0:S]. ∀[F:Top ─→ Top ─→ Top ∩ ∩P:Type. ((S ─→ P) ─→ S ─→ A ─→ (P × B))].  (fix(F) s0 ∈ dataflow(A;B))
BY
{ (Auto THEN Unfold `dataflow` 0 THEN BLemma `fix_wf_corec_parameter` THEN Auto) }

---

Latex:

---

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


By

---

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

---

Home Index