Nuprl Lemma : ler_Leader_from_Propose

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


Proof not projected



Definitions occuring in Statement :  ler_Leader: ler_Leader(),  ler_leader_ring_message-constraint: ler_leader_ring_message-constraint{i:l}(client;nodes;uid),  ler_Nbr: ler_Nbr(),  ler_Propose: ler_Propose(),  Message: Message,  primed-class: Prior(X),  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),  ler_leader_ring_headers_no_inputs: ler_leader_ring_headers_no_inputs(),  ler_Propose: ler_Propose(),  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),  ler_Leader: ler_Leader(),  ler_leader_ring_message-constraint: ler_leader_ring_message-constraint{i:l}(client;nodes;uid),  subtype: S  T,  msg-header: msg-header(m)
Lemmas :  atom2_subtype_base,  subtype_base_sq,  event-ordering+_wf,  bag_wf,  ler_leader_ring_message-constraint_wf,  ler_Leader_wf,  base-headers-msg-val_wf,  bag-member_wf,  ler_Nbr_wf,  primed-class_wf,  ler_Leader_ilf,  es-loc_wf,  ler_leader_ring_main_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,  le_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{}.
    ((ler\_leader\_ring\_message-constraint\{i:l\}(client;nodes;uid)  es)
    {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}epoch:\mBbbZ{}.  \mforall{}l:Id.
                (<epoch,  l>  \mmember{}  ler\_Leader()(e)
                {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                            (l  \mdownarrow{}\mmember{}  nodes
                            \mwedge{}  (e'  <  e)
                            \mwedge{}  (loc(e')  =  l)
                            \mwedge{}  <epoch,  uid  l>  \mmember{}  ler\_Propose()(e')
                            \mwedge{}  (loc(e)  =  client)
                            \mwedge{}  (\mexists{}l':Id.  <epoch,  l'>  \mmember{}  Prior(ler\_Nbr())(e')))))))


Date html generated: 2012_02_20-PM-06_03_38
Last ObjectModification: 2012_02_02-PM-02_38_55

Home Index