Nuprl Lemma : ler_unique_Leader
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_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_setup: ler_ring_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,
prop: 
,
squash: 
T,
true: True,
uall: [x:A]. B[x],
exists: 
x:A. B[x],
sq_stable: SqStable(P),
ge: i 
j ,
le: A 
B,
not: 
A,
false: False,
inject: Inj(A;B;f),
subtype: S 
T,
guard: {T}
Lemmas :
ler_leader_max,
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_setup_wf,
bag_wf,
event-ordering+_wf,
ler_Leader_from_Propose,
sq_stable__bag-member
\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\_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_19
Last ObjectModification:
2012_02_02-PM-02_40_16
Home
Index