Nuprl Lemma : ler_unique_Leader_sub

es:EO'. nodes:bag(Id). client:Id. uid:Id  .
  (((ler_leader_ring_message-constraint{i:l}(client;nodes;uid) es)
   ler_consistent_configuration(es)
   ler_non_dummy_configuration+(es;nodes)
   ler_non_dummy_request(es)
   Inj(Id;;uid)
   ler_ring_sub_setup(es;nodes))
   (e1,e2:E. l:Id. epoch:. l1,l2:Id.
        ((<epoch, l1>  ler_Leader()(e1)  <epoch, l2>  ler_Leader()(e2))  (l1 = l2))))


Proof not projected



Definitions occuring in Statement :  ler_ring_sub_setup: ler_ring_sub_setup(es;nodes),  ler_non_dummy_request: ler_non_dummy_request(es),  ler_consistent_configuration: ler_consistent_configuration(es),  ler_non_dummy_configuration+: ler_non_dummy_configuration+(es;nodes),  ler_Leader: ler_Leader(),  ler_leader_ring_message-constraint: ler_leader_ring_message-constraint{i:l}(client;nodes;uid),  Message: Message,  classrel: v  X(e),  event-ordering+: EO+(Info),  es-E: E,  Id: Id,  inject: Inj(A;B;f),  all: x:A. B[x],  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: bag(T)
Definitions :  all: x:A. B[x],  implies: P  Q,  and: P  Q,  member: t  T,  cand: A c B,  prop: ,  squash: T,  true: True,  Id: Id,  ler_ring_sub_setup: ler_ring_sub_setup(es;nodes),  exists: x:A. B[x],  uall: [x:A]. B[x],  ler_non_dummy_request: ler_non_dummy_request(es),  sq_stable: SqStable(P),  uimplies: b supposing a,  es-p-local-pred: es-p-local-pred(es;P),  uiff: uiff(P;Q),  gt: i > j,  or: P  Q,  ler_dumEpoch: ler_dumEpoch(),  es-locl: (e <loc e'),  sq_type: SQType(T),  guard: {T},  ge: i  j ,  le: A  B,  not: A,  false: False,  inject: Inj(A;B;f),  subtype: S  T
Lemmas :  ler_leader_max_sub,  classrel_wf,  Message_wf,  Id_wf,  ler_Leader_wf,  es-E_wf,  event-ordering+_inc,  ler_leader_ring_message-constraint_wf,  ler_consistent_configuration_wf,  ler_non_dummy_configuration+_wf,  ler_non_dummy_request_wf,  inject_wf,  ler_ring_sub_setup_wf,  bag_wf,  event-ordering+_wf,  ler_Leader_from_Propose,  sq_stable_from_decidable,  l_member_wf,  decidable__l_member,  decidable__equal_Id,  prior-classrel-p-local-pred,  ler_Nbr_wf,  ler_Propose_from_Choose,  ler_Nbr_from_Config,  es-loc_wf,  es-le-loc,  subtype_base_sq,  atom2_subtype_base
\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)
    \mwedge{}  ler\_consistent\_configuration(es)
    \mwedge{}  ler\_non\_dummy\_configuration+(es;nodes)
    \mwedge{}  ler\_non\_dummy\_request(es)
    \mwedge{}  Inj(Id;\mBbbZ{};uid)
    \mwedge{}  ler\_ring\_sub\_setup(es;nodes))
    {}\mRightarrow{}  (\mforall{}e1,e2:E.  \mforall{}l:Id.  \mforall{}epoch:\mBbbZ{}.  \mforall{}l1,l2:Id.
                ((<epoch,  l1>  \mmember{}  ler\_Leader()(e1)  \mwedge{}  <epoch,  l2>  \mmember{}  ler\_Leader()(e2))  {}\mRightarrow{}  (l1  =  l2))))


Date html generated: 2012_02_20-PM-06_07_29
Last ObjectModification: 2012_02_02-PM-02_40_19

Home Index