Nuprl Definition : rsc5

Nuprl Definition : rsc5_roundout

rsc5_roundout(Cmd;clients;cmdeq;coeff;flrs;locs) ==

loc,zc.
   let zd,sndr = zc
   in let ze,c = zd
      in let n,i = ze
         in

z.let pmaj,vlocs = z
               in if eqof(IntDeq) ||vlocs|| (coeff * flrs)
                  then let k,x = rsc5_possmajstep(Cmd;cmdeq) pmaj c
                       in if eqof(IntDeq) k ((coeff * flrs) + 1)
                          then (rsc5_decided'broadcast() locs n) + (rsc5_notify'broadcast(Cmd) clients <n, x>)
                          else {rsc5_retry'send(Cmd) loc <<n, i + 1>, x>}
                          fi
                  else {}
                  fi

Definitions occuring in Statement : rsc5_possmajstep: rsc5_possmajstep(Cmd;cmdeq), rsc5_decided'broadcast: rsc5_decided'broadcast(), rsc5_retry'send: rsc5_retry'send(Cmd), length: ||as||, ifthenelse: if b then t else f fi , apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, multiply: n * m, add: n + m, natural_number: $n, int-deq: IntDeq, eqof: eqof(d), bag-append: as + bs, single-bag: {x}, empty-bag: {}
FDL editor aliases : rsc5_roundout

rsc5\_roundout(Cmd;clients;cmdeq;coeff;flrs;locs) == \mlambda{}loc,zc. let zd,sndr = zc in let ze,c = zd in let n,i = ze in \mlambda{}z.let pmaj,vlocs = z in if eqof(IntDeq) ||vlocs|| (coeff * flrs) then let k,x = rsc5\_possmajstep(Cmd;cmdeq) pmaj c in if eqof(IntDeq) k ((coeff * flrs) + 1) then (rsc5\_decided'broadcast() locs n) + (rsc5\_notify'broadcast(Cmd) clients <n, x>) else \{rsc5\_retry'send(Cmd) loc <<n, i + 1>, x>\} fi else \{\} fi Date html generated: 2012_02_20-PM-05_05_18 Last ObjectModification: 2012_02_02-PM-02_17_59 Home Index