Step
*
1
2
1
3
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
9. quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)) = quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)) ∈ (T List)
10. sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)))
11. permutation(T;quicksort(cmp;filter(λz.0 <z cmp z hd(L);L));filter(λz.0 <z cmp z hd(L);L))
12. quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)) = quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)) ∈ (T List)
13. sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)))
14. permutation(T;quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L));filter(λz.0 <z cmp hd(L) z;L))
⊢ sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp z hd(L);L))
@ filter(λz.(0 =z cmp hd(L) z);L)
@ quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)))
BY
{ (RWO "sorted-by-append" 0 THEN Auto) }
1
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
9. quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)) = quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)) ∈ (T List)
10. sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)))
11. permutation(T;quicksort(cmp;filter(λz.0 <z cmp z hd(L);L));filter(λz.0 <z cmp z hd(L);L))
12. quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)) = quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)) ∈ (T List)
13. sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)))
14. permutation(T;quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L));filter(λz.0 <z cmp hd(L) z;L))
15. sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)))
⊢ sorted-by(λx,y. (0 ≤ (cmp x y));filter(λz.(0 =z cmp hd(L) z);L) @ quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)))
2
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
9. quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)) = quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)) ∈ (T List)
10. sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)))
11. permutation(T;quicksort(cmp;filter(λz.0 <z cmp z hd(L);L));filter(λz.0 <z cmp z hd(L);L))
12. quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)) = quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)) ∈ (T List)
13. sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)))
14. permutation(T;quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L));filter(λz.0 <z cmp hd(L) z;L))
15. sorted-by(λx,y. (0 ≤ (cmp x y));quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)))
16. sorted-by(λx,y. (0 ≤ (cmp x y));filter(λz.(0 =z cmp hd(L) z);L) @ quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)))
⊢ (∀a∈quicksort(cmp;filter(λz.0 <z cmp z hd(L);L)).(∀b∈filter(λz.(0 =z cmp hd(L) z);L)
@ quicksort(cmp;filter(λz.0 <z cmp hd(L) z;L)).(λx,y. (0 ≤ (cmp x
y)))
a
b))
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
9. quicksort(cmp;filter(\mlambda{}z.0 <z cmp z hd(L);L)) = quicksort(cmp;filter(\mlambda{}z.0 <z cmp z hd(L);L))
10. sorted-by(\mlambda{}x,y. (0 \mleq{} (cmp x y));quicksort(cmp;filter(\mlambda{}z.0 <z cmp z hd(L);L)))
11. permutation(T;quicksort(cmp;filter(\mlambda{}z.0 <z cmp z hd(L);L));filter(\mlambda{}z.0 <z cmp z hd(L);L))
12. quicksort(cmp;filter(\mlambda{}z.0 <z cmp hd(L) z;L)) = quicksort(cmp;filter(\mlambda{}z.0 <z cmp hd(L) z;L))
13. sorted-by(\mlambda{}x,y. (0 \mleq{} (cmp x y));quicksort(cmp;filter(\mlambda{}z.0 <z cmp hd(L) z;L)))
14. permutation(T;quicksort(cmp;filter(\mlambda{}z.0 <z cmp hd(L) z;L));filter(\mlambda{}z.0 <z cmp hd(L) z;L))
\mvdash{} sorted-by(\mlambda{}x,y. (0 \mleq{} (cmp x y));quicksort(cmp;filter(\mlambda{}z.0 <z cmp z hd(L);L))
@ filter(\mlambda{}z.(0 =\msubz{} cmp hd(L) z);L)
@ quicksort(cmp;filter(\mlambda{}z.0 <z cmp hd(L) z;L)))
By
Latex:
(RWO "sorted-by-append" 0 THEN Auto)
Home
Index