{ 
[A:Type]. [P:{L:A List| 0 < ||L||} 
].
(collect_filter() 
{L:A List| (0 < ||L||) 
(
P[L])}
({L:A List| (0 < ||L||) 
(P[L])} + Top)
bag( {L:A List| (0 < ||L||) (P[L])} )) }
{ Proof }
Definitions occuring in Statement :
collect_filter: collect_filter(),
length: ||as||,
assert: b,
bool: ,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
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 :
inr: inr x ,
inl: inl x ,
empty-bag: {},
subtract: n - m,
pair: <a, b>,
single-bag: {x},
decide: case b of inl(x) => s[x] | inr(y) => t[y],
spread: spread def,
or: P 
Q,
guard: {T},
uimplies: b supposing a,
eq_knd: a = b,
l_member: (x l),
fpf-dom: x dom(f),
fpf: a:A fp-> B[a],
nil: [],
prop: 
,
cand: A c B,
permutation: permutation(T;L1;L2),
quotient: x,y:A//B[x; y],
spreadn: spread3,
lambda: 
x.A[x],
all: x:A. B[x],
universe: Type,
uall: [x:A]. B[x],
bool: ,
isect: 
x:A. B[x],
member: t T,
not: A,
union: left + right,
top: Top,
bag: bag(T),
and: P Q,
natural_number: $n,
length: ||as||,
assert: b,
so_apply: x[s],
apply: f a,
collect_filter: collect_filter(),
axiom: Ax,
equal: s = t,
int: ,
product: x:A B[x],
set: {x:A| B[x]} ,
list: type List,
implies: P Q,
function: x:A B[x],
less_than: a < b
Lemmas :
bool_wf,
permutation_wf,
bag_wf,
member_wf,
single-bag_wf,
empty-bag_wf,
not_wf,
assert_wf,
length_wf1,
top_wf
\mforall{}[A:Type]. \mforall{}[P:\{L:A List| 0 < ||L||\} {}\mrightarrow{} \mBbbB{}].
(collect\_filter() \mmember{} \mBbbZ{}
\mtimes{} \{L:A List| (0 < ||L||) {}\mRightarrow{} (\mneg{}\muparrow{}P[L])\}
\mtimes{} (\{L:A List| (0 < ||L||) \mwedge{} (\muparrow{}P[L])\} + Top)
{}\mrightarrow{} bag(\mBbbZ{} \mtimes{} \{L:A List| (0 < ||L||) \mwedge{} (\muparrow{}P[L])\} ))
Date html generated:
2011_08_16-AM-11_03_36
Last ObjectModification:
2011_06_18-AM-09_36_49
Home
Index