Step * 1 1 of Lemma cpsquicksort-quicksort


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


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{}  (\mlambda{}S3.(k  (quicksort(cmp;v1)  @  v2  @  S3)))  quicksort(cmp;v3)  \msim{}  k 
                                                                                                                            let  L3  \mleftarrow{}{}  v2
                                                                                                                            in  quicksort(cmp;v1)
                                                                                                                            @  L3
                                                                                                                            @  quicksort(cmp;v3)


By


Latex:
(Reduce  0\mcdot{}  THEN  (CallByValueReduce  0  THENA  Auto)\mcdot{}  THEN  Auto)




Home Index