---

R-decls-compat(R;dd) ==
  case R of 
  Rnone => True
  Rplus(left,right)=>rec1,rec2.rec1  rec2
  Rinit(loc,T,x,v)=> (loc  |dd|)  x : T || ds(dd;loc)
  Rframe(loc,T,x,L)=> (loc  |dd|)  x : T || ds(dd;loc)
  Rsframe(lnk,tag,L)=> True
  Reffect(loc,ds,knd,T,x,f)=> (loc  |dd|)
   (x : T || ds(dd;loc)  ds || ds(dd;loc)  knd : T || da(dd;loc))
  Rsends(ds,knd,T,l,dt,g)=> ((source(l)  |dd|)
   (knd : T || da(dd;source(l))  ds || ds(dd;source(l))))
   ((destination(l)  |dd|)
     lnk-decl(l;fpf-restrict(dt;tg.deq-member(IdDeq;tg;map(p.(fst(p));
                                                              g)))) || ...)
  Rpre(loc,ds,a,p,P)=> (loc  |dd|)
   (locl(a) : Outcome || da(dd;loc)  ds || ds(dd;loc))
  Raframe(loc,k,L)=> True
  Rbframe(loc,k,L)=> True
  Rrframe(loc,x,L)=> True

---

Definitions :  lsrc: source(l),  lnk-decl: lnk-decl(l;dt),  fpf-restrict: fpf-restrict(f;P),  deq-member: deq-member(eq;x;L),  map: map(f;as),  lambda: x.A[x],  pi1: fst(t),  ldst: destination(l),  implies: P  Q,  l_member: (x  l),  es-decl-set-domain: |dd|,  and: P  Q,  Knd: Knd,  Kind-deq: KindDeq,  fpf-single: x : v,  locl: locl(a),  p-outcome: Outcome,  es-decl-set-da: da(dd;i),  fpf-compatible: f || g,  Id: Id,  universe: Type,  id-deq: IdDeq,  es-decl-set-ds: ds(dd;i),  true: True
FDL editor aliases :  R-decls-compat

---

R-decls-compat(R;dd)  ==
    case  R  of 
    Rnone  =>  True
    Rplus(left,right)=>rec1,rec2.rec1  \mwedge{}  rec2
    Rinit(loc,T,x,v)=>  (loc  \mmember{}  |dd|)  {}\mRightarrow{}  x  :  T  ||  ds(dd;loc)
    Rframe(loc,T,x,L)=>  (loc  \mmember{}  |dd|)  {}\mRightarrow{}  x  :  T  ||  ds(dd;loc)
    Rsframe(lnk,tag,L)=>  True
    Reffect(loc,ds,knd,T,x,f)=>  (loc  \mmember{}  |dd|)
    {}\mRightarrow{}  (x  :  T  ||  ds(dd;loc)  \mwedge{}  ds  ||  ds(dd;loc)  \mwedge{}  knd  :  T  ||  da(dd;loc))
    Rsends(ds,knd,T,l,dt,g)=>  ((source(l)  \mmember{}  |dd|)
    {}\mRightarrow{}  (knd  :  T  ||  da(dd;source(l))  \mwedge{}  ds  ||  ds(dd;source(l))))
    \mwedge{}  ((destination(l)  \mmember{}  |dd|)
        {}\mRightarrow{}  lnk-decl(l;fpf-restrict(dt;\mlambda{}tg.deq-member(IdDeq;tg;map(\mlambda{}p.(fst(p));
                                                                                                                            g))))  ||  da(dd;destination(l)))
    Rpre(loc,ds,a,p,P)=>  (loc  \mmember{}  |dd|)  {}\mRightarrow{}  (locl(a)  :  Outcome  ||  da(dd;loc)  \mwedge{}  ds  ||  ds(dd;loc))
    Raframe(loc,k,L)=>  True
    Rbframe(loc,k,L)=>  True
    Rrframe(loc,x,L)=>  True


Date html generated: 2010_08_27-AM-09_32_25
Last ObjectModification: 2009_12_16-AM-01_10_00

Home Index