---

Step * of Lemma state-machine-spec_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[C,R:Type]. ∀[F:(C List) ─→ R]. ∀[I:EClass(C)]. ∀[O:EClass(R)].
  (state-machine-spec{i:l}(Info;es;C;R;F;I;O) ∈ ℙ')
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[C,R:Type].  \mforall{}[F:(C  List)  {}\mrightarrow{}  R].  \mforall{}[I:EClass(C)].  \mforall{}[O:EClass(R)].
    (state-machine-spec\{i:l\}(Info;es;C;R;F;I;O)  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma

---

Home Index