Nuprl Definition : ohc_v2_Phase2

ohc_v2_Phase2(Cmd;cmdeq;flrs;learners;locs) ==
  ni,z.
   let cmdU,cmd = z 
   in ohc_v2_SendVotes(Cmd;locs) ni cmdU || once-class(ohc_v2_Quorum2(Cmd;cmdeq;flrs;learners;locs) ni cmd)


Definitions occuring in Statement :  ohc_v2_SendVotes: ohc_v2_SendVotes(Cmd;locs),  ohc_v2_Quorum2: ohc_v2_Quorum2(Cmd;cmdeq;flrs;learners;locs),  once-class: once-class(X),  parallel-class: X || Y,  apply: f a,  lambda: x.A[x],  spread: spread def
FDL editor aliases :  ohc_v2_Phase2
ohc\_v2\_Phase2(Cmd;cmdeq;flrs;learners;locs)  ==
    \mlambda{}ni,z.
      let  cmdU,cmd  =  z 
      in  ohc\_v2\_SendVotes(Cmd;locs)  ni  cmdU  ||  once-class(ohc\_v2\_Quorum2(Cmd;cmdeq;flrs;learners;locs) 
                                                                                                              ni 
                                                                                                              cmd)


Date html generated: 2012_02_20-PM-05_48_20
Last ObjectModification: 2012_02_17-PM-10_23_20

Home Index