---

Step * 1 of Lemma cpsquicksort-quicksort


1. T : Type
2. valueall-type(T)
3. A : Type
4. cmp : comparison(T)
5. n : ℕ
6. L : T List
7. ∀L1:T List. (||L1|| < ||L|| ⇒ (∀[k:(T List) ⟶ A]. (cpsquicksort(cmp;L1;k) ~ k quicksort(cmp;L1))))
8. k : (T List) ⟶ A
9. ¬(L = [] ∈ (T List))
10. v : T
11. hd(L) = v ∈ T
12. v1 : T List
13. filter(λz.0 <z cmp z v;L) = v1 ∈ (T List)
14. v2 : T List
15. filter(λz.(0 =z cmp v z);L) = v2 ∈ (T List)
16. v3 : T List
17. filter(λz.0 <z cmp v z;L) = v3 ∈ (T List)
18. ||filter(λz.0 <z cmp z v;L)|| < ||L|| ∧ ||filter(λz.0 <z cmp v z;L)|| < ||L||
⊢ cpsquicksort(cmp;v1;λS1.cpsquicksort(cmp;v3;λS3.(k (S1 @ v2 @ S3)))) ~ k 
                                                                         let L3 ⟵ v2
                                                                         in quicksort(cmp;v1) @ L3 @ quicksort(cmp;v3)
BY
{ xxxRepeatFor 2 ((Reduce 0 THEN (RWO "7" 0 THEN Try (Complete (Auto)))⋅))xxx }

1
1. T : Type
2. valueall-type(T)
3. A : Type
4. cmp : comparison(T)
5. n : ℕ
6. L : T List
7. ∀L1:T List. (||L1|| < ||L|| ⇒ (∀[k:(T List) ⟶ A]. (cpsquicksort(cmp;L1;k) ~ k quicksort(cmp;L1))))
8. k : (T List) ⟶ A
9. ¬(L = [] ∈ (T List))
10. v : T
11. hd(L) = v ∈ T
12. v1 : T List
13. filter(λz.0 <z cmp z v;L) = v1 ∈ (T List)
14. v2 : T List
15. filter(λz.(0 =z cmp v z);L) = v2 ∈ (T List)
16. v3 : T List
17. filter(λz.0 <z cmp v z;L) = v3 ∈ (T List)
18. ||filter(λz.0 <z cmp z v;L)|| < ||L|| ∧ ||filter(λz.0 <z cmp v z;L)|| < ||L||
⊢ (λS3.(k (quicksort(cmp;v1) @ v2 @ S3))) quicksort(cmp;v3) ~ k 
                                                              let L3 ⟵ v2
                                                              in quicksort(cmp;v1) @ L3 @ quicksort(cmp;v3)

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  A  :  Type
4.  cmp  :  comparison(T)
5.  n  :  \mBbbN{}
6.  L  :  T  List
7.  \mforall{}L1:T  List
          (||L1||  <  ||L||  {}\mRightarrow{}  (\mforall{}[k:(T  List)  {}\mrightarrow{}  A].  (cpsquicksort(cmp;L1;k)  \msim{}  k  quicksort(cmp;L1))))
8.  k  :  (T  List)  {}\mrightarrow{}  A
9.  \mneg{}(L  =  [])
10.  v  :  T
11.  hd(L)  =  v
12.  v1  :  T  List
13.  filter(\mlambda{}z.0  <z  cmp  z  v;L)  =  v1
14.  v2  :  T  List
15.  filter(\mlambda{}z.(0  =\msubz{}  cmp  v  z);L)  =  v2
16.  v3  :  T  List
17.  filter(\mlambda{}z.0  <z  cmp  v  z;L)  =  v3
18.  ||filter(\mlambda{}z.0  <z  cmp  z  v;L)||  <  ||L||  \mwedge{}  ||filter(\mlambda{}z.0  <z  cmp  v  z;L)||  <  ||L||
\mvdash{}  cpsquicksort(cmp;v1;\mlambda{}S1.cpsquicksort(cmp;v3;\mlambda{}S3.(k  (S1  @  v2  @  S3))))  \msim{}  k 
                                                                                                                                                  let  L3  \mleftarrow{}{}  v2
                                                                                                                                                  in  quicksort(cmp;v1)
                                                                                                                                                  @  L3
                                                                                                                                                  @  quicksort(cmp;v3)


By

---

Latex:
xxxRepeatFor  2  ((Reduce  0  THEN  (RWO  "7"  0  THEN  Try  (Complete  (Auto)))\mcdot{}))xxx

---

Home Index