Nuprl Definition : ohc_v1_roundout2

ohc_v1_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 cmds,z = z 
               in if (||cmds|| = flrs + 1)
                  then let vlist = ohc_v1_prune_off_units(Cmd) [cmdU / cmds] in
                           let k,x = poss-maj(cmdeq;vlist;cmd) 
                           in if (k = flrs + 1)
                                then (ohc_v1_notify'broadcast(Cmd) learners <n, x>)
                                     + (ohc_v1_decided'broadcast() locs n)
                              if null(vlist) then {ohc_v1_retry'send(Cmd) loc <<n, i + 1>, cmd>}
                              else {ohc_v1_retry'send(Cmd) loc <<n, i + 1>, x>}
                              fi 
                  else {}
                  fi 


Definitions occuring in Statement :  ohc_v1_prune_off_units: ohc_v1_prune_off_units(Cmd),  ohc_v1_notify'broadcast: ohc_v1_notify'broadcast(Cmd),  ohc_v1_decided'broadcast: ohc_v1_decided'broadcast(),  ohc_v1_retry'send: ohc_v1_retry'send(Cmd),  length: ||as||,  null: null(as),  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>,  cons: [car / cdr],  add: n + m,  natural_number: $n,  poss-maj: poss-maj(eq;L;x),  bag-append: as + bs,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  ohc_v1_roundout2 ohc_v1_roundout2
ohc\_v1\_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  cmds,z  =  z 
                              in  if  (||cmds||  =\msubz{}  flrs  +  1)
                                    then  let  vlist  =  ohc\_v1\_prune\_off\_units(Cmd)  [cmdU  /  cmds]  in
                                                      let  k,x  =  poss-maj(cmdeq;vlist;cmd) 
                                                      in  if  (k  =\msubz{}  flrs  +  1)
                                                                then  (ohc\_v1\_notify'broadcast(Cmd)  learners  <n,  x>)
                                                                          +  (ohc\_v1\_decided'broadcast()  locs  n)
                                                            if  null(vlist)  then  \{ohc\_v1\_retry'send(Cmd)  loc  <<n,  i  +  1>,  cmd>\}
                                                            else  \{ohc\_v1\_retry'send(Cmd)  loc  <<n,  i  +  1>,  x>\}
                                                            fi 
                                    else  \{\}
                                    fi 


Date html generated: 2012_02_20-PM-05_22_29
Last ObjectModification: 2012_02_13-PM-12_56_06

Home Index