Nuprl Definition : pv8_p2

Nuprl Definition : pv8_p2_propose

pv8_p2_propose(Cid;Op;RepState;eq_Cid;ldrs) ==

cmd,state.
let rstate,slt,proposals,decisions = state
in if (

zi

map(

x.(snd(x));decisions).pv8_p2_same_command(Cid;Op;eq_Cid) cmd zi)_b
then <state, {}>
else let slt' = pv8_p2_first_unoccupied() map(

x.(fst(x));proposals @ decisions) in
            let proposals' = pv8_p2_add_if_new(Cid;Op) pv8_p2_same_proposal(Cid;Op;eq_Cid) <slt', cmd> proposals in
            let msgs = pv8_p2_propose'broadcast(Cid;Op) ldrs <slt', cmd> in
            <<rstate, slt, proposals', decisions>, msgs>
      fi

Definitions occuring in Statement : pv8_p2_first_unoccupied: pv8_p2_first_unoccupied(), pv8_p2_propose'broadcast: pv8_p2_propose'broadcast(Cid;Op), pv8_p2_add_if_new: pv8_p2_add_if_new(Cid;Op), pv8_p2_same_proposal: pv8_p2_same_proposal(Cid;Op;eq_Cid), pv8_p2_same_command: pv8_p2_same_command(Cid;Op;eq_Cid), map: map(f;as), append: as @ bs, ifthenelse: if b then t else f fi , let: let, spreadn: spread4, pi1: fst(t), pi2: snd(t), apply: f a, lambda:

x.A[x], pair: <a, b>, empty-bag: {}, bl-exists: (

x

L.P[x])_b
FDL editor aliases : pv8_p2_propose pv8_p2_propose

pv8\_p2\_propose(Cid;Op;RepState;eq$_{Cid}$;ldrs) == \mlambda{}cmd,state. let rstate,slt,proposals,decisions = state in if (\mexists{}zi\mmember{}map(\mlambda{}x.(snd(x));decisions).pv8\_p2\_same\_command(Cid;Op;eq$_{Cid}$) \000Ccmd zi)\_b then <state, \{\}> else let slt' = pv8\_p2\_first\_unoccupied() map(\mlambda{}x.(fst(x));proposals @ decisions) in let proposals' = pv8\_p2\_add\_if\_new(Cid;Op) pv8\_p2\_same\_proposal(Cid;Op;eq$_{\000CCid}$) <slt', cmd> proposals in let msgs = pv8\_p2\_propose'broadcast(Cid;Op) ldrs <slt', cmd> in <<rstate, slt, proposals', decisions>, msgs> fi Date html generated: 2012_02_20-PM-07_39_50 Last ObjectModification: 2012_02_06-PM-03_07_12 Home Index