Nuprl Lemma : ler_Propose_from_Propose_or_Choose

es:EO'. nodes:bag(Id). client:Id. uid:Id  .
  ((ler_leader_ring_message-constraint{i:l}(client;nodes;uid) es)
   (e:E. epoch,i:.
        (<epoch, i>  ler_Propose()(e)
         (e':E
              (loc(e')  nodes
               (e' < e)
               <epoch, loc(e)>  Prior(ler_Nbr())(e')
               <loc(e), info(e)>  ler_leader_ring_main(client;nodes;uid)(e')
               ((j:. (<epoch, j>  ler_Propose()(e')  ((j = (uid loc(e'))))  (i = imax(j;uid loc(e')))))
                 (epoch  ler_Choose()(e')  (i = (uid loc(e'))))))))))


Proof not projected



Definitions occuring in Statement :  ler_leader_ring_message-constraint: ler_leader_ring_message-constraint{i:l}(client;nodes;uid),  ler_leader_ring_main: ler_leader_ring_main(client;nodes;uid),  ler_Nbr: ler_Nbr(),  ler_Propose: ler_Propose(),  ler_Choose: ler_Choose(),  Message: Message,  primed-class: Prior(X),  classrel: v  X(e),  es-info: info(e),  event-ordering+: EO+(Info),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  Id: Id,  imax: imax(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,  apply: f a,  function: x:A  B[x],  pair: <a, b>,  product: x:A  B[x],  int: ,  equal: s = t,  bag-member: x  bs,  bag: bag(T)
Definitions :  guard: {T},  iff: P  Q,  rev_implies: P  Q,  true: True,  cand: A c B,  prop: ,  so_lambda: x.t[x],  member: t  T,  name: Name,  es-header: es-header(es;e),  ler_leader_ring_headers_no_inputs: ler_leader_ring_headers_no_inputs(),  ler_Choose: ler_Choose(),  or: P  Q,  and: P  Q,  exists: x:A. B[x],  squash: T,  ler_Propose: ler_Propose(),  implies: P  Q,  all: x:A. B[x],  so_apply: x[s],  uall: [x:A]. B[x],  uiff: uiff(P;Q),  uimplies: b supposing a,  message-constraint: message-constraint{i:l}(es;X;hdrs),  ler_leader_ring_message-constraint: ler_leader_ring_message-constraint{i:l}(client;nodes;uid),  subtype: S  T,  msg-header: msg-header(m)
Lemmas :  and_assoc,  exists_functionality_wrt_iff,  or_functionality_wrt_iff,  base-headers-msg-val_wf,  event-ordering+_wf,  bag_wf,  ler_leader_ring_message-constraint_wf,  ler_Propose_wf,  ler_Choose_wf,  imax_wf,  not_wf,  ler_Nbr_wf,  primed-class_wf,  bag-member_wf,  ler_Propose_ilf,  es-loc_wf,  ler_leader_ring_main_wf,  Id_wf,  classrel_wf,  es-causl_wf,  Message_wf,  event-ordering+_inc,  es-E_wf,  squash_wf,  ler_leader_ring_headers_no_inputs_wf,  msg-header_wf,  l_member_wf,  name_wf,  cons_member,  valueall-type_wf,  int-valueall-type,  product-valueall-type,  base-noloc-classrel-make-Msg
\mforall{}es:EO'.  \mforall{}nodes:bag(Id).  \mforall{}client:Id.  \mforall{}uid:Id  {}\mrightarrow{}  \mBbbZ{}.
    ((ler\_leader\_ring\_message-constraint\{i:l\}(client;nodes;uid)  es)
    {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}epoch,i:\mBbbZ{}.
                (<epoch,  i>  \mmember{}  ler\_Propose()(e)
                {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                            (loc(e')  \mdownarrow{}\mmember{}  nodes
                            \mwedge{}  (e'  <  e)
                            \mwedge{}  <epoch,  loc(e)>  \mmember{}  Prior(ler\_Nbr())(e')
                            \mwedge{}  <loc(e),  info(e)>  \mmember{}  ler\_leader\_ring\_main(client;nodes;uid)(e')
                            \mwedge{}  ((\mexists{}j:\mBbbZ{}
                                      (<epoch,  j>  \mmember{}  ler\_Propose()(e')
                                      \mwedge{}  (\mneg{}(j  =  (uid  loc(e'))))
                                      \mwedge{}  (i  =  imax(j;uid  loc(e')))))
                                \mvee{}  (epoch  \mmember{}  ler\_Choose()(e')  \mwedge{}  (i  =  (uid  loc(e'))))))))))


Date html generated: 2012_02_20-PM-06_03_47
Last ObjectModification: 2012_02_02-PM-02_38_58

Home Index