---

dd1 || dd2 ==
  let S1,ds1,da1 = dd1 in 
  let S2,ds2,da2 = dd2 in 
  i:Id. ((i  S1)  (i  S2)  (da1 i || da2 i  ds1 i || ds2 i))

---

Definitions :  spreadn: spread3,  all: x:A. B[x],  implies: P  Q,  l_member: (x  l),  and: P  Q,  set: {x:A| B[x]} ,  Knd: Knd,  assert: b,  hasloc: hasloc(k;i),  Kind-deq: KindDeq,  fpf-compatible: f || g,  Id: Id,  universe: Type,  id-deq: IdDeq,  apply: f a
FDL editor aliases :  es-decl-sets-compatible

---

dd1  ||  dd2  ==
    let  S1,ds1,da1  =  dd1  in 
    let  S2,ds2,da2  =  dd2  in 
    \mforall{}i:Id.  ((i  \mmember{}  S1)  {}\mRightarrow{}  (i  \mmember{}  S2)  {}\mRightarrow{}  (da1  i  ||  da2  i  \mwedge{}  ds1  i  ||  ds2  i))


Date html generated: 2010_08_27-AM-09_32_05
Last ObjectModification: 2009_12_16-AM-01_09_25

Home Index