Nuprl Lemma : ler_propose_all_nodes2_sub
es:EO'. nodes:bag(Id). client:Id. uid:Id 
. L:Id List. succ:{i:Id| (i 
L)} {i:Id| (i L)} . epoch:.
(((ler_leader_ring_messages-delivered{i:l}(client;nodes;uid) es)
ler_consistent_configuration(es)
ler_non_dummy_configuration(es;nodes)
Inj(Id;;uid)
sub-bag(Id;L;nodes)
no_repeats(Id;L)
ma-ring(L;succ)
(i:{i:Id| (i L)}
e':E
((e1,e2:E. u:.
((e' <loc e1)
(e1 <loc e2)
(<epoch, u> ler_Propose()(e2) 
epoch ler_Choose()(e2))
(
w: 
Id. w ler_Config()(e1))))
<epoch, succ i> ler_Config()(e')
(e'':{e'':E| (e'' <loc e')} . epoch':. j:Id. (<epoch', j> ler_Config()(e'') (epoch' 
epoch)))
(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
(epoch ler_Choose()(e)
(loc(e) L)
(i:
||L||. (L[i] = (succ^i loc(e))))
(i:{1..||L||
}
(e':E. (<epoch, imax-list((
n.(uid L[n]))[i])> ler_Propose()(e') (e < e') (loc(e') = L[i])))))))
Proof not projected
Definitions occuring in Statement :
ler_consistent_configuration: ler_consistent_configuration(es),
ler_non_dummy_configuration: ler_non_dummy_configuration(es;nodes),
ler_leader_ring_messages-delivered: ler_leader_ring_messages-delivered{i:l}(client;nodes;uid),
ler_Propose: ler_Propose(),
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-locl: (e <loc e'),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
listify: listify(f;m;n),
select: l[i],
length: ||as||,
inject: Inj(A;B;f),
int_seg: {i..j},
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
squash: T,
implies: P Q,
or: P Q,
and: P Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
pair: <a, b>,
product: x:A B[x],
list: type List,
natural_number: $n,
int: ,
equal: s = t,
no_repeats: no_repeats(T;l),
l_member: (x l),
fun_exp: f^n,
sub-bag: sub-bag(T;as;bs),
bag: bag(T),
imax-list: imax-list(L)
Definitions :
nat: ,
so_lambda: 
x.t[x],
prop: 
,
true: True,
false: False,
member: t T,
le: A B,
squash: T,
not: A,
implies: P Q,
all: x:A. B[x],
ler_send_propose: ler_send_propose(),
and: P Q,
sq_or: a b,
or: P Q,
cand: A c B,
es-p-local-pred: es-p-local-pred(es;P),
es-locl: (e <loc e'),
exists: x:A. B[x],
gt: i > j,
top: Top,
let: let,
guard: {T},
ler_Nbr: ler_Nbr(),
name: Name,
tl: tl(l),
hd: hd(l),
list_accum: list_accum(x,a.f[x; a];y;l),
bfalse: ff,
btrue: tt,
lt_int: i <z j,
bnot: 
b,
le_int: i z j,
ifthenelse: if b then t else f fi ,
ycomb: Y,
listify: listify(f;m;n),
imax-list: imax-list(L),
lelt: i j < k,
int_seg: {i..j},
Id: Id,
msg-has-type: msg-has-type(m;T),
mData: mData,
pMsg: pMsg(P.M[P]),
msg-body: msg-body(msg),
msg-type: msg-type(msg),
assert: 
b,
es-header: es-header(es;e),
make-Msg: make-Msg(hdr;typ;val),
pi2: snd(t),
pi1: fst(t),
ler_Propose: ler_Propose(),
Message: Message,
ge: i 
j ,
listp: A List
,
iff: P 
Q,
rev_implies: P Q,
uimplies: b supposing a,
so_apply: x[s],
messages-delivered: messages-delivered{i:l}(es;X),
uall: [x:A]. B[x],
ler_leader_ring_messages-delivered: ler_leader_ring_messages-delivered{i:l}(client;nodes;uid),
sub-bag: sub-bag(T;as;bs),
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
ler_non_dummy_configuration: ler_non_dummy_configuration(es;nodes),
ler_Choose: ler_Choose(),
eq_int: (i =
j),
primrec: primrec(n;b;c),
sq_type: SQType(T),
fun_exp: f^n,
compose: f o g,
inject: Inj(A;B;f),
no_repeats: no_repeats(T;l),
subtype: S 
T
Lemmas :
event-ordering+_wf,
bag_wf,
es-causl_wf,
ler_Config_wf,
squash_wf,
not_wf,
ler_Propose_wf,
or_wf,
es-locl_wf,
exists_wf,
ma-ring_wf,
no_repeats_wf,
bag_qinc,
sub-bag_wf,
inject_wf,
ler_non_dummy_configuration_wf,
ler_consistent_configuration_wf,
ler_leader_ring_messages-delivered_wf,
and_wf,
es-E_wf,
ler_Choose_wf,
classrel_wf,
le_wf,
fun_exp_wf,
select_wf,
equal_wf,
all_wf,
length_wf,
int_seg_wf,
ler_send_propose_wf,
Id_wf,
l_member_wf,
Message_wf,
event-ordering+_inc,
es-loc_wf,
lelt_wf,
int_seg_properties,
ler_Propose_ilf,
bag-member_wf,
decidable__equal_Id,
bag-member-list,
bag-member-append,
es-p-local-pred_wf,
ler_Nbr_wf,
prior-classrel-p-local-pred,
ler_Config_to_Nbr2,
ler_dumEpoch_wf,
primed-class-opt_wf,
single-bag_wf,
lt_int_wf,
ifthenelse_wf,
simple-loc-comb-2-concat-classrel,
rec-combined-loc-class-opt-1-classrel,
imax_wf,
base-headers-msg-val_wf,
atom2_subtype_base,
int_subtype_base,
subtype_base_sq,
msg-body_wf2,
type-valueall-type,
eq_term_wf,
assert_wf,
name_wf,
base-noloc-classrel,
length_wf_nat,
listify_length,
non_neg_length,
listify_wf,
imax-list_wf,
select_member,
es-causle_weakening,
es-causl_transitivity2,
fun_exp_add1-sq,
nat_wf,
ge_wf,
member-listify,
imax-list-eq-implies,
true_wf,
length_append,
append_wf,
length_cons,
length_wf_nil,
length_nil,
less_than_wf,
listify-append-last,
assert_of_lt_int,
imax-imax-list-left
\mforall{}es:EO'. \mforall{}nodes:bag(Id). \mforall{}client:Id. \mforall{}uid:Id {}\mrightarrow{} \mBbbZ{}. \mforall{}L:Id List. \mforall{}succ:\{i:Id| (i \mmember{} L)\} {}\mrightarrow{} \{i:Id|
(i \mmember{} L)\} .
\mforall{}epoch:\mBbbZ{}.
(((ler\_leader\_ring\_messages-delivered\{i:l\}(client;nodes;uid) es)
\mwedge{} ler\_consistent\_configuration(es)
\mwedge{} ler\_non\_dummy\_configuration(es;nodes)
\mwedge{} Inj(Id;\mBbbZ{};uid)
\mwedge{} 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
((\mforall{}e1,e2:E. \mforall{}u:\mBbbZ{}.
((e' <loc e1)
{}\mRightarrow{} (e1 <loc e2)
{}\mRightarrow{} (<epoch, u> \mmember{} ler\_Propose()(e2) \mvee{} epoch \mmember{} ler\_Choose()(e2))
{}\mRightarrow{} (\mneg{}\mdownarrow{}\mexists{}w:\mBbbZ{} \mtimes{} Id. w \mmember{} ler\_Config()(e1))))
\mwedge{} <epoch, succ i> \mmember{} ler\_Config()(e')
\mwedge{} (\mforall{}e'':\{e'':E| (e'' <loc e')\} . \mforall{}epoch':\mBbbZ{}. \mforall{}j:Id.
(<epoch', j> \mmember{} ler\_Config()(e'') {}\mRightarrow{} (epoch' \mleq{} epoch)))
\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
(epoch \mmember{} ler\_Choose()(e)
{}\mRightarrow{} (loc(e) \mmember{} L)
{}\mRightarrow{} (\mforall{}i:\mBbbN{}||L||. (L[i] = (succ\^{}i loc(e))))
{}\mRightarrow{} (\mforall{}i:\{1..||L||\msupminus{}\}
(\mdownarrow{}\mexists{}e':E
(<epoch, imax-list((\mlambda{}n.(uid L[n]))[\mBbbN{}i])> \mmember{} ler\_Propose()(e')
\mwedge{} (e < e')
\mwedge{} (loc(e') = L[i])))))))
Date html generated:
2012_02_20-PM-06_09_06
Last ObjectModification:
2012_02_02-PM-02_40_39
Home
Index