Nuprl Definition : ler_ring_strong_setup_sub+

ler_ring_strong_setup_sub+(es;nodes;epoch;L) ==
  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
         ((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)))
          (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_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],  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_strong_setup_sub+
ler\_ring\_strong\_setup\_sub+(es;nodes;epoch;L)  ==
    \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
                  ((\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)))))
      \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_06_18
Last ObjectModification: 2012_02_02-PM-02_40_02

Home Index