Nuprl Definition : R-decls-compat

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.tg ∈b map(λp.(fst(p));g)))) || da(dd;destination(l)))
  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 occuring in Statement :  es-decl-set-da: da(dd;i),  es-decl-set-ds: ds(dd;i),  es-decl-set-domain: |dd|,  lnk-decl: lnk-decl(l;dt),  fpf-restrict: fpf-restrict(f;P),  fpf-single: x : v,  fpf-compatible: f || g,  Kind-deq: KindDeq,  ldst: destination(l),  lsrc: source(l),  locl: locl(a),  Knd: Knd,  id-deq: IdDeq,  Id: Id,  deq-member: x ∈b L),  l_member: (x ∈ l),  map: map(f;as),  pi1: fst(t),  implies: P ⇒ Q,  and: P ∧ Q,  true: True,  lambda: λx.A[x],  universe: Type,  p-outcome: Outcome
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.tg  \mmember{}\msubb{}  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: 2015_07_17-AM-11_57_38
Last ObjectModification: 2013_03_27-AM-10_39_13

Home Index