---

Step * 1 of Lemma cpsquicksort_wf


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
BY
{ xxx((GenConclAtAddrVar  [2;1] `x' THEN RW (AddrC [2] UnfoldTopAbC) 0 THEN Reduce 0)
      THEN RepeatFor 3 ((GenConclAtAddrVar  [2;1] `L' THEN RW (AddrC [2] UnfoldTopAbC) 0 THEN Reduce 0))
      )xxx }

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
9. x : T
10. hd(L) = x ∈ T
11. L1 : T List
12. filter(λz.0 <z cmp z x;L) = L1 ∈ (T List)
13. L2 : T List
14. filter(λz.(0 =z cmp x z);L) = L2 ∈ (T List)
15. L3 : T List
16. filter(λz.0 <z cmp x z;L) = L3 ∈ (T List)
⊢ cpsquicksort(cmp;L1;λS1.cpsquicksort(cmp;L3;λS3.(k (S1 @ L2 @ S3)))) ∈ A

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  cmp  :  comparison(T)
4.  n  :  \mBbbN{}
5.  L  :  T  List
6.  \mneg{}(L  =  [])
7.  \mforall{}L1:T  List.  (||L1||  <  ||L||  {}\mRightarrow{}  (\mforall{}[k:(T  List)  {}\mrightarrow{}  A].  (cpsquicksort(cmp;L1;k)  \mmember{}  A)))
8.  k  :  (T  List)  {}\mrightarrow{}  A
\mvdash{}  let  x  =  hd(L)  in
      let  L1  =  filter(\mlambda{}z.0  <z  cmp  z  x;L)  in
      let  L2  =  filter(\mlambda{}z.(0  =\msubz{}  cmp  x  z);L)  in
      let  L3  =  filter(\mlambda{}z.0  <z  cmp  x  z;L)  in
      cpsquicksort(cmp;L1;\mlambda{}S1.cpsquicksort(cmp;L3;\mlambda{}S3.(k  (S1  @  L2  @  S3))))  \mmember{}  A


By

---

Latex:
xxx((GenConclAtAddrVar    [2;1]  `x'  THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0  THEN  Reduce  0)
        THEN  RepeatFor  3  ((GenConclAtAddrVar    [2;1]  `L'
                                              THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0
                                              THEN  Reduce  0))
        )xxx

---

Home Index