---

Step * of Lemma frs-non-dec-sorted-by

∀[p:ℝ List]. (frs-non-dec(p) ⇐⇒ sorted-by(λx,y. (x ≤ y);p))
BY
{ (RepUR ``frs-non-dec sorted-by`` 0
   THEN (Auto THEN (Decide ⌜i = j ∈ ℤ⌝⋅ THENA Auto))
   THEN Auto'
   THEN Try ((BackThruSomeHyp THEN Complete (Auto')))
   THEN HypSubst' (-1) 0⋅
   THEN RelRST
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbR{}  List].  (frs-non-dec(p)  \mLeftarrow{}{}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (x  \mleq{}  y);p))


By

---

Latex:
(RepUR  ``frs-non-dec  sorted-by``  0
  THEN  (Auto  THEN  (Decide  \mkleeneopen{}i  =  j\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  Auto'
  THEN  Try  ((BackThruSomeHyp  THEN  Complete  (Auto')))
  THEN  HypSubst'  (-1)  0\mcdot{}
  THEN  RelRST
  THEN  Auto)

---

Home Index