Nuprl Definition : ler_ring_setup

ler_ring_setup(es;nodes) ==
  L:Id List
   ((L = nodes)
    no_repeats(Id;L)
    (epoch:
        succ:{i:Id| (i  L)}   {i:Id| (i  L)} 
         (ma-ring(L;succ)
          (i:{i:Id| (i  L)} 
              e':E
               (<epoch, succ i>  ler_Config()(e')  (loc(e') = i)  (e:E. (epoch  ler_Choose()(e)  (e' < e))))))))


Definitions occuring in Statement :  ler_Choose: ler_Choose(),  ler_Config: ler_Config(),  ma-ring: ma-ring(R;s),  classrel: v  X(e),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  Id: Id,  all: x:A. B[x],  exists: x:A. B[x],  implies: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  pair: <a, b>,  product: x:A  B[x],  list: type List,  int: ,  equal: s = t,  no_repeats: no_repeats(T;l),  l_member: (x  l),  bag: bag(T)
FDL editor aliases :  ler_ring_setup
ler\_ring\_setup(es;nodes)  ==
    \mexists{}L:Id  List
      ((L  =  nodes)
      \mwedge{}  no\_repeats(Id;L)
      \mwedge{}  (\mforall{}epoch:\mBbbZ{}
                \mexists{}succ:\{i:Id|  (i  \mmember{}  L)\}    {}\mrightarrow{}  \{i:Id|  (i  \mmember{}  L)\} 
                  (ma-ring(L;succ)
                  \mwedge{}  (\mforall{}i:\{i:Id|  (i  \mmember{}  L)\} 
                            \mexists{}e':E
                              (<epoch,  succ  i>  \mmember{}  ler\_Config()(e')
                              \mwedge{}  (loc(e')  =  i)
                              \mwedge{}  (\mforall{}e:E.  (epoch  \mmember{}  ler\_Choose()(e)  {}\mRightarrow{}  (e'  <  e))))))))


Date html generated: 2012_02_20-PM-06_05_11
Last ObjectModification: 2012_02_02-PM-02_39_33

Home Index