---

Step * of Lemma quicksort-int_wf

∀L:ℤ List. (quicksort-int(L) ∈ {srtd:ℤ List| sorted-by(λx,y. (x ≤ y);srtd) ∧ permutation(ℤ;srtd;L)} )
BY
{ ((D 0 THENA Auto)
   THEN Unfold `quicksort-int` 0
   THEN (InstLemma `quicksort_wf` [⌜ℤ⌝;⌜λx,y. (y - x)⌝;⌜L⌝]⋅
         THENA (Auto THEN Unfold `comparison` 0 THEN MemTypeCD THEN Reduce 0 THEN Auto')
         )
   THEN Reduce (-1)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN All (Unfold `sorted-by`)
   THEN All Reduce
   THEN Auto
   THEN (InstHyp [⌜i⌝;⌜j⌝] (-4)⋅ THENA Auto)
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}L:\mBbbZ{}  List.  (quicksort-int(L)  \mmember{}  \{srtd:\mBbbZ{}  List|  sorted-by(\mlambda{}x,y.  (x  \mleq{}  y);srtd)  \mwedge{}  permutation(\mBbbZ{};srtd;L)\}  \000C)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfold  `quicksort-int`  0
  THEN  (InstLemma  `quicksort\_wf`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  (y  -  x)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Unfold  `comparison`  0  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto')
              )
  THEN  Reduce  (-1)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  All  (Unfold  `sorted-by`)
  THEN  All  Reduce
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  Auto')

---

Home Index