Nuprl Definition : processChoose
processChoose(l_comm) ==
RecProcess([];seen,i.if pDVrequest?(i)
then let trip = pDVrequest-rndv2(i) in
let cntr = pDVrequest-counter(i) in
if cntr ∈b seen then <seen, make-lg([])> else <[cntr / seen], make-lg([<l_comm, mk-tagged("msg";pDVselex(trip))>\000C])> fi
else <seen, make-lg([])>
fi )
Definitions occuring in Statement :
pDVrequest-counter: pDVrequest-counter(x),
pDVrequest-rndv2: pDVrequest-rndv2(x),
pDVrequest?: pDVrequest?(x),
pDVselex: pDVselex(rndv1),
make-lg: make-lg(L),
rec-process: RecProcess(s0;s,m.next[s; m]),
deq-member: x ∈b L,
cons: [a / b],
nil: [],
nat-deq: NatDeq,
ifthenelse: if b then t else f fi ,
let: let,
pair: <a, b>,
token: "$token",
mk-tagged: mk-tagged(tg;x)
FDL editor aliases :
processChoose
Latex:
processChoose(l$_{comm}$) ==
RecProcess([];seen,i.if pDVrequest?(i)
then let trip = pDVrequest-rndv2(i) in
let cntr = pDVrequest-counter(i) in
if cntr \mmember{}\msubb{} seen
then <seen, make-lg([])>
else <[cntr / seen], make-lg([<l$_{comm}$, mk-tagged("msg";pDVselex(trip\000C))>])>
fi
else <seen, make-lg([])>
fi )
Date html generated:
2016_05_17-AM-11_30_56
Last ObjectModification:
2012_08_30-PM-01_47_41
Theory : event-logic-applications
Home
Index