Nuprl Definition : ler_ring_sub_setup

ler_ring_sub_setup(es;nodes) ==
  epoch:
    L:Id List
     succ:{i:Id| (i  L)}   {i:Id| (i  L)} 
      (sub-bag(Id;L;nodes)
       no_repeats(Id;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')))))
       (j:Id. e:E.  (<epoch, j>  ler_Config()(e)  (loc(e)  L))))


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),  sub-bag: sub-bag(T;as;bs)
FDL editor aliases :  ler_ring_sub_setup
ler\_ring\_sub\_setup(es;nodes)  ==
    \mforall{}epoch:\mBbbZ{}
        \mexists{}L:Id  List
          \mexists{}succ:\{i:Id|  (i  \mmember{}  L)\}    {}\mrightarrow{}  \{i:Id|  (i  \mmember{}  L)\} 
            (sub-bag(Id;L;nodes)
            \mwedge{}  no\_repeats(Id;L)
            \mwedge{}  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')))))
            \mwedge{}  (\mforall{}j:Id.  \mforall{}e:E.    (<epoch,  j>  \mmember{}  ler\_Config()(e)  {}\mRightarrow{}  (loc(e)  \mmember{}  L))))


Date html generated: 2012_02_20-PM-06_05_24
Last ObjectModification: 2012_02_02-PM-02_39_39

Home Index