flow-allowed{i:l}(R;dd;G;a;b;T) ==
let S,ds,da = dd in
i:{i:Id| (i 
S)} . j:{j:Id| (i
j)G} .
((
(<(link(a i j) from i to j), b> R-lnktags(R)))
(kfpf-domain(da i).
send-allowed(R;k;(link(a i j) from i to j);[b]))
R-decls-compat(R;es-decl-set-single(j;
;rcv((link(a i j) from i to j),b)
: T)))
Definitions :
spreadn: spread3,
all: x:A. B[x],
id-graph-edge: (ij)G,
not: A,
l_member: (x l),
pair: <a, b>,
product: x:A 
B[x],
IdLnk: IdLnk,
Id: Id,
and: P Q,
l_all: (xL.P[x]),
fpf-domain: fpf-domain(f),
set: {x:A| B[x]} ,
Knd: Knd,
hasloc: hasloc(k;i),
assert: b,
cons: [car / cdr],
nil: [],
R-decls-compat: R-decls-compat(R;dd),
es-decl-set-single: es-decl-set-single(i;ds;da),
fpf-empty: ,
fpf-single: x : v,
rcv: rcv(l,tg),
mk_lnk: (link(n) from i to j),
apply: f a
FDL editor aliases :
flow-allowed
flow-allowed\{i:l\}(R;dd;G;a;b;T) ==
let S,ds,da = dd in
\mforall{}i:\{i:Id| (i \mmember{} S)\} . \mforall{}j:\{j:Id| (i{}\mrightarrow{}j)\mmember{}G\} .
((\mneg{}(<(link(a i j) from i to j), b> \mmember{} R-lnktags(R)))
\mwedge{} (\mforall{}k\mmember{}fpf-domain(da i).\muparrow{}send-allowed(R;k;(link(a i j) from i to j);[b]))
\mwedge{} R-decls-compat(R;es-decl-set-single(j;\motimes{};rcv((link(a i j) from i to j),b) : T)))
Date html generated:
2010_08_27-AM-09_32_31
Last ObjectModification:
2009_12_16-AM-01_10_42
Home
Index