Nuprl Lemma : rsc4-retry-property
[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff,flrs:
]. [es:EO'].
((StandardAssumptions(rsc4_Main) es)
(e:E. c:Cmd. n,r:
.
(<<n, r + 1>, c> 
rsc4_retry'base(Cmd)(e)
(
x:Id
cs:Cmd List
L:Id List
((no_repeats(Id;L) 
(||L|| = ((coeff * flrs) + 1)) (||cs|| = ||L||))
(i:||L||
((e':E. <x, make-Msg(``rsc4 vote``; 
Cmd Id;<<<n, r>, cs[i]>, L[i]>)> rsc4_Main(e'))
L[i] locs))
(c = (snd(poss-maj(cmdeq;cs;hd(cs))))))))))
Proof
Definitions occuring in Statement :
rsc4_stdma: StandardAssumptions(rsc4_Main),
rsc4_main: rsc4_Main,
rsc4_retry'base: rsc4_retry'base(Cmd),
make-Msg: make-Msg(hdr;typ;val),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
select: l[i],
hd: hd(l),
length: ||as||,
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
pi2: snd(t),
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
apply: f a,
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
multiply: n * m,
add: n + m,
natural_number: $n,
int: ,
token: "$token",
equal: s = t,
no_repeats: no_repeats(T;l),
listp: A List,
poss-maj: poss-maj(eq;L;x),
deq: EqDecider(T),
bag-member: x bs,
bag: bag(T),
vatype: ValueAllType
Definitions :
guard: {T},
ge: i 
j ,
rsc4_QuorumState: rsc4_QuorumState(Cmd),
cand: A c B,
bfalse: ff,
btrue: tt,
lt_int: i <z j,
bnot: 
b,
le_int: i 
z j,
ifthenelse: if b then t else f fi ,
prop: 
,
false: False,
not: A,
le: A B,
lelt: i j < k,
ycomb: Y,
so_lambda: 
x.t[x],
name: Name,
es-header: es-header(es;e),
rsc4_headers_no_inputs: rsc4_headers_no_inputs(),
true: True,
member: t T,
hd: hd(l),
select: l[i],
int_seg: {i..j},
length: ||as||,
and: P Q,
exists: x:A. B[x],
squash: T,
all: x:A. B[x],
implies: P Q,
vatype: ValueAllType,
uall: [x:A]. B[x],
uiff: uiff(P;Q),
rsc4_vote'base: rsc4_vote'base(Cmd),
so_lambda: x y.t[x; y],
iff: P 
Q,
rev_implies: P Q,
Id: Id,
bag-member: x bs,
rsc4_newvote: rsc4_newvote(Cmd),
sq_or: a 
b,
or: P Q,
so_apply: x[s],
uimplies: b supposing a,
std-ma: StandardMessageAutomaton(X;hdrs),
message-constraint: message-constraint{i:l}(es;X;hdrs),
sq_stable: SqStable(P),
rsc4_retry'base: rsc4_retry'base(Cmd),
rsc4_stdma: StandardAssumptions(rsc4_Main),
nat: ,
so_apply: x[s1;s2],
sq_type: SQType(T),
decidable: Dec(P),
subtype: S 
T,
msg-header: msg-header(m)
Lemmas :
assert-deq-member,
not_functionality_wrt_iff,
assert_of_bnot,
assert_of_eq_int,
and_functionality_wrt_uiff,
uiff_transitivity,
and_functionality_wrt_iff,
assert_of_band,
iff_weakening_uiff,
iff_transitivity,
listp_wf,
hd_wf,
poss-maj_wf,
pi2_wf,
bag-member_wf,
select_wf,
Id-valueall-type,
make-Msg_wf,
all_wf,
length_wf,
no_repeats_wf,
int_seg_wf,
no_repeats_cons,
cons_wf_listp,
mul_bounds_1a,
not_wf,
and_wf,
id-deq_wf,
deq-member_wf,
bnot_wf,
eq_int_wf,
band_wf,
assert_wf,
deq_wf,
bag_wf,
nat_wf,
rsc4_stdma_wf,
rsc4_retry'base_wf,
event-ordering+_wf,
subtype_rel_set,
eo-forward-E-subtype,
equal_wf,
decidable__es-le,
es-le_wf,
sq_stable_from_decidable,
member-eo-forward-E,
eo-forward_wf,
rsc4_quorum_invariant,
rsc4-retry,
es-loc_wf,
rsc4_main_wf,
Id_wf,
classrel_wf,
es-causl_wf,
Message_wf,
event-ordering+_inc,
es-E_wf,
exists_wf,
squash_wf,
rsc4_headers_no_inputs_wf,
msg-header_wf,
l_member_wf,
lelt_wf,
name_wf,
select_member,
int-valueall-type,
product-valueall-type,
base-noloc-classrel-make-Msg,
valueall-type_wf,
sq_stable__valueall-type,
base-headers-msg-val_wf,
eo-forward-base-classrel,
eo-forward-le,
select_cons_tl,
eclass_wf,
true_wf,
int_subtype_base,
subtype_base_sq,
decidable__equal_int,
product_subtype_base,
atom2_subtype_base,
es-le-loc,
rsc4-vote
\mforall{}[Cmd:ValueAllType]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[locs,clients:bag(Id)]. \mforall{}[coeff,flrs:\mBbbN{}]. \mforall{}[es:EO'].
((StandardAssumptions(rsc4\_Main) es)
{}\mRightarrow{} (\mforall{}e:E. \mforall{}c:Cmd. \mforall{}n,r:\mBbbZ{}.
(<<n, r + 1>, c> \mmember{} rsc4\_retry'base(Cmd)(e)
{}\mRightarrow{} (\mdownarrow{}\mexists{}x:Id
\mexists{}cs:Cmd List\msupplus{}
\mexists{}L:Id List
((no\_repeats(Id;L) \mwedge{} (||L|| = ((coeff * flrs) + 1)) \mwedge{} (||cs|| = ||L||))
\mwedge{} (\mforall{}i:\mBbbN{}||L||
((\mdownarrow{}\mexists{}e':E
<x, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, r>, cs[i]>, L[i]>)> \mmember{}
rsc4\_Main(e'))
\mwedge{} L[i] \mdownarrow{}\mmember{} locs))
\mwedge{} (c = (snd(poss-maj(cmdeq;cs;hd(cs))))))))))
Date html generated:
2012_02_20-PM-05_00_55
Last ObjectModification:
2012_02_02-PM-02_16_44
Home
Index