Nuprl Definition : pv8_p1_on

Nuprl Definition : pv8_p1_on_propose

pv8_p1_on_propose(Cid;Op;eq_Cid) ==

loc,zq.
let s,p = zq
in

z.let ballot_num,active,proposals = z in
         let proposals' = if pv8_p1_in_domain(Cid;Op) IntDeq s proposals
                          then proposals
                          else pv8_p1_add_if_new() pv8_p1_same_proposal(Cid;Op;eq_Cid) <s, p> proposals
                          fi  in
             <ballot_num, active, proposals'>

Definitions occuring in Statement : pv8_p1_add_if_new: pv8_p1_add_if_new(), pv8_p1_same_proposal: pv8_p1_same_proposal(Cid;Op;eq_Cid), pv8_p1_in_domain: pv8_p1_in_domain(Cid;Op), ifthenelse: if b then t else f fi , let: let, spreadn: spread3, apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, int-deq: IntDeq
FDL editor aliases : pv8_p1_on_propose pv8_p1_on_propose

pv8\_p1\_on\_propose(Cid;Op;eq$_{Cid}$) == \mlambda{}loc,zq. let s,p = zq in \mlambda{}z.let ballot$_{num}$,active,proposals = z in let proposals' = if pv8\_p1\_in\_domain(Cid;Op) IntDeq s proposals then proposals else pv8\_p1\_add\_if\_new() pv8\_p1\_same\_proposal(Cid;Op;eq$_{Cid\mbackslash{}\000Cff7d$) <s, p> proposals fi in <ballot$_{num}$, active, proposals'> Date html generated: 2012_02_20-PM-07_30_03 Last ObjectModification: 2012_02_06-PM-01_47_17 Home Index