Nuprl Definition : state-var-allowed
state-var-allowed{i:l}(R;dd;x;T) ==
let S,ds,da = dd in
∀i:{i:Id| (i ∈ S)}
(l_all(fpf-domain(da i); Knd; k.(↑read-allowed(R;k;i;[x])) ∧ (↑write-allowed(R;k;i;x)))
∧ (¬↑R-affects(R;x;i))
∧ R-decls-compat(R;es-decl-set-single(i;x : 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),
Knd: Knd,
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
FDL editor aliases :
state-var-allowed
state-var-allowed\{i:l\}(R;dd;x;T) ==
let S,ds,da = dd in
\mforall{}i:\{i:Id| (i \mmember{} S)\}
(l\_all(fpf-domain(da i); Knd; k.(\muparrow{}read-allowed(R;k;i;[x])) \mwedge{} (\muparrow{}write-allowed(R;k;i;x)))
\mwedge{} (\mneg{}\muparrow{}R-affects(R;x;i))
\mwedge{} R-decls-compat(R;es-decl-set-single(i;x : T;\motimes{})))
Date html generated:
2015_07_17-AM-11_57_44
Last ObjectModification:
2013_03_27-AM-10_39_15
Home
Index