---

Step * 1 of Lemma quicksort-int-iseg


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
BY
{ (Subst ⌜n = quicksort-int(L)[||L'||] ∈ ℤ⌝ 0⋅
   THENA (Auto'
          THEN (RWO "-2" 0 THENA (Auto' THEN RWO "-3" 0 THEN Auto'))
          THEN (RWO "select_append_front" 0 THENA Auto')
          THEN (RWO "select_append_back" 0 THENA Auto')
          THEN (Subst ⌜||L'|| - ||L'|| ~ 0⌝ 0⋅ THENA Auto)
          THEN Reduce 0
          THEN Auto)
   )⋅ }

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] ≤ quicksort-int(L)[||L'||]

---

Latex:

---

Latex:

1.  L'  :  \mBbbZ{}  List
2.  L  :  \mBbbZ{}  List
3.  k  :  \mBbbN{}||L'||
4.  n  :  \mBbbZ{}
5.  l  :  \mBbbZ{}  List
6.  quicksort-int(L)  =  ((L'  @  [n])  @  l)
7.  ||L'||  -  1  -  k  <  ||L'||
\mvdash{}  L'[||L'||  -  1  -  k]  \mleq{}  n


By

---

Latex:
(Subst  \mkleeneopen{}n  =  quicksort-int(L)[||L'||]\mkleeneclose{}  0\mcdot{}
  THENA  (Auto'
                THEN  (RWO  "-2"  0  THENA  (Auto'  THEN  RWO  "-3"  0  THEN  Auto'))
                THEN  (RWO  "select\_append\_front"  0  THENA  Auto')
                THEN  (RWO  "select\_append\_back"  0  THENA  Auto')
                THEN  (Subst  \mkleeneopen{}||L'||  -  ||L'||  \msim{}  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                THEN  Reduce  0
                THEN  Auto)
  )\mcdot{}

---

Home Index