Nuprl Definition : flow-allowed
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)))
∧ l_all(fpf-domain(da i); {k:Knd| ↑hasloc(k;i)} ; k.↑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 occuring in Statement :
R-decls-compat: R-decls-compat(R;dd),
es-decl-set-single: es-decl-set-single(i;ds;da),
fpf-single: x : v,
fpf-empty: ⊗,
fpf-domain: fpf-domain(f),
hasloc: hasloc(k;i),
rcv: rcv(l,tg),
Knd: Knd,
mk_lnk: (link(n) from i to j),
IdLnk: IdLnk,
id-graph-edge: (i─→j)∈G,
Id: Id,
l_member: (x ∈ l),
cons: [a / b],
nil: [],
assert: ↑b,
spreadn: spread3,
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
pair: <a, b>,
product: x:A × B[x]
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{} l\_all(fpf-domain(da i); \{k:Knd| \muparrow{}hasloc(k;i)\} ; k.\muparrow{}send-allowed(R;k;(link(a i j) from i to j);\000C[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:
2015_07_17-AM-11_58_10
Last ObjectModification:
2013_03_27-AM-10_39_20
Home
Index