Nuprl Lemma : ler_liveness_prop
es:EO'. nodes:bag(Id). client:Id. uid:Id 
.
(((ler_leader_ring_messages-delivered{i:l}(client;nodes;uid) es)
ler_non_decreasing_configuration(es)
ler_consistent_configuration(es)
ler_non_dummy_configuration+(es;nodes)
Inj(Id;;uid)
ler_ring_setup_non_reconf(es;nodes))
(e:E. epoch:. i:{i:{i:Id| i 
nodes} | j:{i:Id| i nodes} . ((uid i) 
(uid j) )} .
(epoch ler_Choose()(e) loc(e) nodes (
e':E. <epoch, i> ler_Leader()(e')))))
Proof not projected
Definitions occuring in Statement :
ler_ring_setup_non_reconf: ler_ring_setup_non_reconf(es;nodes),
ler_non_decreasing_configuration: ler_non_decreasing_configuration(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_messages-delivered: ler_leader_ring_messages-delivered{i:l}(client;nodes;uid),
ler_Choose: ler_Choose(),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
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],
squash: T,
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],
int: ,
bag-member: x bs,
bag: bag(T)
Definitions :
all: x:A. B[x],
implies: P Q,
and: P Q,
ge: i j ,
squash: T,
not: 
A,
member: t T,
int_seg: {i..j
},
subtype: S 
T,
name: Name,
true: True,
prop: 
,
so_lambda: 
x.t[x],
cand: A c B,
le: A 
B,
lelt: i j < k,
false: False,
top: Top,
suptype: suptype(S; T),
bag-member: x bs,
exists: x:A. B[x],
l_all: (xL.P[x]),
Id: Id,
fun_exp: f^n,
nat: 
,
primrec: primrec(n;b;c),
ycomb: Y,
ifthenelse: if b then t else f fi ,
eq_int: (i =
j),
btrue: tt,
iff: P 
Q,
so_lambda: x y.t[x; y],
rev_implies: P Q,
ler_ring_setup_non_reconf: ler_ring_setup_non_reconf(es;nodes),
ler_Choose: ler_Choose(),
l_member: (x l),
listp: A List
,
l_eqset: l_eqset(T;L1;L2),
uall: [x:A]. B[x],
uimplies: b supposing a,
uiff: uiff(P;Q),
sq_stable: SqStable(P),
so_apply: x[s],
sq_type: SQType(T),
guard: {T},
so_apply: x[s1;s2]
Lemmas :
ma-ring-property2,
es-loc_wf,
event-ordering+_inc,
Message_wf,
base-noloc-classrel,
sq_stable_from_decidable,
l_member_wf,
decidable__l_member,
decidable__equal_Id,
bag-member-list-member,
list-eq-in-bag-if-l_eqset-and-no_repeats,
id-deq_wf,
ler_propose_all_max+,
subtype_rel_function,
Id_wf,
subtype_rel_sets,
subtype_rel_self,
le_wf,
length_wf,
select_wf,
imax-list_wf,
map_wf,
non_neg_length,
map_length,
length_wf_nat,
top_wf,
int_seg_wf,
bag-member_wf,
classrel_wf,
ler_Choose_wf,
ge_wf,
es-E_wf,
ler_leader_ring_messages-delivered_wf,
ler_non_decreasing_configuration_wf,
ler_consistent_configuration_wf,
ler_non_dummy_configuration+_wf,
inject_wf,
ler_ring_setup_non_reconf_wf,
bag_wf,
event-ordering+_wf,
imax-list-unique,
member_map,
select_member,
subtype_base_sq,
int_subtype_base,
bag_qinc,
int_seg_properties,
select0,
atom2_subtype_base,
fun_exp_add1-sq,
squash_wf,
true_wf,
Error :eclass_wf,
ler_Leader_wf
\mforall{}es:EO'. \mforall{}nodes:bag(Id). \mforall{}client:Id. \mforall{}uid:Id {}\mrightarrow{} \mBbbZ{}.
(((ler\_leader\_ring\_messages-delivered\{i:l\}(client;nodes;uid) es)
\mwedge{} ler\_non\_decreasing\_configuration(es)
\mwedge{} ler\_consistent\_configuration(es)
\mwedge{} ler\_non\_dummy\_configuration+(es;nodes)
\mwedge{} Inj(Id;\mBbbZ{};uid)
\mwedge{} ler\_ring\_setup\_non\_reconf(es;nodes))
{}\mRightarrow{} (\mforall{}e:E. \mforall{}epoch:\mBbbZ{}. \mforall{}i:\{i:\{i:Id| i \mdownarrow{}\mmember{} nodes\} | \mforall{}j:\{i:Id| i \mdownarrow{}\mmember{} nodes\} . ((uid i) \mgeq{} (uid j) )\} .
(epoch \mmember{} ler\_Choose()(e) {}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} nodes {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. <epoch, i> \mmember{} ler\_Leader()(e')))))
Date html generated:
2012_02_20-PM-06_10_58
Last ObjectModification:
2012_02_02-PM-02_40_59
Home
Index