---

decl-set-read-allowed(R;dd) ==
  let S,ds,da = dd in 
  i:{i:Id| (i  S)} 
    (kfpf-domain(da i).read-allowed(R;k;i;fpf-domain(ds i)))

---

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

---

decl-set-read-allowed(R;dd)  ==
    let  S,ds,da  =  dd  in 
    \mforall{}i:\{i:Id|  (i  \mmember{}  S)\}  .  (\mforall{}k\mmember{}fpf-domain(da  i).\muparrow{}read-allowed(R;k;i;fpf-domain(ds  i)))


Date html generated: 2010_08_27-AM-09_32_22
Last ObjectModification: 2009_12_16-AM-01_09_54

Home Index