---

Step * 1 1 1 of Lemma cpsquicksort_wf

.....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||
BY
{ Auto }

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)
⊢ ||L1|| < ||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||

---

Latex:

---

Latex:
.....assertion..... 
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{}  ||L1||  <  ||L||  \mwedge{}  ||L3||  <  ||L||


By

---

Latex:
Auto

---

Home Index