Nuprl Definition : ohc_v2_roundout2

ohc_v2_roundout2(Cmd;cmdeq;flrs;learners;locs) ==
  loc,cmd,zi.
   let zj,sender = zi 
   in let zk,cmdU = zj 
      in let n,i = zk 
         in z.let cmdUs,z = z 
               in if (||cmdUs|| = flrs + 1)
                  then let vlist = mapfilter(x.outl(x);x.isl(x);cmdUs) in
                           let k,x = poss-maj(cmdeq;vlist;cmd) 
                           in if (k = flrs + 1)
                                then (ohc_v2_notify'broadcast(Cmd) learners <n, x>)
                                     + (ohc_v2_decided'broadcast() locs n)
                              if null(vlist) then {ohc_v2_retry'send(Cmd) loc <<n, i + 1>, cmd>}
                              else {ohc_v2_retry'send(Cmd) loc <<n, i + 1>, x>}
                              fi 
                  else {}
                  fi 


Definitions occuring in Statement :  ohc_v2_notify'broadcast: ohc_v2_notify'broadcast(Cmd),  ohc_v2_decided'broadcast: ohc_v2_decided'broadcast(),  ohc_v2_retry'send: ohc_v2_retry'send(Cmd),  length: ||as||,  null: null(as),  outl: outl(x),  isl: isl(x),  eq_int: (i = j),  ifthenelse: if b then t else f fi ,  let: let,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n,  mapfilter: mapfilter(f;P;L),  poss-maj: poss-maj(eq;L;x),  bag-append: as + bs,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  ohc_v2_roundout2
ohc\_v2\_roundout2(Cmd;cmdeq;flrs;learners;locs)  ==
    \mlambda{}loc,cmd,zi.
      let  zj,sender  =  zi 
      in  let  zk,cmdU  =  zj 
            in  let  n,i  =  zk 
                  in  \mlambda{}z.let  cmdUs,z  =  z 
                              in  if  (||cmdUs||  =\msubz{}  flrs  +  1)
                                    then  let  vlist  =  mapfilter(\mlambda{}x.outl(x);\mlambda{}x.isl(x);cmdUs)  in
                                                      let  k,x  =  poss-maj(cmdeq;vlist;cmd) 
                                                      in  if  (k  =\msubz{}  flrs  +  1)
                                                                then  (ohc\_v2\_notify'broadcast(Cmd)  learners  <n,  x>)
                                                                          +  (ohc\_v2\_decided'broadcast()  locs  n)
                                                            if  null(vlist)  then  \{ohc\_v2\_retry'send(Cmd)  loc  <<n,  i  +  1>,  cmd>\}
                                                            else  \{ohc\_v2\_retry'send(Cmd)  loc  <<n,  i  +  1>,  x>\}
                                                            fi 
                                    else  \{\}
                                    fi 


Date html generated: 2012_02_20-PM-05_46_53
Last ObjectModification: 2012_02_17-PM-10_22_20

Home Index