---

Step * of Lemma quicksort-int-single

∀[n:ℤ]. (quicksort-int([n]) ~ [n])
BY
{ (Auto
   THEN RepUR ``quicksort-int`` 0
   THEN RecUnfold `quicksort` 0
   THEN Reduce 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (Subst ⌜n - n ~ 0⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Fold `quicksort-int` 0
   THEN RWO "quicksort-int-nil" 0
   THEN Reduce 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN Try ((BLemma `sorted-by-single` THEN Auto))
   THEN BLemma `permutation_weakening`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  (quicksort-int([n])  \msim{}  [n])


By

---

Latex:
(Auto
  THEN  RepUR  ``quicksort-int``  0
  THEN  RecUnfold  `quicksort`  0
  THEN  Reduce  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}n  -  n  \msim{}  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Fold  `quicksort-int`  0
  THEN  RWO  "quicksort-int-nil"  0
  THEN  Reduce  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((BLemma  `sorted-by-single`  THEN  Auto))
  THEN  BLemma  `permutation\_weakening`
  THEN  Auto)

---

Home Index