Nuprl Definition : pv8_p2_inner_tr
pv8_p2_inner_tr(Cid;Op;RepState;Result;apply_op;eq_Cid;ldrs) ==
cmd,state.
let rstate,slt,proposals,decisions = state
in let to_repropose = mapfilter(x.(snd(x));pv8_p2_diff_proposal(Cid;Op;eq_Cid) <slt, cmd>;proposals) in
let new_state,proposes = pv8_p2_iterate_tr(Cid;Op;RepState) pv8_p2_propose(Cid;Op;RepState;eq_Cid;ldrs) state
to_repropose
in let new_state',responses = pv8_p2_perform(Cid;Op;RepState;Result;apply_op;eq_Cid) cmd new_state
in <new_state', proposes + responses>
Definitions occuring in Statement :
pv8_p2_perform: pv8_p2_perform(Cid;Op;RepState;Result;apply_op;eq_Cid),
pv8_p2_propose: pv8_p2_propose(Cid;Op;RepState;eq_Cid;ldrs),
pv8_p2_iterate_tr: pv8_p2_iterate_tr(Cid;Op;RepState),
pv8_p2_diff_proposal: pv8_p2_diff_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),
bag-append: as + bs
FDL editor aliases :
pv8_p2_inner_tr
pv8_p2_inner_tr
pv8\_p2\_inner\_tr(Cid;Op;RepState;Result;apply$_{op}$;eq$_{Cid}\mbackslash{}ff\000C24;ldrs) ==
\mlambda{}cmd,state.
let rstate,slt,proposals,decisions = state
in let to$_{repropose}$ = mapfilter(\mlambda{}x.(snd(x));
pv8\_p2\_diff\_proposal(Cid;Op;eq$_{Cid}$) <slt, \000Ccmd>
proposals) in
let new$_{state}$,proposes = pv8\_p2\_iterate\_tr(Cid;Op;RepState)
pv8\_p2\_propose(Cid;Op;RepState;eq$_{Cid}$;ldrs\000C)
state
to$_{repropose}$
in let new$_{state'}$,responses = pv8\_p2\_perform(Cid;Op;RepState;Resul\000Ct;apply$_{op}$;eq$_{Cid}$) cmd
new$_{state}$
in <new$_{state'}$, proposes + responses>
Date html generated:
2012_02_20-PM-07_40_25
Last ObjectModification:
2012_02_06-PM-03_07_32
Home
Index