Nuprl Definition : pv8_p1_on

Nuprl Definition : pv8_p1_on_p2a

pv8_p1_on_p2a(Cid;Op;eq_Cid;ldrs_uid) ==

loc,zh.
   let zj,zi = zh
   in let b,sp = zi
      in

z.let ballot_num,accepted = z
            in let ballot_num' = pv8_p1_max_bnum(ldrs_uid) b ballot_num in
                let accepted' = if pv8_p1_leq_bnum(ldrs_uid) ballot_num b
                                then pv8_p1_add_if_new() pv8_p1_same_pvalue(Cid;Op;eq_Cid) <b, sp> accepted
                                else accepted
                                fi  in
                <ballot_num', accepted'>

Definitions occuring in Statement : pv8_p1_add_if_new: pv8_p1_add_if_new(), pv8_p1_same_pvalue: pv8_p1_same_pvalue(Cid;Op;eq_Cid), pv8_p1_max_bnum: pv8_p1_max_bnum(ldrs_uid), pv8_p1_leq_bnum: pv8_p1_leq_bnum(ldrs_uid), ifthenelse: if b then t else f fi , let: let, apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>
FDL editor aliases : pv8_p1_on_p2a pv8_p1_on_p2a

pv8\_p1\_on\_p2a(Cid;Op;eq$_{Cid}$;ldrs$_{uid}$) == \mlambda{}loc,zh. let zj,zi = zh in let b,sp = zi in \mlambda{}z.let ballot$_{num}$,accepted = z in let ballot$_{num'}$ = pv8\_p1\_max\_bnum(ldrs$_{uid}\000C$) b ballot$_{num}$ in let accepted' = if pv8\_p1\_leq\_bnum(ldrs$_{uid}$) ballot$\mbackslash{}ff5\000Cf{num}$ b then pv8\_p1\_add\_if\_new() pv8\_p1\_same\_pvalue(Cid;Op;eq$_{\000CCid}$) <b, sp> accepted else accepted fi in <ballot$_{num'}$, accepted'> Date html generated: 2012_02_20-PM-07_24_50 Last ObjectModification: 2012_02_06-PM-01_43_52 Home Index