---

Step * of Lemma quicksort-int-last

∀[L:ℤ List]. ∀n:ℤ. n ≤ last(quicksort-int(L)) supposing (n ∈ L)
BY
{ ((UnivCD
    THENA (Auto
           THEN (RWO "quicksort-int-member" (-2) THENA Auto)
           THEN (RW assert_pushdownC 0 THENA Auto)
           THEN (D 0 THEN Auto)
           THEN (RWO "-1" (-3) THENA Auto)
           THEN GenListD (-3))
    )
   THEN (RWO "quicksort-int-member" (-1) THENA Auto)
   THEN RepeatFor 2 (D (-1))
   THEN Unfold `last` 0
   THEN (RWO "-1" 0 THENA Auto)
   THEN (Decide ⌜i = (||quicksort-int(L)|| - 1) ∈ ℤ⌝⋅ THENA Auto)
   THEN Try (Complete ((RWO "-1" 0 THEN Auto)))
   THEN (BLemma `quicksort-int-prop1` THEN Auto)
   THEN (MemTypeCD THEN Auto)
   THEN RWO "quicksort-int-length<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}n:\mBbbZ{}.  n  \mleq{}  last(quicksort-int(L))  supposing  (n  \mmember{}  L)


By

---

Latex:
((UnivCD
    THENA  (Auto
                  THEN  (RWO  "quicksort-int-member"  (-2)  THENA  Auto)
                  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
                  THEN  (D  0  THEN  Auto)
                  THEN  (RWO  "-1"  (-3)  THENA  Auto)
                  THEN  GenListD  (-3))
    )
  THEN  (RWO  "quicksort-int-member"  (-1)  THENA  Auto)
  THEN  RepeatFor  2  (D  (-1))
  THEN  Unfold  `last`  0
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}i  =  (||quicksort-int(L)||  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((RWO  "-1"  0  THEN  Auto)))
  THEN  (BLemma  `quicksort-int-prop1`  THEN  Auto)
  THEN  (MemTypeCD  THEN  Auto)
  THEN  RWO  "quicksort-int-length<"  0
  THEN  Auto)

---

Home Index