---

Step * of Lemma ts-type_wf

∀[ts:transition-system{i:l}]. (ts-type(ts) ∈ Type)
BY
{ ((D 0 THENM (RepeatFor 3 (D -1) THEN RepUR ``ts-type`` 0)) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENM  (RepeatFor  3  (D  -1)  THEN  RepUR  ``ts-type``  0))  THEN  Auto)

---

Home Index