Nuprl Definition : pv8_p1_LeaderPreempted

pv8_p1_LeaderPreempted(Cid;Op;eq_Cid;ldrs_uid) ==
  let f = ldr,bnum,z.
           let ballot_num,zu,z = z in 
           if isl(bnum)  (pv8_p1_lt_bnum(ldrs_uid) ballot_num bnum)
           then {inl <(fst(outl(bnum))) + 1, ldr> }
           else {}
           fi  in
      f@Loc|Loc,pv8_p1_preempted'base(), pv8_p1_LeaderState(Cid;Op;eq_Cid;ldrs_uid)|


Definitions occuring in Statement :  pv8_p1_LeaderState: pv8_p1_LeaderState(Cid;Op;eq_Cid;ldrs_uid),  pv8_p1_preempted'base: pv8_p1_preempted'base(),  pv8_p1_lt_bnum: pv8_p1_lt_bnum(ldrs_uid),  concat-lifting-loc-2: f@Loc,  simple-loc-comb-2: F|Loc,X, Y|,  outl: outl(x),  isl: isl(x),  band: p  q,  ifthenelse: if b then t else f fi ,  let: let,  spreadn: spread3,  pi1: fst(t),  apply: f a,  lambda: x.A[x],  pair: <a, b>,  inl: inl x ,  add: n + m,  natural_number: $n,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  pv8_p1_LeaderPreempted pv8_p1_LeaderPreempted
pv8\_p1\_LeaderPreempted(Cid;Op;eq$_{Cid}$;ldrs$_{uid}$)  ==
    let  f  =  \mlambda{}ldr,bnum,z.
                      let  ballot$_{num}$,zu,z  =  z  in 
                      if  isl(bnum)  \mwedge{}\msubb{}  (pv8\_p1\_lt\_bnum(ldrs$_{uid}$)  ballot$_{nu\000Cm}$  bnum)
                      then  \{inl  <(fst(outl(bnum)))  +  1,  ldr>  \}
                      else  \{\}
                      fi    in
            f@Loc|Loc,pv8\_p1\_preempted'base(),  pv8\_p1\_LeaderState(Cid;Op;eq$_{Cid}$;ld\000Crs$_{uid}$)|


Date html generated: 2012_02_20-PM-07_32_12
Last ObjectModification: 2012_02_06-PM-01_48_32

Home Index