Nuprl Definition : pv8_p1_LeaderPropose

pv8_p1_LeaderPropose(Cid;Op;eq_Cid;ldrs_uid) ==
  let f = loc,zs.
           let s,p = zs 
           in z.let ballot_num,active,proposals = z in 
                 if active  ((pv8_p1_in_domain(Cid;Op) IntDeq s proposals)) then {<ballot_num, s, p>} else {} fi  in
      f@Loc|Loc,pv8_p1_propose'base(Cid;Op), 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_propose'base: pv8_p1_propose'base(Cid;Op),  pv8_p1_in_domain: pv8_p1_in_domain(Cid;Op),  concat-lifting-loc-2: f@Loc,  simple-loc-comb-2: F|Loc,X, Y|,  band: p  q,  bnot: b,  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,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  pv8_p1_LeaderPropose pv8_p1_LeaderPropose
pv8\_p1\_LeaderPropose(Cid;Op;eq$_{Cid}$;ldrs$_{uid}$)  ==
    let  f  =  \mlambda{}loc,zs.
                      let  s,p  =  zs 
                      in  \mlambda{}z.let  ballot$_{num}$,active,proposals  =  z  in 
                                  if  active  \mwedge{}\msubb{}  (\mneg{}\msubb{}(pv8\_p1\_in\_domain(Cid;Op)  IntDeq  s  proposals))
                                  then  \{<ballot$_{num}$,  s,  p>\}
                                  else  \{\}
                                  fi    in
            f@Loc|Loc,pv8\_p1\_propose'base(Cid;Op),  pv8\_p1\_LeaderState(Cid;Op;eq$_{Cid}\mbackslash{}ff2\000C4;ldrs$_{uid}$)|


Date html generated: 2012_02_20-PM-07_31_21
Last ObjectModification: 2012_02_06-PM-01_48_02

Home Index