---

Step * of Lemma cpsquicksort_wf

∀[T,A:Type]. ∀[cmp:comparison(T)].  ∀L:T List. ∀[k:(T List) ⟶ A]. (cpsquicksort(cmp;L;k) ∈ A)
BY
{ (InductionOnLength THEN Auto THEN RecUnfold `cpsquicksort` 0⋅ THEN AutoSplit) }

1
1. T : Type
2. A : Type
3. cmp : comparison(T)
4. n : ℕ
5. L : T List
6. ¬(L = [] ∈ (T List))
7. ∀L1:T List. (||L1|| < ||L|| ⇒ (∀[k:(T List) ⟶ A]. (cpsquicksort(cmp;L1;k) ∈ A)))
8. k : (T List) ⟶ A
⊢ let x = hd(L) in
   let L1 = filter(λz.0 <z cmp z x;L) in
   let L2 = filter(λz.(0 =z cmp x z);L) in
   let L3 = filter(λz.0 <z cmp x z;L) in
   cpsquicksort(cmp;L1;λS1.cpsquicksort(cmp;L3;λS3.(k (S1 @ L2 @ S3)))) ∈ A

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[cmp:comparison(T)].    \mforall{}L:T  List.  \mforall{}[k:(T  List)  {}\mrightarrow{}  A].  (cpsquicksort(cmp;L;k)  \mmember{}  A)


By

---

Latex:
(InductionOnLength  THEN  Auto  THEN  RecUnfold  `cpsquicksort`  0\mcdot{}  THEN  AutoSplit)

---

Home Index