---

Step * 1 1 1 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)
⊢ ||filter(λz.0 <z cmp z x;L)|| < ||L||
BY
{ (RevHypSubst' -7 0 THEN 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)
⊢ ||filter(λz@0.0 <z cmp z@0 hd(L);L)|| < ||L||

---

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{}  ||filter(\mlambda{}z.0  <z  cmp  z  x;L)||  <  ||L||


By

---

Latex:
(RevHypSubst'  -7  0  THEN  Auto)

---

Home Index