Nuprl Lemma : ler2_propose_from_propose_or_choose

es:EO'. nodes:bag(Id). client:Id. uid:Id    .
  ((ler2_message-constraint{i:l}(client;nodes;uid) es)
   (e:E. epoch,i:.
        (<epoch, i>  ler2_propose'base()(e)
         (e':E
              (loc(e')  nodes
               (e' < e)
               <epoch, loc(e)>  ler2_PrNbr{SpLeaderRing2.esh:o}(e')
               <loc(e), info(e)>  ler2_main(client;nodes;uid)(e')
               ((j:
                   (<epoch, j>  ler2_propose'base()(e')
                    ((j = (uid loc(e') epoch)))
                    (i = imax(j;uid loc(e') epoch))))
                 (epoch  ler2_choose'base()(e')  (i = (uid loc(e') epoch)))))))))


Proof not projected



Definitions occuring in Statement :  Message: Message,  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 :  rev_implies: P  Q,  guard: {T},  iff: 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),  ler2_headers_no_inputs: Error :ler2_headers_no_inputs,  or: P  Q,  and: P  Q,  exists: x:A. B[x],  squash: T,  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),  ler2_propose'base: Error :ler2_propose'base,  ler2_message-constraint: Error :ler2_message-constraint,  subtype: S  T,  msg-header: msg-header(m),  ler2_choose'base: Error :ler2_choose'base,  ler2_PrNbr: Error :ler2_PrNbr
Lemmas :  and_assoc,  exists_functionality_wrt_iff,  or_functionality_wrt_iff,  or_wf,  Error :ler2_PrNbr_wf,  bag-member_wf,  Error :ler2_choose'base_wf,  imax_wf,  equal_wf,  not_wf,  and_wf,  event-ordering+_wf,  bag_wf,  Error :ler2_message-constraint_wf,  Error :ler2_propose'base_wf,  ler2_propose-ilf,  es-loc_wf,  Error :ler2_main_wf,  Id_wf,  classrel_wf,  es-causl_wf,  Message_wf,  event-ordering+_inc,  es-E_wf,  exists_wf,  squash_wf,  Error :ler2_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{}  {}\mrightarrow{}  \mBbbZ{}.
    ((ler2\_message-constraint\{i:l\}(client;nodes;uid)  es)
    {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}epoch,i:\mBbbZ{}.
                (<epoch,  i>  \mmember{}  ler2\_propose'base()(e)
                {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                            (loc(e')  \mdownarrow{}\mmember{}  nodes
                            \mwedge{}  (e'  <  e)
                            \mwedge{}  <epoch,  loc(e)>  \mmember{}  ler2\_PrNbr\{SpLeaderRing2.esh:o\}(e')
                            \mwedge{}  <loc(e),  info(e)>  \mmember{}  ler2\_main(client;nodes;uid)(e')
                            \mwedge{}  ((\mexists{}j:\mBbbZ{}
                                      (<epoch,  j>  \mmember{}  ler2\_propose'base()(e')
                                      \mwedge{}  (\mneg{}(j  =  (uid  loc(e')  epoch)))
                                      \mwedge{}  (i  =  imax(j;uid  loc(e')  epoch))))
                                \mvee{}  (epoch  \mmember{}  ler2\_choose'base()(e')  \mwedge{}  (i  =  (uid  loc(e')  epoch)))))))))


Date html generated: 2012_02_20-PM-06_16_25
Last ObjectModification: 2012_02_02-PM-02_43_48

Home Index