---

Step * 1 1 1 1 1 of Lemma quicksort-int-iseg

.....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||
BY
{ (HypSubst' (-3) (-1) THEN Auto') }

---

Latex:

---

Latex:
.....wf..... 
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{}  ||L'||  \mmember{}  \mBbbN{}||L||


By

---

Latex:
(HypSubst'  (-3)  (-1)  THEN  Auto')

---

Home Index