{ 
[F,es,e:Top].
(e 
dataflow-set-class(x.F[x])
~ (bag-size(dataflow-history-val(es;e;x.F[x])) =
1)) }
{ Proof }
Definitions occuring in Statement :
dataflow-set-class: dataflow-set-class(x.P[x]),
dataflow-history-val: dataflow-history-val(es;e;x.P[x]),
in-eclass: e X,
eq_int: (i = j),
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
natural_number: $n,
sqequal: s ~ t,
bag-size: bag-size(bs)
Definitions :
lambda: 
x.A[x],
in-eclass: e X,
dataflow-set-class: dataflow-set-class(x.P[x]),
uall: [x:A]. B[x],
isect: 
x:A. B[x],
sqequal: s ~ t,
equal: s = t,
member: t T,
top: Top,
all: x:A. B[x],
function: x:A 
B[x],
Auto: Error :Auto,
RepUR: Error :RepUR,
CollapseTHEN: Error :CollapseTHEN,
CollapseTHENA: Error :CollapseTHENA,
tactic: Error :tactic
Lemmas :
top_wf
\mforall{}[F,es,e:Top].
(e \mmember{}\msubb{} dataflow-set-class(x.F[x]) \msim{} (bag-size(dataflow-history-val(es;e;x.F[x])) =\msubz{} 1))
Date html generated:
2011_08_16-PM-06_12_42
Last ObjectModification:
2011_06_20-AM-01_50_29
Home
Index