Nuprl Lemma : rsc4-retry
[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:
]. [locs:bag(Id)]. [es:EO']. [e:E].
[i:Id]. [k,k1:]. [v:Cmd].
(<i, make-Msg(``rsc4 retry``; 
Cmd;<<k, k1>, v>)> 
rsc4_Main(e)
loc(e) 
locs
(i = loc(e))
(
e':{e':E| e' 
loc e }
a:
(((a2:
b2: List
(<a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e')
((a2 < a) 
(a b2))))
(b:Cmd
(<a, b> Base([propose]; Cmd)(e')
(b1:. b3:Id. <<<a, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e')))))
(((b1:
((k1 = (b1 + 1))
(b2:Cmd
b3:Id
(<<<k, b1>, b2>, b3> Base(``rsc4 vote``; Cmd Id)(e)
(a2:Cmd List
((((||a2|| = (coeff * flrs))
(
((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))))
(v = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
(b4:Id List
(<a2, b4> Memory-class(rsc4_add_to_quorum(Cmd) <a, 0>;rsc4_init()
<[], []>;rsc4_vote'base(Cmd))(
e)
(
(rsc4_newvote(Cmd) <a, 0> <<<k, b1>, b2>, b3> <a2, b4>))))))))))
((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)))
((e1:{e1:E| e1 loc e }
b:
((((b4:
(b4 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e1)
(b4 < b)))
(b1:Cmd
(<<a, b>, b1> Base(``rsc4 retry``; Cmd)(e1)
(b5:Id. <<<a, b>, b1>, b5> Base(``rsc4 vote``; Cmd Id)(e1)))))
(b1:
((k1 = (b1 + 1))
(b2:Cmd
b3:Id
(<<<k, b1>, b2>, b3> Base(``rsc4 vote``; Cmd Id)(e)
(a2:Cmd List
((((||a2|| = (coeff * flrs))
(((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))))
(v = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
(b4:Id List
(<a2, b4> Memory-class(rsc4_add_to_quorum(Cmd)
<a, b>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e)
((rsc4_newvote(Cmd) <a, b> <<<k, b1>, b2>, b3> <a2, b4>)))))))))))
((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e1 and e))))
(no rsc4_Notify(Cmd;clients) a between e' and e))))))
Proof
Definitions occuring in Statement :
rsc4_main: rsc4_Main,
rsc4_update_replica: rsc4_update_replica(Cmd),
rsc4_Proposal: rsc4_Proposal(Cmd),
rsc4_Notify: rsc4_Notify(Cmd;clients),
rsc4_update_round: rsc4_update_round(Cmd),
rsc4_RoundInfo: rsc4_RoundInfo(Cmd),
rsc4_Quorum: rsc4_Quorum(Cmd;cmdeq;coeff;flrs),
rsc4_add_to_quorum: rsc4_add_to_quorum(Cmd),
rsc4_newvote: rsc4_newvote(Cmd),
rsc4_init: rsc4_init(),
rsc4_vote'base: rsc4_vote'base(Cmd),
Memory-class: Memory-class(f;init;X),
make-Msg: make-Msg(hdr;typ;val),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
no-classrel-in-interval: (no X between start and e),
classrel: v X(e),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-loc: loc(e),
es-E: E,
Id: Id,
length: ||as||,
assert: b,
sq_or: a b,
uall: [x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
exists: x:A. B[x],
iff: P Q,
not: A,
squash: T,
or: P Q,
and: P Q,
less_than: a < b,
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,
l_member: (x l),
poss-maj: poss-maj(eq;L;x),
deq: EqDecider(T),
bag-member: x bs,
bag: bag(T),
vatype: ValueAllType
Definitions :
bfalse: ff,
btrue: tt,
eq_atom: x =a y,
atom-deq: AtomDeq,
band: p 
q,
list-deq: list-deq(eq),
name-deq: NameDeq,
ifthenelse: if b then t else f fi ,
name_eq: name_eq(x;y),
assert: b,
false: False,
uiff: uiff(P;Q),
guard: {T},
sq_or: a b,
top: Top,
name: Name,
subtype: S 
T,
prop: 
,
rev_implies: P Q,
true: True,
so_lambda: 
x.t[x],
implies: P Q,
cand: A c B,
all: x:A. B[x],
member: t T,
or: P Q,
exists: x:A. B[x],
squash: T,
bag-member: x bs,
and: P Q,
classrel: v X(e),
iff: P Q,
vatype: ValueAllType,
uall: [x:A]. B[x],
pi2: snd(t),
pi1: fst(t),
rev_uimplies: rev_uimplies(P;Q),
uimplies: b supposing a,
nat: 
,
sq_stable: SqStable(P),
so_apply: x[s]
Lemmas :
Id-valueall-type,
assert-name_eq,
msg-body_wf,
msg-type_wf,
msg-header_wf,
eo-forward-base-classrel,
make-Msg-equal,
eo-forward-loc,
subtype_rel_set,
squash_false,
and_false_r,
rsc4_decided'base_wf,
rsc4_decision_wf,
concat-lifting-loc-1_wf,
simple-loc-comb-1_wf,
and_false_l,
or_false_l,
sq_or_simp,
trivial-eq,
exists-elim,
squash_squash,
and_true_l,
true_wf,
or_false_r,
false_wf,
squash_equal,
squash_and,
deq_wf,
rsc4_Notify_wf,
rsc4_RoundInfo_wf,
rsc4_update_round_wf,
eo-forward-E-subtype,
event-ordering+_wf,
rsc4_Quorum_wf,
no-classrel-in-interval_wf,
rsc4_newvote_wf,
assert_wf,
decidable__es-le,
sq_stable_from_decidable,
member-eo-forward-E,
eo-forward_wf,
rsc4_vote'base_wf,
rsc4_add_to_quorum_wf,
pi2_wf,
nat_wf,
poss-maj_wf,
pi1_wf_top,
equal_wf,
not_wf,
length_wf,
base-headers-msg-val_wf,
sq_or_wf,
l_member_wf,
less_than_wf,
or_wf,
rsc4_Proposal_wf,
bag_wf,
rsc4_init_wf,
rsc4_update_replica_wf,
Memory-class_wf,
es-le_wf,
es-E_wf,
exists_wf,
squash_wf,
event-ordering+_inc,
es-loc_wf,
bag-member_wf,
rsc4_main_wf,
Id_wf,
Message_wf,
classrel_wf,
make-Msg_wf,
valueall-type_wf,
sq_stable__valueall-type,
int-valueall-type,
product-valueall-type,
rsc4-ilf
\mforall{}[Cmd:ValueAllType]. \mforall{}[clients:bag(Id)]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[coeff,flrs:\mBbbZ{}]. \mforall{}[locs:bag(Id)].
\mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[k,k1:\mBbbZ{}]. \mforall{}[v:Cmd].
(<i, make-Msg(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd;<<k, k1>, v>)> \mmember{} rsc4\_Main(e)
\mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} locs
\mwedge{} (i = loc(e))
\mwedge{} (\mdownarrow{}\mexists{}e':\{e':E| e' \mleq{}loc e \}
\mexists{}a:\mBbbZ{}
(((\mdownarrow{}\mexists{}a2:\mBbbZ{}
\mexists{}b2:\mBbbZ{} List
(<a2, b2> \mmember{} Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init()
ɘ, []>rsc4\_Proposal(Cmd))(e')
\mwedge{} ((a2 < a) \mvee{} (a \mmember{} b2))))
\mwedge{} (\mexists{}b:Cmd
(<a, b> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e')
\mdownarrow{}\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, b>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e')))))
\mwedge{} (\mdownarrow{}((\mdownarrow{}\mexists{}b1:\mBbbZ{}
((k1 = (b1 + 1))
\mwedge{} (\mexists{}b2:Cmd
\mexists{}b3:Id
(<<<k, b1>, b2>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)
\mwedge{} (\mexists{}a2:Cmd List
((((||a2|| = (coeff * flrs))
\mwedge{} (\mneg{}((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))))
\mwedge{} (v = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
\mwedge{} (\mexists{}b4:Id List
(<a2, b4> \mmember{} Memory-class(rsc4\_add\_to\_quorum(Cmd)
<a, 0>rsc4\_init()
<[], []>rsc4\_vote'base(Cmd))(e)
\mwedge{} (\muparrow{}(rsc4\_newvote(Cmd) <a, 0> <<<k, b1>, b2>, b3>
<a2, b4>))))))))))
\mwedge{} (\mdownarrow{}(no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)))
\mvee{} ((\mdownarrow{}\mexists{}e1:\{e1:E| e1 \mleq{}loc e \}
\mexists{}b:\mBbbZ{}
((((\mdownarrow{}\mexists{}b4:\mBbbZ{}
(b4 \mmember{} Memory-class(rsc4\_update\_round(Cmd) a;rsc4\_init()
0;rsc4\_RoundInfo(Cmd))(e1)
\mwedge{} (b4 < b)))
\mwedge{} (\mexists{}b1:Cmd
(<<a, b>, b1> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e1)
\mdownarrow{}\mvee{} (\mexists{}b5:Id
<<<a, b>, b1>, b5> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e1)))))
\mwedge{} (\mdownarrow{}\mexists{}b1:\mBbbZ{}
((k1 = (b1 + 1))
\mwedge{} (\mexists{}b2:Cmd
\mexists{}b3:Id
(<<<k, b1>, b2>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)
\mwedge{} (\mexists{}a2:Cmd List
((((||a2|| = (coeff * flrs))
\mwedge{} (\mneg{}((fst(poss-maj(cmdeq;[b2 / a2];b2)))
= ((coeff * flrs) + 1))))
\mwedge{} (v = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
\mwedge{} (\mexists{}b4:Id List
(<a2, b4> \mmember{}
Memory-class(rsc4\_add\_to\_quorum(Cmd)
<a, b>rsc4\_init()
<[], []>rsc4\_vote'base(Cmd))(e)
\mwedge{} (\muparrow{}(rsc4\_newvote(Cmd) <a, b> <<<k, b1>, b2>, b3>
<a2, b4>)))))))))))
\mwedge{} (\mdownarrow{}(no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e1 and e))))
\mwedge{} (no rsc4\_Notify(Cmd;clients) a between e' and e))))))
Date html generated:
2012_02_20-PM-04_57_07
Last ObjectModification:
2012_02_02-PM-02_16_19
Home
Index