---

Step * of Lemma order-type-less-transitive

Trans(WFO{i:l}();x,y.order-type-less() x y)
BY
{ (D 0
   THEN Auto
   THEN All (RepUR ``order-type-less WFO``)
   THEN D 3
   THEN D 4
   THEN D 2
   THEN D 3
   THEN D 1
   THEN D 2
   THEN All Reduce
   THEN ExRepD
   THEN (At ⌜Type⌝ (InstConcl [ ⌜f o f1⌝;⌜b⌝])⋅⋅ THENA Auto)
   THEN All (RepUR ``order-preserving``)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(D  0
  THEN  Auto
  THEN  All  (RepUR  ``order-type-less  WFO``)
  THEN  D  3
  THEN  D  4
  THEN  D  2
  THEN  D  3
  THEN  D  1
  THEN  D  2
  THEN  All  Reduce
  THEN  ExRepD
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (InstConcl  [  \mkleeneopen{}f  o  f1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}])\mcdot{}\mcdot{}  THENA  Auto)
  THEN  All  (RepUR  ``order-preserving``)
  THEN  Auto)

---

Home Index