{ 
[A:Type]. [P:{L:A List| 0 < ||L||} 
].
(collect_filter() 
{s:
{L:A List| (0 < ||L||) 
(
P[L])}
({L:A List| (0 < ||L||) 
(P[L])} + Top)|
(isl(snd(snd(s)))) (1 
(fst(s)))}
bag(
{L:A List| (0 < ||L||) (P[L])} )) }
{ Proof }
Definitions occuring in Statement :
collect_filter: collect_filter(),
length: ||as||,
isl: isl(x),
assert: b,
bool: ,
nat: ,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
le: A B,
not: A,
implies: P Q,
and: P Q,
member: t T,
less_than: a < b,
set: {x:A| B[x]} ,
function: x:A B[x],
product: x:A B[x],
union: left + right,
list: type List,
natural_number: $n,
int: ,
universe: Type,
bag: bag(T)
Definitions :
so_lambda: 
x.t[x],
empty-bag: {},
minus: -n,
add: n + m,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
real: 
,
rationals: 
,
subtype: S 
T,
subtract: n - m,
pair: <a, b>,
nil: [],
prop: 
,
cand: A c B,
single-bag: {x},
true: True,
lambda: x.A[x],
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
ge: i 
j ,
uimplies: b supposing a,
uiff: uiff(P;Q),
subtype_rel: A r B,
void: Void,
false: False,
all: x:A. B[x],
universe: Type,
uall: [x:A]. B[x],
bool: ,
isect: 
x:A. B[x],
member: t T,
equal: s = t,
int: ,
not: A,
union: left + right,
top: Top,
implies: P Q,
function: x:A B[x],
isl: isl(x),
pi2: snd(t),
le: A B,
pi1: fst(t),
bag: bag(T),
nat: ,
set: {x:A| B[x]} ,
list: type List,
and: P Q,
product: x:A B[x],
less_than: a < b,
natural_number: $n,
length: ||as||,
assert: b,
so_apply: x[s],
apply: f a,
collect_filter: collect_filter(),
axiom: Ax,
MaAuto: Error :MaAuto,
CollapseTHEN: Error :CollapseTHEN,
D: Error :D,
RepeatFor: Error :RepeatFor,
Try: Error :Try,
Unfold: Error :Unfold,
Auto: Error :Auto,
tactic: Error :tactic
Lemmas :
empty-bag_wf,
nat_wf,
assert_wf,
le_wf,
false_wf,
not_wf,
member_wf,
length_wf1,
single-bag_wf,
top_wf,
bool_wf,
bag_wf,
pi2_wf,
isl_wf,
pi1_wf_top
\mforall{}[A:Type]. \mforall{}[P:\{L:A List| 0 < ||L||\} {}\mrightarrow{} \mBbbB{}].
(collect\_filter() \mmember{} \{s:\mBbbZ{}
\mtimes{} \{L:A List| (0 < ||L||) {}\mRightarrow{} (\mneg{}\muparrow{}P[L])\}
\mtimes{} (\{L:A List| (0 < ||L||) \mwedge{} (\muparrow{}P[L])\} + Top)|
(\muparrow{}isl(snd(snd(s)))) {}\mRightarrow{} (1 \mleq{} (fst(s)))\} {}\mrightarrow{} bag(\mBbbN{} \mtimes{} \{L:A List|
(0 < ||L||) \mwedge{} (\muparrow{}P[L])\} ))
Date html generated:
2011_08_16-AM-11_03_47
Last ObjectModification:
2011_06_18-AM-09_36_55
Home
Index