---

Step * 1 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
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
BY
{ xxxxxxAssert ⌜||L1|| < ||L|| ∧ ||L3|| < ||L||⌝⋅xxxxxx }

1
.....assertion..... 
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)
⊢ ||L1|| < ||L|| ∧ ||L3|| < ||L||

2
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)
17. ||L1|| < ||L|| ∧ ||L3|| < ||L||
⊢ 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
9.  x  :  T
10.  hd(L)  =  x
11.  L1  :  T  List
12.  filter(\mlambda{}z.0  <z  cmp  z  x;L)  =  L1
13.  L2  :  T  List
14.  filter(\mlambda{}z.(0  =\msubz{}  cmp  x  z);L)  =  L2
15.  L3  :  T  List
16.  filter(\mlambda{}z.0  <z  cmp  x  z;L)  =  L3
\mvdash{}  cpsquicksort(cmp;L1;\mlambda{}S1.cpsquicksort(cmp;L3;\mlambda{}S3.(k  (S1  @  L2  @  S3))))  \mmember{}  A


By

---

Latex:
xxxxxxAssert  \mkleeneopen{}||L1||  <  ||L||  \mwedge{}  ||L3||  <  ||L||\mkleeneclose{}\mcdot{}xxxxxx

---

Home Index