---

Step * of Lemma ts-init_wf_reachable

∀[ts:transition-system{i:l}]. (ts-init(ts) ∈ ts-reachable(ts))
BY
{ Auto }

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index