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: 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: 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