---

Step * of Lemma ts-final_wf

∀[ts:transition-system{i:l}]. (ts-final(ts) ∈ ts-reachable(ts) ⟶ ℙ)
BY
{ (RepUR ``transition-system ts-final ts-reachable ts-rel ts-init ts-type`` 0
   THEN (D 0 THENA Auto)
   THEN (RepeatFor 3 (D -1) THEN Reduce 0)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(RepUR  ``transition-system  ts-final  ts-reachable  ts-rel  ts-init  ts-type``  0
  THEN  (D  0  THENA  Auto)
  THEN  (RepeatFor  3  (D  -1)  THEN  Reduce  0)
  THEN  Auto)

---

Home Index