Step * 1 1 2 of Lemma cpsquicksort_wf


1. Type
2. Type
3. cmp comparison(T)
4. : ℕ
5. List
6. ¬(L [] ∈ (T List))
7. ∀L1:T List. (||L1|| < ||L||  (∀[k:(T List) ⟶ A]. (cpsquicksort(cmp;L1;k) ∈ A)))
8. (T List) ⟶ A
9. T
10. hd(L) x ∈ T
11. L1 List
12. filter(λz.0 <cmp x;L) L1 ∈ (T List)
13. L2 List
14. filter(λz.(0 =z cmp z);L) L2 ∈ (T List)
15. L3 List
16. filter(λz.0 <cmp z;L) L3 ∈ (T List)
17. ||L1|| < ||L|| ∧ ||L3|| < ||L||
⊢ cpsquicksort(cmp;L1;λS1.cpsquicksort(cmp;L3;λS3.(k (S1 L2 S3)))) ∈ A
BY
RepeatFor ((BackThruSomeHyp⋅ THEN Auto)) }


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
17.  ||L1||  <  ||L||  \mwedge{}  ||L3||  <  ||L||
\mvdash{}  cpsquicksort(cmp;L1;\mlambda{}S1.cpsquicksort(cmp;L3;\mlambda{}S3.(k  (S1  @  L2  @  S3))))  \mmember{}  A


By


Latex:
RepeatFor  2  ((BackThruSomeHyp\mcdot{}  THEN  Auto))




Home Index