Nuprl Lemma : RSC-retry-property2
[Cmd:ValueAllType]. [eq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [f:
]. [es:EO'].
((RSC_stdma{i:l}(Cmd;clients;eq;f;locs) es)
(e:E. c:Cmd. n,r:.
(<<n, r + 1>, c> 
RSC_Retry(Cmd)(e)
(
x:Id
cs:Cmd List
L:Id List
((no_repeats(Id;L) 
(||L|| = ((2 * f) + 1)) (||cs|| = ||L||))
(i:
||L||
((e':{e':E| (e' < e)}
<x, make-Msg(``sc vote``; 
Cmd Id;<<<n, r>, cs[i]>, L[i]>)>
RSC_main(Cmd;clients;eq;f;locs)(e'))
L[i] locs))
(c = (snd(poss-maj(eq;cs;hd(cs))))))))))
Proof not projected
Definitions occuring in Statement :
RSC_stdma: RSC_stdma{i:l}(Cmd;clients;cmdeq;flrs;locs),
RSC_main: RSC_main(Cmd;clients;cmdeq;flrs;locs),
RSC_Retry: RSC_Retry(Cmd),
make-Msg: make-Msg(hdr;typ;val),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-causl: (e < e'),
es-E: E,
Id: Id,
select: l[i],
hd: hd(l),
length: ||as||,
int_seg: {i..j
},
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,
set: {x:A| B[x]} ,
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),
poss-maj: poss-maj(eq;L;x),
deq: EqDecider(T),
bag-member: x bs,
bag: bag(T),
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
vatype: ValueAllType,
implies: P Q,
all: x:A. B[x],
squash: T,
exists: x:A. B[x],
and: P Q,
length: ||as||,
int_seg: {i..j},
select: l[i],
member: t T,
true: True,
not: 
A,
RSC_headers_no_inputs: Error :RSC_headers_no_inputs,
es-header: es-header(es;e),
name: Name,
so_lambda: 
x.t[x],
ycomb: Y,
lelt: i 
j < k,
le: A B,
false: False,
prop: 
,
ifthenelse: if b then t else f fi ,
le_int: i z j,
bnot: 
b,
lt_int: i <z j,
btrue: tt,
bfalse: ff,
cand: A c B,
label: ...$L... t,
RSC_VotesInRound: Error :RSC_VotesInRound,
Accum-class: Accum-class(f;init;X),
RSC_collect: Error :RSC_collect,
RSC_Vote: Error :RSC_Vote,
top: Top,
uiff: uiff(P;Q),
band: p q,
guard: {T},
hd: hd(l),
nat: ,
Id: Id,
bag-member: x bs,
RSC_stdma: Error :RSC_stdma,
RSC_Retry: Error :RSC_Retry,
sq_stable: SqStable(P),
message-constraint: message-constraint{i:l}(es;X;hdrs),
std-ma: StandardMessageAutomaton(X;hdrs),
uimplies: b supposing a,
so_apply: x[s],
or: P 
Q,
sq_or: a b,
iff: P 
Q,
sq_type: SQType(T),
rev_uimplies: rev_uimplies(P;Q),
bool: 
,
unit: Unit,
msg-header: msg-header(m),
subtype: S 
T,
it: 
,
!hyp_hide: x
Lemmas :
sq_stable__valueall-type,
valueall-type_wf,
base-noloc-classrel-make-Msg,
product-valueall-type,
int-valueall-type,
select_member,
name_wf,
le_wf,
l_member_wf,
msg-header_wf,
Error :RSC_headers_no_inputs_wf,
squash_wf,
es-E_wf,
event-ordering+_inc,
Message_wf,
es-causl_wf,
classrel_wf,
Id_wf,
Error :RSC_main_wf,
es-loc_wf,
RSC_retry,
Error :RSC_Retry_wf,
Error :RSC_stdma_wf,
event-ordering+_wf,
bag_wf,
deq_wf,
subtype_base_sq,
int_subtype_base,
member-eo-forward-E,
sq_stable_from_decidable,
es-le_wf,
decidable__es-le,
eo-forward-E-subtype,
primed-class-opt_wf,
single-bag_wf,
Error :RSC_VotesInRound_wf,
eo-forward_wf,
not_wf,
product-wf,
length_wf,
Error :pi2_wf,
nat_wf,
poss-maj_wf,
base-headers-msg-val_wf,
rec-combined-class-opt-1-classrel,
Error :RSC_collect_wf,
simple-comb-2-classrel,
Error :RSC_Vote_wf,
rec-combined-class-opt-1_wf,
lifting-2_wf,
eq_int_wf,
bool_wf,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert_of_eq_int,
deq-member_wf,
id-deq_wf,
iff_transitivity,
iff_weakening_uiff,
assert-deq-member,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_iff,
not_functionality_wrt_uiff,
eo-forward-base-classrel,
pair_wf,
RSC_VotesInRound-inv,
int_seg_wf,
no_repeats_wf,
make-Msg_wf,
Id-valueall-type,
select_wf,
bag-member_wf,
hd_wf,
pos_length,
nat_properties,
atom2_subtype_base,
es-le-loc,
eo-forward-loc,
eo-forward-le,
decidable__es-causl,
es-causle_weakening_locl,
es-causl_transitivity2,
es-causle_weakening,
RSC_vote,
length_wf_nat,
top_wf,
member_wf
\mforall{}[Cmd:ValueAllType]. \mforall{}[eq:EqDecider(Cmd)]. \mforall{}[locs,clients:bag(Id)]. \mforall{}[f:\mBbbZ{}]. \mforall{}[es:EO'].
((RSC\_stdma\{i:l\}(Cmd;clients;eq;f;locs) es)
{}\mRightarrow{} (\mforall{}e:E. \mforall{}c:Cmd. \mforall{}n,r:\mBbbZ{}.
(<<n, r + 1>, c> \mmember{} RSC\_Retry(Cmd)(e)
{}\mRightarrow{} (\mdownarrow{}\mexists{}x:Id
\mexists{}cs:Cmd List
\mexists{}L:Id List
((no\_repeats(Id;L) \mwedge{} (||L|| = ((2 * f) + 1)) \mwedge{} (||cs|| = ||L||))
\mwedge{} (\mforall{}i:\mBbbN{}||L||
((\mdownarrow{}\mexists{}e':\{e':E| (e' < e)\}
<x, make-Msg(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, r>, cs[i]>, L[i]>)> \mmember{}
RSC\_main(Cmd;clients;eq;f;locs)(e'))
\mwedge{} L[i] \mdownarrow{}\mmember{} locs))
\mwedge{} (c = (snd(poss-maj(eq;cs;hd(cs))))))))))
Date html generated:
2012_02_20-PM-04_04_21
Last ObjectModification:
2012_02_02-PM-01_59_51
Home
Index