Nuprl Definition : pv8_p1_when_adopted

pv8_p1_when_adopted(Cid;Op;ldrs_uid) ==
  loc,zr.
   let bnum,pvals = zr 
   in z.let ballot_num,active,proposals = z in 
         if eqof(union-deq(  Id;Unit;product-deq(;Id;IntDeq;IdDeq);unit-deq())) bnum ballot_num
         then let proposals' = pv8_p1_update_proposals(Cid;Op) proposals (pv8_p1_pmax(Cid;Op;ldrs_uid) pvals) in
                  <ballot_num, tt, proposals'>
         else <ballot_num, active, proposals>
         fi 


Definitions occuring in Statement :  pv8_p1_update_proposals: pv8_p1_update_proposals(Cid;Op),  pv8_p1_pmax: pv8_p1_pmax(Cid;Op;ldrs_uid),  id-deq: IdDeq,  Id: Id,  ifthenelse: if b then t else f fi ,  btrue: tt,  let: let,  spreadn: spread3,  unit: Unit,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  int: ,  union-deq: union-deq(A;B;a;b),  product-deq: product-deq(A;B;a;b),  unit-deq: unit-deq(),  int-deq: IntDeq,  eqof: eqof(d)
FDL editor aliases :  pv8_p1_when_adopted pv8_p1_when_adopted
pv8\_p1\_when\_adopted(Cid;Op;ldrs$_{uid}$)  ==
    \mlambda{}loc,zr.
      let  bnum,pvals  =  zr 
      in  \mlambda{}z.let  ballot$_{num}$,active,proposals  =  z  in 
                  if  eqof(union-deq(\mBbbZ{}  \mtimes{}  Id;Unit;product-deq(\mBbbZ{};Id;IntDeq;IdDeq);unit-deq()))  bnum  ballot$\mbackslash{}\000Cff5f{num}$
                  then  let  proposals'  =  pv8\_p1\_update\_proposals(Cid;Op)  proposals 
                                                              (pv8\_p1\_pmax(Cid;Op;ldrs$_{uid}$)  pvals)  in
                                    <ballot$_{num}$,  tt,  proposals'>
                  else  <ballot$_{num}$,  active,  proposals>
                  fi 


Date html generated: 2012_02_20-PM-07_30_20
Last ObjectModification: 2012_02_06-PM-01_47_27

Home Index