---

Step * of Lemma ts-init_wf

∀[ts:transition-system{i:l}]. (ts-init(ts) ∈ ts-type(ts))
BY
{ (Unfolds ``transition-system ts-init ts-type`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[ts:transition-system\{i:l\}].  (ts-init(ts)  \mmember{}  ts-type(ts))


By

---

Latex:
(Unfolds  ``transition-system  ts-init  ts-type``  0  THEN  Auto)

---

Home Index