---

Step * of Lemma quicksort-int-prop1

∀[L:ℤ List]. ∀[i:ℕ||L||]. ∀[j:ℕi].  (quicksort-int(L)[j] ≤ quicksort-int(L)[i])
BY
{ (Auto
   THEN InstLemma `quicksort-int-length` [⌜L⌝]⋅
   THEN Auto
   THEN (InstLemma `quicksort-int_wf` [⌜L⌝]⋅ THENA Auto)
   THEN DVarSets
   THEN Auto
   THEN RepUR ``sorted-by`` (-2)
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}[i:\mBbbN{}||L||].  \mforall{}[j:\mBbbN{}i].    (quicksort-int(L)[j]  \mleq{}  quicksort-int(L)[i])


By

---

Latex:
(Auto
  THEN  InstLemma  `quicksort-int-length`  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `quicksort-int\_wf`  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DVarSets
  THEN  Auto
  THEN  RepUR  ``sorted-by``  (-2)
  THEN  BackThruSomeHyp)

---

Home Index