Nuprl Lemma : ler2_leader_from_propose

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


Proof not projected



Definitions occuring in Statement :  ler2_leader'base: ler2_leader'base(),  Message: Message,  classrel: v  X(e),  event-ordering+: EO+(Info),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  Id: Id,  all: x:A. B[x],  exists: x:A. B[x],  squash: T,  implies: 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 :  Id: Id,  true: True,  cand: A c B,  bfalse: ff,  btrue: tt,  lt_int: i <z j,  bnot: b,  le_int: i z j,  ifthenelse: if b then t else f fi ,  prop: ,  false: False,  not: A,  le: A  B,  lelt: i  j < k,  ycomb: Y,  length: ||as||,  int_seg: {i..j},  select: l[i],  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,  and: P  Q,  exists: x:A. B[x],  squash: T,  implies: P  Q,  all: x:A. B[x],  guard: {T},  sq_type: SQType(T),  iff: P  Q,  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_leader'base: ler2_leader'base(),  ler2_message-constraint: Error :ler2_message-constraint,  subtype: S  T,  msg-header: msg-header(m),  ler2_PrNbr: Error :ler2_PrNbr,  ler2_propose'base: Error :ler2_propose'base
Lemmas :  atom2_subtype_base,  subtype_base_sq,  event-ordering+_wf,  bag_wf,  Error :ler2_message-constraint_wf,  ler2_leader'base_wf,  Error :ler2_propose'base_wf,  bag-member_wf,  Error :ler2_PrNbr_wf,  ler2_leader-ilf,  es-loc_wf,  Error :ler2_main_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,  lelt_wf,  name_wf,  select_member,  valueall-type_wf,  Id-valueall-type,  int-valueall-type,  product-valueall-type,  Id_wf,  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:\mBbbZ{}.  \mforall{}l:Id.
                (<epoch,  l>  \mmember{}  ler2\_leader'base()(e)
                {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                            (l  \mdownarrow{}\mmember{}  nodes
                            \mwedge{}  (e'  <  e)
                            \mwedge{}  (loc(e')  =  l)
                            \mwedge{}  <epoch,  uid  l  epoch>  \mmember{}  ler2\_propose'base()(e')
                            \mwedge{}  (loc(e)  =  client)
                            \mwedge{}  (\mexists{}l':Id.  <epoch,  l'>  \mmember{}  ler2\_PrNbr\{SpLeaderRing2.esh:o\}(e')))))))


Date html generated: 2012_02_20-PM-06_16_15
Last ObjectModification: 2012_02_02-PM-02_43_45

Home Index