---

Step * of Lemma ts-reachable_wf

∀[ts:transition-system{i:l}]. (ts-reachable(ts) ∈ {T:Type| T ⊆r ts-type(ts)} )
BY
{ (RepUR ``transition-system ts-type ts-reachable ts-init ts-rel`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[ts:transition-system\{i:l\}].  (ts-reachable(ts)  \mmember{}  \{T:Type|  T  \msubseteq{}r  ts-type(ts)\}  )


By

---

Latex:
(RepUR  ``transition-system  ts-type  ts-reachable  ts-init  ts-rel``  0  THEN  Auto)

---

Home Index