Nuprl Lemma : ler-ilf

([es:EO']. [e:E]. [v:  Id].
   {v  ler_Nbr()(e)
    v  zb,za.
            let epoch,succ = za 
            in z.let epoch',succ' = z 
                  in if epoch' <z epoch
                     then {<epoch, succ>}
                     else {<epoch', succ'>}
                     fi @Loc|Loc, ler_Config(), Prior(self)?l.{<ler_dumEpoch(), l>}|(e)})
 ([client:Id]. [nodes:bag(Id)]. [uid:Id  ]. [es:EO']. [e:E]. [i:Id]. [m:Message].
     {<i, m>  ler_leader_ring_main(client;nodes;uid)(e)
      loc(e)  nodes
          ((a:
              a1:Id
               (<a, a1>  Prior(ler_Nbr())(e)
                (b1:
                   (<a, b1>  Base([propose];  )(e)
                    (((b1 = (uid loc(e)))  (i = client)  (m = make-Msg([leader];  Id;<a, loc(e)>)))
                      (((b1 = (uid loc(e))))
                        (i = a1)
                        (m = make-Msg([propose];  ;<a, imax(b1;uid loc(e))>))))))))
            (a:
                (a  Base([choose];)(e)
                 (m = make-Msg([propose];  ;<a, uid loc(e)>))
                 <a, i>  Prior(ler_Nbr())(e))))})


Proof not projected



Definitions occuring in Statement :  ler_leader_ring_main: ler_leader_ring_main(client;nodes;uid),  ler_Nbr: ler_Nbr(),  ler_dumEpoch: ler_dumEpoch(),  ler_Config: ler_Config(),  concat-lifting-loc-2: f@Loc,  make-Msg: make-Msg(hdr;typ;val),  base-headers-msg-val: Base(hdr;typ),  Message: Message,  rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|,  primed-class: Prior(X),  classrel: v  X(e),  event-ordering+: EO+(Info),  es-loc: loc(e),  es-E: E,  Id: Id,  imax: imax(a;b),  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  sq_or: a  b,  uall: [x:A]. B[x],  guard: {T},  exists: x:A. B[x],  iff: P  Q,  not: A,  or: P  Q,  and: P  Q,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  cons: [car / cdr],  nil: [],  int: ,  token: "$token",  equal: s = t,  bag-member: x  bs,  single-bag: {x},  bag: bag(T)
Lemmas :  SpLeaderRing-ilf
(\mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[v:\mBbbZ{}  \mtimes{}  Id].
      \{v  \mmember{}  ler\_Nbr()(e)
      \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  \mlambda{}zb,za.
                        let  epoch,succ  =  za 
                        in  \mlambda{}z.let  epoch',succ'  =  z 
                                    in  if  epoch'  <z  epoch
                                          then  \{<epoch,  succ>\}
                                          else  \{<epoch',  succ'>\}
                                          fi  @Loc|Loc,  ler\_Config(),  Prior(self)?\mlambda{}l.\{<ler\_dumEpoch(),  l>\}|(e)\})
\mwedge{}  (\mforall{}[client:Id].  \mforall{}[nodes:bag(Id)].  \mforall{}[uid:Id  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[m:Message].
          \{<i,  m>  \mmember{}  ler\_leader\_ring\_main(client;nodes;uid)(e)
          \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  nodes
                  \mwedge{}  ((\mexists{}a:\mBbbZ{}
                            \mexists{}a1:Id
                              (<a,  a1>  \mmember{}  Prior(ler\_Nbr())(e)
                              \mwedge{}  (\mexists{}b1:\mBbbZ{}
                                      (<a,  b1>  \mmember{}  Base([propose];\mBbbZ{}  \mtimes{}  \mBbbZ{})(e)
                                      \mwedge{}  (((b1  =  (uid  loc(e)))
                                          \mwedge{}  (i  =  client)
                                          \mwedge{}  (m  =  make-Msg([leader];\mBbbZ{}  \mtimes{}  Id;<a,  loc(e)>)))
                                          \mvee{}  ((\mneg{}(b1  =  (uid  loc(e))))
                                              \mwedge{}  (i  =  a1)
                                              \mwedge{}  (m  =  make-Msg([propose];\mBbbZ{}  \mtimes{}  \mBbbZ{};<a,  imax(b1;uid  loc(e))>))))))))
                      \mdownarrow{}\mvee{}  (\mexists{}a:\mBbbZ{}
                                (a  \mmember{}  Base([choose];\mBbbZ{})(e)
                                \mwedge{}  (m  =  make-Msg([propose];\mBbbZ{}  \mtimes{}  \mBbbZ{};<a,  uid  loc(e)>))
                                \mwedge{}  <a,  i>  \mmember{}  Prior(ler\_Nbr())(e))))\})


Date html generated: 2012_02_20-PM-06_03_06
Last ObjectModification: 2012_02_02-PM-02_38_47

Home Index