rec-dataflow-halt-state(A;B;s0;s,a.next[s; a]) ==
a:A. L:A List. ((snd(rec-dataflow(s0;s,a.next[s; a])*(L)(a))) = {})
Definitions occuring in Statement :
iterate-dataflow: P*(inputs),
dataflow-ap: df(a),
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
pi2: snd(t),
all: x:A. B[x],
list: type List,
equal: s = t
Definitions :
all: x:A. B[x],
list: type List,
equal: s = t,
bag: Error :bag,
pi2: snd(t),
dataflow-ap: df(a),
iterate-dataflow: P*(inputs),
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
empty-bag: Error :empty-bag
FDL editor aliases :
rec-dataflow-halt-state
rec-dataflow-halt-state(A;B;s0;s,a.next[s; a]) ==
\mforall{}a:A. \mforall{}L:A List. ((snd(rec-dataflow(s0;s,a.next[s; a])*(L)(a))) = \{\})
Date html generated:
2011_08_10-AM-08_19_55
Last ObjectModification:
2011_03_22-PM-01_38_34
Home
Index