---

Step * of Lemma quicksort-int-iseg

∀[L,L':ℤ List]. ∀[n:ℤ].  ∀[x:ℤ]. x ≤ n supposing (x ∈ L') supposing L' @ [n] ≤ quicksort-int(L)
BY
{ (Auto
   THEN Unfold `l_member` (-1)
   THEN ExRepD
   THEN Unfold `iseg` (-5)
   THEN ExRepD
   THEN (Assert ⌜∃k:ℕ||L'||. (i = (||L'|| - 1 - k) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜||L'|| - 1 - i⌝]⋅ THEN Auto'))
   THEN ExRepD
   THEN Eliminate ⌜i⌝⋅
   THEN ThinVar `i'
   THEN (RWO "-1" 0 THENA Auto)
   THEN ThinVar `x') }

1
1. L' : ℤ List
2. L : ℤ List
3. k : ℕ||L'||
4. n : ℤ
5. l : ℤ List
6. quicksort-int(L) = ((L' @ [n]) @ l) ∈ (ℤ List)
7. ||L'|| - 1 - k < ||L'||
⊢ L'[||L'|| - 1 - k] ≤ n

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `l\_member`  (-1)
  THEN  ExRepD
  THEN  Unfold  `iseg`  (-5)
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}||L'||.  (i  =  (||L'||  -  1  -  k))\mkleeneclose{}\mcdot{}
              THENA  (InstConcl  [\mkleeneopen{}||L'||  -  1  -  i\mkleeneclose{}]\mcdot{}  THEN  Auto')
              )
  THEN  ExRepD
  THEN  Eliminate  \mkleeneopen{}i\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `i'
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  ThinVar  `x')

---

Home Index