{ 
[Info:Type]. [es:EO+(Info)]. [A,B:Type]. [f:A 
bag(B)]. [X:EClass(A)].
[e:E].
uiff(
e 
f[X];{(e X) 
(bag-size(f X(e)) = 1)}) }
{ Proof }
Definitions occuring in Statement :
es-filter-image: f[X],
eclass-val: X(e),
in-eclass: e X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
guard: {T},
and: P Q,
apply: f a,
function: x:A B[x],
natural_number: $n,
int: 
,
universe: Type,
equal: s = t,
bag-size: bag-size(bs),
bag: bag(T)
Definitions :
guard: {T},
isect: 
x:A. B[x],
uall: [x:A]. B[x],
Try: Error :Try,
Unfold: Error :Unfold,
CollapseTHEN: Error :CollapseTHEN
Lemmas :
es-is-filter-image
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[A,B:Type]. \mforall{}[f:A {}\mrightarrow{} bag(B)]. \mforall{}[X:EClass(A)]. \mforall{}[e:E].
uiff(\muparrow{}e \mmember{}\msubb{} f[X];\{(\muparrow{}e \mmember{}\msubb{} X) \mwedge{} (bag-size(f X(e)) = 1)\})
Date html generated:
2011_08_16-PM-04_11_28
Last ObjectModification:
2011_06_20-AM-00_43_28
Home
Index