---

Step * of Lemma ts-rel_wf

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

---

Latex:

---

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


By

---

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

---

Home Index