---

Step * 1 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'||
8. ||L|| = ||quicksort-int(L)|| ∈ ℤ
⊢ quicksort-int(L)[||L'|| - 1 - k] ≤ quicksort-int(L)[||L'||]
BY
{ (BLemma `quicksort-int-prop1` THEN Auto) }

1
.....wf..... 
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)|| ∈ ℤ
⊢ ||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'||
8.  ||L||  =  ||quicksort-int(L)||
\mvdash{}  quicksort-int(L)[||L'||  -  1  -  k]  \mleq{}  quicksort-int(L)[||L'||]


By

---

Latex:
(BLemma  `quicksort-int-prop1`  THEN  Auto)

---

Home Index