---

Step * 1 1 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'||
⊢ quicksort-int(L)[||L'|| - 1 - k] ≤ quicksort-int(L)[||L'||]
BY
{ (InstLemma `quicksort-int-length` [⌜L⌝]⋅ THENA 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'||
8. ||L|| = ||quicksort-int(L)|| ∈ ℤ
⊢ quicksort-int(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{}  quicksort-int(L)[||L'||  -  1  -  k]  \mleq{}  quicksort-int(L)[||L'||]


By

---

Latex:
(InstLemma  `quicksort-int-length`  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index