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