---

Step * of Lemma from-upto-sorted

∀a,b:ℤ.  sorted-by(λx,y. x < y;[a, b))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN Reduce 0
   THEN RWO "select-from-upto" 0
   THEN Auto
   THEN All (RWO "length-from-upto")
   THEN Auto
   THEN OnMaybeHyp 3 (\h. (SplitOnHypITE h  THEN Auto))⋅) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    sorted-by(\mlambda{}x,y.  x  <  y;[a,  b))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  Reduce  0
  THEN  RWO  "select-from-upto"  0
  THEN  Auto
  THEN  All  (RWO  "length-from-upto")
  THEN  Auto
  THEN  OnMaybeHyp  3  (\mbackslash{}h.  (SplitOnHypITE  h    THEN  Auto))\mcdot{})

---

Home Index