---

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-sub: f  g,  Id: Id,  universe: Type,  id-deq: IdDeq,  apply: f a
FDL editor aliases :  es-decl-sets-sub

---

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


Date html generated: 2010_08_27-AM-09_32_15
Last ObjectModification: 2009_12_16-AM-01_09_41

Home Index