Nuprl Definition : pv8_p1_when_preempted

pv8_p1_when_preempted(Cid;Op;ldrs_uid) ==
  ldr,bnum,z.
   let ballot_num,active,proposals = z in 
   if isl(bnum)  (pv8_p1_lt_bnum(ldrs_uid) ballot_num bnum)
   then let r',loc' = outl(bnum) 
        in <inl <r' + 1, ldr> , ff, proposals>
   else <ballot_num, active, proposals>
   fi 


Definitions occuring in Statement :  pv8_p1_lt_bnum: pv8_p1_lt_bnum(ldrs_uid),  outl: outl(x),  isl: isl(x),  band: p  q,  ifthenelse: if b then t else f fi ,  bfalse: ff,  spreadn: spread3,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  inl: inl x ,  add: n + m,  natural_number: $n
FDL editor aliases :  pv8_p1_when_preempted pv8_p1_when_preempted
pv8\_p1\_when\_preempted(Cid;Op;ldrs$_{uid}$)  ==
    \mlambda{}ldr,bnum,z.
      let  ballot$_{num}$,active,proposals  =  z  in 
      if  isl(bnum)  \mwedge{}\msubb{}  (pv8\_p1\_lt\_bnum(ldrs$_{uid}$)  ballot$_{num}\mbackslash{}f\000Cf24  bnum)
      then  let  r',loc'  =  outl(bnum) 
                in  <inl  <r'  +  1,  ldr>  ,  ff,  proposals>
      else  <ballot$_{num}$,  active,  proposals>
      fi 


Date html generated: 2012_02_20-PM-07_30_34
Last ObjectModification: 2012_02_06-PM-01_47_37

Home Index