---

Step * of Lemma ot-less-trans_wf

ot-less-trans() ∈ Trans(WFO{i:l}();x,y.order-type-less() x y)
BY
{ xxx((Assert TERMOF{order-type-less-transitive-ext:o, 1:l, i:l} ∈ Trans(WFO{i:l}();x,y.order-type-less() x y) BY
             Auto)
      THEN RW (AddrC [2] (TagC (mk_tag_term 1))) (-1)
      THEN Auto)xxx }

---

Latex:

---

Latex:
ot-less-trans()  \mmember{}  Trans(WFO\{i:l\}();x,y.order-type-less()  x  y)


By

---

Latex:
xxx((Assert  TERMOF\{order-type-less-transitive-ext:o,  1:l,  i:l\}
                        \mmember{}  Trans(WFO\{i:l\}();x,y.order-type-less()  x  y)  BY
                      Auto)
        THEN  RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  (-1)
        THEN  Auto)xxx

---

Home Index