Nuprl Lemma : ler_leader_max_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))
(epoch:. L:Id List. succ:{i:Id| (i 
L)} {i:Id| (i L)} .
((sub-bag(Id;L;nodes)
no_repeats(Id;L)
ma-ring(L;succ)
(i:{i:Id| (i L)}
e:E. (<epoch, succ i> ler_Config()(e) (loc(e) = i) (e':E. (epoch ler_Choose()(e') (e < e')))))
(j:Id. e:E. (<epoch, j> ler_Config()(e) (loc(e) L))))
(e:E. l:Id. (<epoch, l> ler_Leader()(e) (l':Id. ((l' L) ((uid l) 
(uid l') ))))))))
Proof not projected
Definitions occuring in Statement :
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),
ler_Choose: ler_Choose(),
ler_Config: ler_Config(),
ma-ring: ma-ring(R;s),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
inject: Inj(A;B;f),
ge: i j ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
pair: <a, b>,
product: x:A 
B[x],
list: type List,
int: ,
equal: s = t,
no_repeats: no_repeats(T;l),
l_member: (x l),
sub-bag: sub-bag(T;as;bs),
bag: bag(T)
Definitions :
all: x:A. B[x],
implies: P Q,
and: P Q,
exists: x:A. B[x],
ge: i j ,
squash: 
T,
member: t T,
true: True,
prop: 
,
le: A 
B,
not: 
A,
false: False,
Id: Id,
gt: i > j,
ler_non_dummy_configuration: ler_non_dummy_configuration(es;nodes),
cand: A c B,
subtype: S 
T,
top: Top,
so_apply: x[s1;s2],
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
int_seg: {i..j
},
or: P 
Q,
lelt: i j < k,
nat: 
,
name: Name,
length: ||as||,
ycomb: Y,
iff: P 
Q,
rev_implies: P Q,
pi2: snd(t),
pi1: fst(t),
l_member: (x l),
ler_non_dummy_request: ler_non_dummy_request(es),
sq_stable: SqStable(P),
uall: [x:A]. B[x],
uimplies: b supposing a,
uiff: uiff(P;Q),
ler_dumEpoch: ler_dumEpoch(),
es-p-local-pred: es-p-local-pred(es;P),
ler_consistent_configuration: ler_consistent_configuration(es),
es-locl: (e <loc e'),
sq_type: SQType(T),
guard: {T},
ler_non_dummy_configuration+: ler_non_dummy_configuration+(es;nodes),
listp: A List
,
so_apply: x[s],
no_repeats: no_repeats(T;l),
ler_Propose: ler_Propose(),
last: last(L),
single-valued-classrel: single-valued-classrel(es;X;T),
inject: Inj(A;B;f),
l_all: (xL.P[x])
Lemmas :
ler_Leader_from_Propose,
sq_stable_from_decidable,
le_wf,
decidable__le,
ler_Propose_from_Choose,
l_member_wf,
Id_wf,
classrel_wf,
Message_wf,
ler_Leader_wf,
es-E_wf,
event-ordering+_inc,
sub-bag_wf,
bag_qinc,
no_repeats_wf,
ma-ring_wf,
ler_Config_wf,
es-loc_wf,
ler_Choose_wf,
es-causl_wf,
ler_leader_ring_message-constraint_wf,
ler_consistent_configuration_wf,
ler_non_dummy_configuration+_wf,
ler_non_dummy_request_wf,
inject_wf,
bag_wf,
event-ordering+_wf,
prior-classrel-p-local-pred,
ler_Nbr_wf,
ler_Nbr_from_Config,
es-le-loc,
subtype_base_sq,
atom2_subtype_base,
ler_list_Propose,
es-locl_transitivity1,
es-locl_wf,
listp_properties,
pi1_wf_top,
select_wf,
top_wf,
length_wf,
decidable__l_member,
decidable__equal_Id,
ma-ring-property2,
int_seg_wf,
nat_properties,
gt_wf,
nat_wf,
natrec_wf,
length-map,
length_wf_nat,
select-map,
int_subtype_base,
select0,
Error :pi2_wf,
single-valued-classrel-base,
base-headers-msg-val_wf,
squash_wf,
true_wf,
Error :eclass_wf,
imax-list_wf,
firstn_wf,
map_wf,
non_neg_length,
length_firstn,
map_length,
length_cons,
imax-list-eq-implies,
cons_member,
member_firstn,
bag-member-l_eqset,
bag-member-list,
ler_Propose_wf,
imax-list-lb,
select_cons_tl,
select_firstn,
add_functionality_wrt_eq
\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))
{}\mRightarrow{} (\mforall{}epoch:\mBbbZ{}. \mforall{}L:Id List. \mforall{}succ:\{i:Id| (i \mmember{} L)\} {}\mrightarrow{} \{i:Id| (i \mmember{} L)\} .
((sub-bag(Id;L;nodes)
\mwedge{} no\_repeats(Id;L)
\mwedge{} ma-ring(L;succ)
\mwedge{} (\mforall{}i:\{i:Id| (i \mmember{} L)\}
\mexists{}e:E
(<epoch, succ i> \mmember{} ler\_Config()(e)
\mwedge{} (loc(e) = i)
\mwedge{} (\mforall{}e':E. (epoch \mmember{} ler\_Choose()(e') {}\mRightarrow{} (e < e')))))
\mwedge{} (\mforall{}j:Id. \mforall{}e:E. (<epoch, j> \mmember{} ler\_Config()(e) {}\mRightarrow{} (loc(e) \mmember{} L))))
{}\mRightarrow{} (\mforall{}e:E. \mforall{}l:Id.
(<epoch, l> \mmember{} ler\_Leader()(e) {}\mRightarrow{} (\mforall{}l':Id. ((l' \mmember{} L) {}\mRightarrow{} ((uid l) \mgeq{} (uid l') ))))))))
Date html generated:
2012_02_20-PM-06_07_11
Last ObjectModification:
2012_02_02-PM-02_40_13
Home
Index