---

public-decls(R;dd) ==
  let S,ds,da = dd in 
  i:{i:Id| (i  S)} 
    ((kfpf-domain(da i).(write-restricted(R;i;k))
         (send-restricted(R;i;k)))
     (yfpf-domain(ds i).read-restricted(R;i;y)))

---

Definitions :  spreadn: spread3,  all: x:A. B[x],  set: {x:A| B[x]} ,  l_member: (x  l),  Knd: Knd,  and: P  Q,  l_all: (xL.P[x]),  fpf-domain: fpf-domain(f),  apply: f a,  Id: Id,  not: A,  assert: b
FDL editor aliases :  public-decls

---

public-decls(R;dd)  ==
    let  S,ds,da  =  dd  in 
    \mforall{}i:\{i:Id|  (i  \mmember{}  S)\} 
        ((\mforall{}k\mmember{}fpf-domain(da  i).(\mneg{}\muparrow{}write-restricted(R;i;k))  \mwedge{}  (\mneg{}\muparrow{}send-restricted(R;i;k)))
        \mwedge{}  (\mforall{}y\mmember{}fpf-domain(ds  i).\mneg{}\muparrow{}read-restricted(R;i;y)))


Date html generated: 2010_08_27-AM-09_32_33
Last ObjectModification: 2009_12_16-AM-01_10_48

Home Index