Nuprl Definition : ler_ring_strong_setup

ler_ring_strong_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
               ((e1,e2:E. u:.
                   ((e' <loc e1)
                    (e1 <loc e2)
                    (<epoch, u>  ler_Propose()(e2)  epoch  ler_Choose()(e2))
                    (w:  Id. w  ler_Config()(e1))))
                <epoch, succ i>  ler_Config()(e')
                (e'':{e'':E| (e'' <loc e')} . epoch':. j:Id.  (<epoch', j>  ler_Config()(e'')  (epoch'  epoch))\000C)
                (loc(e') = i)
                (e:E. (epoch  ler_Choose()(e)  (e' < e))))))))


Definitions occuring in Statement :  ler_Propose: ler_Propose(),  ler_Choose: ler_Choose(),  ler_Config: ler_Config(),  ma-ring: ma-ring(R;s),  classrel: v  X(e),  es-locl: (e <loc e'),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  Id: Id,  le: A  B,  all: x:A. B[x],  exists: x:A. B[x],  not: A,  squash: T,  implies: P  Q,  or: 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_strong_setup
ler\_ring\_strong\_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
                              ((\mforall{}e1,e2:E.  \mforall{}u:\mBbbZ{}.
                                      ((e'  <loc  e1)
                                      {}\mRightarrow{}  (e1  <loc  e2)
                                      {}\mRightarrow{}  (<epoch,  u>  \mmember{}  ler\_Propose()(e2)  \mvee{}  epoch  \mmember{}  ler\_Choose()(e2))
                                      {}\mRightarrow{}  (\mneg{}\mdownarrow{}\mexists{}w:\mBbbZ{}  \mtimes{}  Id.  w  \mmember{}  ler\_Config()(e1))))
                              \mwedge{}  <epoch,  succ  i>  \mmember{}  ler\_Config()(e')
                              \mwedge{}  (\mforall{}e'':\{e'':E|  (e''  <loc  e')\}  .  \mforall{}epoch':\mBbbZ{}.  \mforall{}j:Id.
                                        (<epoch',  j>  \mmember{}  ler\_Config()(e'')  {}\mRightarrow{}  (epoch'  \mleq{}  epoch)))
                              \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_51
Last ObjectModification: 2012_02_02-PM-02_39_50

Home Index