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))>])>
        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), nat-deq: NatDeq, cons: [a / b], nil: [], 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: 2015_07_23-AM-11_36_32 Last ObjectModification: 2012_08_30-PM-01_47_41 Home Index