Nuprl Definition : pv8_p2_on

Nuprl Definition : pv8_p2_on_decision

pv8_p2_on_decision(Cid;Op;RepState;Result;apply_op;eq_Cid;ldrs) ==

v,state.
   let rstate,slt,proposals,decisions = state
   in let decisions' = pv8_p2_add_if_new(Cid;Op) pv8_p2_same_proposal(Cid;Op;eq_Cid) v decisions in
       let ready = mapfilter(

x.(snd(x));

z.let s,z = z in eqof(IntDeq) s slt;decisions') in
       pv8_p2_iterate_tr(Cid;Op;RepState) pv8_p2_inner_tr(Cid;Op;RepState;Result;apply_op;eq_Cid;ldrs)
       <rstate, slt, proposals, decisions'>
       ready

Definitions occuring in Statement : pv8_p2_inner_tr: pv8_p2_inner_tr(Cid;Op;RepState;Result;apply_op;eq_Cid;ldrs), pv8_p2_iterate_tr: pv8_p2_iterate_tr(Cid;Op;RepState), pv8_p2_add_if_new: pv8_p2_add_if_new(Cid;Op), pv8_p2_same_proposal: pv8_p2_same_proposal(Cid;Op;eq_Cid), let: let, spreadn: spread4, pi2: snd(t), apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, mapfilter: mapfilter(f;P;L), int-deq: IntDeq, eqof: eqof(d)
FDL editor aliases : pv8_p2_on_decision

pv8\_p2\_on\_decision(Cid;Op;RepState;Result;apply$_{op}$;eq$_{Cid}\000C$;ldrs) == \mlambda{}v,state. let rstate,slt,proposals,decisions = state in let decisions' = pv8\_p2\_add\_if\_new(Cid;Op) pv8\_p2\_same\_proposal(Cid;Op;eq$_{Cid\mbackslash{}ff\000C7d$) v decisions in let ready = mapfilter(\mlambda{}x.(snd(x));\mlambda{}z.let s,z = z in eqof(IntDeq) s slt;decisions') in pv8\_p2\_iterate\_tr(Cid;Op;RepState) pv8\_p2\_inner\_tr(Cid;Op;RepState;Result;apply$_\mbackslash{}ff7\000Cbop}$;eq$_{Cid}$;...) <rstate, slt, proposals, decisions'> ready Date html generated: 2012_02_20-PM-07_40_43 Last ObjectModification: 2012_02_06-PM-03_07_43 Home Index