---

Step * of Lemma max-WFTO_wf

max-WFTO{i:l}() ∈ WFTRO{i':l}
BY
{ (Unfolds ``max-WFTO WFTRO`` 0⋅ THEN Auto) }

---

Latex:

---

Latex:
max-WFTO\{i:l\}()  \mmember{}  WFTRO\{i':l\}


By

---

Latex:
(Unfolds  ``max-WFTO  WFTRO``  0\mcdot{}  THEN  Auto)

---

Home Index