Nuprl Lemma : ler_list_Propose
es:EO'. nodes:bag(Id). client:Id. uid:Id 
.
(((ler_leader_ring_message-constraint{i:l}(client;nodes;uid) es)
ler_non_dummy_configuration(es;nodes)
ler_non_dummy_request(es))
(e:E. epoch,k:. e':{e':E| (e' <loc e)} . l:Id.
(<epoch, k> 
ler_Propose()(e)
<epoch, l> ler_Config()(e')
(
e1,e2:E
L:E 
E List
(epoch ler_Choose()(e1)
<epoch, loc(fst(L[0]))> ler_Config()(e2)
((e2 <loc e1) loc(e1) nodes)
(<e, e'> = last(L))
(e1 < fst(L[0]))
<epoch, uid loc(e1)> ler_Propose()(fst(L[0]))
(snd(L[0]) <loc fst(L[0]))
(i:{1..||L||
}
((fst(L[i - 1]) < fst(L[i]))
<epoch, loc(fst(L[i]))> ler_Config()(snd(L[i - 1]))
((snd(L[i]) <loc fst(L[i])) loc(snd(L[i - 1])) nodes)
<epoch, imax-list([uid loc(e1) / firstn(i;map(
p.(uid loc(fst(p)));L))])>
ler_Propose()(fst(L[i])))))))))
Proof not projected
Definitions occuring in Statement :
ler_non_dummy_request: ler_non_dummy_request(es),
ler_non_dummy_configuration: ler_non_dummy_configuration(es;nodes),
ler_leader_ring_message-constraint: ler_leader_ring_message-constraint{i:l}(client;nodes;uid),
ler_Propose: ler_Propose(),
ler_Choose: ler_Choose(),
ler_Config: ler_Config(),
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,
select: l[i],
firstn: firstn(n;as),
map: map(f;as),
length: ||as||,
int_seg: {i..j},
pi1: fst(t),
pi2: snd(t),
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,
lambda: x.A[x],
function: x:A B[x],
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
subtract: n - m,
natural_number: $n,
int: ,
equal: s = t,
listp: A List,
last: last(L),
bag-member: x bs,
bag: bag(T),
imax-list: imax-list(L)
Definitions :
all: x:A. B[x],
implies: P Q,
and: P Q,
ler_non_dummy_configuration: ler_non_dummy_configuration(es;nodes),
ler_non_dummy_request: ler_non_dummy_request(es),
squash: T,
gt: i > j,
member: t T,
nat: 
,
ge: i 
j ,
le: A 
B,
not: 
A,
false: False,
prop: 
,
true: True,
exists: x:A. B[x],
listp: A List,
length: ||as||,
subtype: S 
T,
top: Top,
ycomb: Y,
so_lambda: 
x.t[x],
assert: 
b,
ifthenelse: if b then t else f fi ,
btrue: tt,
iff: P 
Q,
rev_implies: P Q,
select: l[i],
last: last(L),
lt_int: i <z j,
bfalse: ff,
le_int: i z j,
bnot: 
b,
pi1: fst(t),
pi2: snd(t),
int_seg: {i..j},
lelt: i j < k,
or: P 
Q,
imax-list: imax-list(L),
firstn: firstn(n;as),
map: map(f;as),
append: as @ bs,
hd: hd(l),
tl: tl(l),
list_accum: list_accum(x,a.f[x; a];y;l),
name: Name,
label: ...$L... t,
strongwellfounded: SWellFounded(R[x; y]),
uall: [x:A]. B[x],
uimplies: b supposing a,
es-p-local-pred: es-p-local-pred(es;P),
uiff: uiff(P;Q),
ler_dumEpoch: ler_dumEpoch(),
rev_uimplies: rev_uimplies(P;Q),
so_apply: x[s],
sq_type: SQType(T),
guard: {T},
sq_stable: SqStable(P),
bool: 
,
unit: Unit,
es-locl: (e <loc e'),
ler_Propose: ler_Propose(),
single-valued-classrel: single-valued-classrel(es;X;T),
it: 
Lemmas :
es-causl-swellfnd,
nat_properties,
ge_wf,
nat_wf,
le_wf,
es-causl_wf,
ler_Propose_from_Propose_or_Choose,
classrel_wf,
ler_Config_wf,
ler_Propose_wf,
es-locl_wf,
ler_leader_ring_message-constraint_wf,
es-E_wf,
event-ordering+_inc,
Message_wf,
Id_wf,
gt_wf,
bag-member_wf,
ler_Choose_wf,
bag_wf,
event-ordering+_wf,
prior-classrel-p-local-pred,
ler_Nbr_wf,
es-loc_wf,
ler_Nbr_from_Config,
es-locl_transitivity1,
append_wf,
length-append,
top_wf,
assert_of_lt_int,
length_wf,
non_neg_length,
length_wf_nat,
assert_wf,
lt_int_wf,
listp_properties,
pos_length2,
int_seg_properties,
firstn_wf,
map_wf,
pi1_wf_top,
length_firstn,
map_length,
select_wf,
last_wf,
Error :pi2_wf,
int_seg_wf,
imax-list_wf,
listp_wf,
select-append,
subtype_base_sq,
bool_subtype_base,
iff_imp_equal_bool,
btrue_wf,
iff_functionality_wrt_iff,
true_wf,
iff_weakening_uiff,
int_subtype_base,
bfalse_wf,
false_wf,
bool_wf,
le_int_wf,
bnot_wf,
sq_stable_from_decidable,
decidable__es-locl,
uiff_transitivity,
eqtt_to_assert,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
es-le-loc,
map_append_sq,
firstn_append,
length-map,
list_decomp,
hd_wf,
tl_wf,
select0,
single-valued-classrel-base,
imax_wf,
squash_wf,
firstn_decomp,
select-map,
length_nil,
length_cons,
length_append,
imax-imax-list-left,
cons_wf_listp,
event_ordering_wf
\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\_non\_dummy\_configuration(es;nodes)
\mwedge{} ler\_non\_dummy\_request(es))
{}\mRightarrow{} (\mforall{}e:E. \mforall{}epoch,k:\mBbbZ{}. \mforall{}e':\{e':E| (e' <loc e)\} . \mforall{}l:Id.
(<epoch, k> \mmember{} ler\_Propose()(e)
{}\mRightarrow{} <epoch, l> \mmember{} ler\_Config()(e')
{}\mRightarrow{} (\mdownarrow{}\mexists{}e1,e2:E
\mexists{}L:E \mtimes{} E List\msupplus{}
(epoch \mmember{} ler\_Choose()(e1)
\mwedge{} <epoch, loc(fst(L[0]))> \mmember{} ler\_Config()(e2)
\mwedge{} ((e2 <loc e1) \mwedge{} loc(e1) \mdownarrow{}\mmember{} nodes)
\mwedge{} (<e, e'> = last(L))
\mwedge{} (e1 < fst(L[0]))
\mwedge{} <epoch, uid loc(e1)> \mmember{} ler\_Propose()(fst(L[0]))
\mwedge{} (snd(L[0]) <loc fst(L[0]))
\mwedge{} (\mforall{}i:\{1..||L||\msupminus{}\}
((fst(L[i - 1]) < fst(L[i]))
\mwedge{} <epoch, loc(fst(L[i]))> \mmember{} ler\_Config()(snd(L[i - 1]))
\mwedge{} ((snd(L[i]) <loc fst(L[i])) \mwedge{} loc(snd(L[i - 1])) \mdownarrow{}\mmember{} nodes)
\mwedge{} <epoch, imax-list([uid loc(e1) / firstn(i;map(\mlambda{}p.(uid loc(fst(p)));L))])> \mmember{}
ler\_Propose()(fst(L[i])))))))))
Date html generated:
2012_02_20-PM-06_06_41
Last ObjectModification:
2012_02_02-PM-02_40_07
Home
Index