Nuprl Definition : Comm-next-selex
Comm-next-selex(l_comm;piD;cSt) ==
let rndv = pDVselex-rndv1(piD) in
let val = snd(snd(snd(rndv))) in
let i = fst(rndv) in
let loc = fst(snd(rndv)) in
let j = fst(snd(snd(rndv))) in
let cSt' = fpf-restrict(Comm-st(cSt);λx.(¬bx = loc)) in
<<cSt', Comm-q(cSt), Comm-req_from(cSt), ff, Comm-count(cSt)>
, make-lg([<l_comm, mk-tagged("msg";pDVcontinue())>; <Comm-req_from(cSt), mk-tagged("msg";pDVmsg(val;i))>; <loc, mk-t\000Cagged("msg";pDVmsg(val;j))>])
>
Definitions occuring in Statement :
Comm-count: Comm-count(cSt),
Comm-req_from: Comm-req_from(cSt),
Comm-q: Comm-q(cSt),
Comm-st: Comm-st(cSt),
pDVselex-rndv1: pDVselex-rndv1(x),
pDVcontinue: pDVcontinue(),
pDVmsg: pDVmsg(val;index),
make-lg: make-lg(L),
fpf-restrict: fpf-restrict(f;P),
eq_id: a = b,
cons: [a / b],
nil: [],
bnot: ¬bb,
bfalse: ff,
let: let,
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x],
pair: <a, b>,
token: "$token",
mk-tagged: mk-tagged(tg;x)
FDL editor aliases :
Comm-next-selex
Latex:
Comm-next-selex(l$_{comm}$;piD;cSt) ==
let rndv = pDVselex-rndv1(piD) in
let val = snd(snd(snd(rndv))) in
let i = fst(rndv) in
let loc = fst(snd(rndv)) in
let j = fst(snd(snd(rndv))) in
let cSt' = fpf-restrict(Comm-st(cSt);\mlambda{}x.(\mneg{}\msubb{}x = loc)) in
<<cSt', Comm-q(cSt), Comm-req\_from(cSt), ff, Comm-count(cSt)>
, make-lg([<l$_{comm}$, mk-tagged("msg";pDVcontinue())>
<Comm-req\_from(cSt), mk-tagged("msg";pDVmsg(val;i))>
<loc, mk-tagged("msg";pDVmsg(val;j))>])
>
Date html generated:
2016_05_17-AM-11_33_17
Last ObjectModification:
2012_08_30-PM-01_49_17
Theory : event-logic-applications
Home
Index