---

Step * 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'||
⊢ L'[||L'|| - 1 - k] ≤ quicksort-int(L)[||L'||]
BY
{ (Subst' ⌜L'[||L'|| - 1 - k] = quicksort-int(L)[||L'|| - 1 - k] ∈ ℤ⌝ 0⋅
   THENA (Auto'
          THEN ((RWO "-2" 0 THENA (Auto' THEN RWO "-3" 0 THEN Auto'))
                THEN RepeatFor 2 ((RWO "select_append_front" 0 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'||
⊢ 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{}  L'[||L'||  -  1  -  k]  \mleq{}  quicksort-int(L)[||L'||]


By

---

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

---

Home Index