---

Step * 1 2 1 1 1 of Lemma quicksort_wf


1. T : Type
2. cmp : comparison(T)
3. valueall-type(T)
4. n : ℕ
5. L : T List@i
6. ∀L1:T List
     (||L1|| < ||L|| ⇒ (quicksort(cmp;L1) ∈ {srtd:T List| sorted-by(λx,y. (0 ≤ (cmp x y));srtd) ∧ permutation(T;srtd;L1\000C)} ))
7. ¬(L = [] ∈ (T List))
8. ||L|| ≥ 1 
⊢ (∃x∈L. ¬↑0 <z cmp x hd(L))
BY
{ ((BLemma `l_exists_iff` THEN Auto)
   THEN (With ⌜hd(L)⌝ (D 0)⋅ THENA Auto)
   THEN Auto
   THEN Subst' cmp hd(L) hd(L) ~ 0 0
   THEN Reduce 0
   THEN Auto
   THEN (InstLemma `comparison-equiv` [⌜T⌝;⌜cmp⌝]⋅ THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  valueall-type(T)
4.  n  :  \mBbbN{}
5.  L  :  T  List@i
6.  \mforall{}L1:T  List
          (||L1||  <  ||L||
          {}\mRightarrow{}  (quicksort(cmp;L1)  \mmember{}  \{srtd:T  List| 
                                                            sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));srtd)  \mwedge{}  permutation(T;srtd;L1)\}  ))
7.  \mneg{}(L  =  [])
8.  ||L||  \mgeq{}  1 
\mvdash{}  (\mexists{}x\mmember{}L.  \mneg{}\muparrow{}0  <z  cmp  x  hd(L))


By

---

Latex:
((BLemma  `l\_exists\_iff`  THEN  Auto)
  THEN  (With  \mkleeneopen{}hd(L)\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  Auto
  THEN  Subst'  cmp  hd(L)  hd(L)  \msim{}  0  0
  THEN  Reduce  0
  THEN  Auto
  THEN  (InstLemma  `comparison-equiv`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}cmp\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index