---

Step * of Lemma l-ordered-is-sorted-by

∀[T:Type]. ∀R:T ⟶ T ⟶ ℙ. ∀L:T List.  (l-ordered(T;x,y.R[x;y];L) ⇐⇒ sorted-by(λx,y. R[x;y];L))
BY
{ xxx(RepUR ``l-ordered sorted-by`` 0
      THEN Auto
      THEN Try (Complete ((BackThruSomeHyp THEN BLemma `l_before_select` THEN Auto)))
      THEN RepUR ``l_before sublist`` (-1)
      THEN ExRepD
      THEN InstHyp [⌜f 1⌝;⌜f 0⌝] (-6)⋅
      THEN Auto
      THEN RWO "-2<" (-1)
      THEN Auto
      THEN Reduce 0
      THEN RWO "-2<" 0
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}L:T  List.    (l-ordered(T;x,y.R[x;y];L)  \mLeftarrow{}{}\mRightarrow{}  sorted-by(\mlambda{}x,y.  R[x;y];L))


By

---

Latex:
xxx(RepUR  ``l-ordered  sorted-by``  0
        THEN  Auto
        THEN  Try  (Complete  ((BackThruSomeHyp  THEN  BLemma  `l\_before\_select`  THEN  Auto)))
        THEN  RepUR  ``l\_before  sublist``  (-1)
        THEN  ExRepD
        THEN  InstHyp  [\mkleeneopen{}f  1\mkleeneclose{};\mkleeneopen{}f  0\mkleeneclose{}]  (-6)\mcdot{}
        THEN  Auto
        THEN  RWO  "-2<"  (-1)
        THEN  Auto
        THEN  Reduce  0
        THEN  RWO  "-2<"  0
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index