Nuprl Lemma : rsc4-vote2
[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:
]. [locs:bag(Id)]. [es:EO']. [e:E].
[rcvr:Id]. [num,rnd:]. [c:Cmd]. [sndr:Id].
(<rcvr, rsc4_vote'msg(Cmd;<<<num, rnd>, c>, sndr>)> 
rsc4_Main(e)
loc(e) 
locs
(rcvr locs (sndr = loc(e)))
(
e':{e':E| e' 
loc e }
((max:. missing: List. (<max, missing> rsc4_ReplicaState(Cmd)(e') ((max < num) 
(num missing))))
(c':Cmd
((((e = e') (c = c') (rnd = 0))
((e1:{e1:E| e1 loc e }
(((maxr:. (maxr rsc4_NewRoundsState(Cmd) num(e1) (maxr < rnd)))
(<<num, rnd>, c> rsc4_retry'base(Cmd)(e1)
(sndr':Id. <<<num, rnd>, c>, sndr'> rsc4_vote'base(Cmd)(e1))))
(e = e1)))
(no rsc4_Notify(Cmd;clients) num between e' and e)))
(<num, c'> rsc4_propose'base(Cmd)(e')
(rnd':. sndr':Id. <<<num, rnd'>, c'>, sndr'> rsc4_vote'base(Cmd)(e'))))))))
Proof
Definitions occuring in Statement :
rsc4_vote'msg: rsc4_vote'msg(Cmd;vote),
rsc4_main: rsc4_Main,
rsc4_ReplicaState: rsc4_ReplicaState(Cmd),
rsc4_Notify: rsc4_Notify(Cmd;clients),
rsc4_NewRoundsState: rsc4_NewRoundsState(Cmd),
rsc4_propose'base: rsc4_propose'base(Cmd),
rsc4_retry'base: rsc4_retry'base(Cmd),
rsc4_vote'base: rsc4_vote'base(Cmd),
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,
sq_or: a b,
uall: [x:A]. B[x],
exists: x:A. B[x],
iff: P Q,
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],
list: type List,
natural_number: $n,
int: ,
equal: s = t,
l_member: (x l),
deq: EqDecider(T),
bag-member: x bs,
bag: bag(T),
vatype: ValueAllType
Definitions :
rsc4_propose'base: rsc4_propose'base(Cmd),
rsc4_vote'base: rsc4_vote'base(Cmd),
rsc4_retry'base: rsc4_retry'base(Cmd),
rsc4_NewRoundsState: rsc4_NewRoundsState(Cmd),
rsc4_ReplicaState: rsc4_ReplicaState(Cmd),
rsc4_vote'msg: rsc4_vote'msg(Cmd;vote)
Lemmas :
rsc4-vote
\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{}[rcvr:Id]. \mforall{}[num,rnd:\mBbbZ{}]. \mforall{}[c:Cmd]. \mforall{}[sndr:Id].
(<rcvr, rsc4\_vote'msg(Cmd;<<<num, rnd>, c>, sndr>)> \mmember{} rsc4\_Main(e)
\mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} locs
\mwedge{} (rcvr \mdownarrow{}\mmember{} locs \mwedge{} (sndr = loc(e)))
\mwedge{} (\mdownarrow{}\mexists{}e':\{e':E| e' \mleq{}loc e \}
((\mdownarrow{}\mexists{}max:\mBbbZ{}
\mexists{}missing:\mBbbZ{} List
(<max, missing> \mmember{} rsc4\_ReplicaState(Cmd)(e') \mwedge{} ((max < num) \mvee{} (num \mmember{} missing))))
\mwedge{} (\mexists{}c':Cmd
((\mdownarrow{}((e = e') \mwedge{} (c = c') \mwedge{} (rnd = 0))
\mvee{} ((\mdownarrow{}\mexists{}e1:\{e1:E| e1 \mleq{}loc e \}
(((\mdownarrow{}\mexists{}maxr:\mBbbZ{}. (maxr \mmember{} rsc4\_NewRoundsState(Cmd) num(e1) \mwedge{} (maxr < rnd)))
\mwedge{} (<<num, rnd>, c> \mmember{} rsc4\_retry'base(Cmd)(e1)
\mdownarrow{}\mvee{} (\mexists{}sndr':Id. <<<num, rnd>, c>, sndr'> \mmember{} rsc4\_vote'base(Cmd)(e1))))
\mwedge{} (e = e1)))
\mwedge{} (no rsc4\_Notify(Cmd;clients) num between e' and e)))
\mwedge{} (<num, c'> \mmember{} rsc4\_propose'base(Cmd)(e')
\mdownarrow{}\mvee{} (\mexists{}rnd':\mBbbZ{}. \mexists{}sndr':Id. <<<num, rnd'>, c'>, sndr'> \mmember{} rsc4\_vote'base(Cmd)(e'))))))))
Date html generated:
2012_02_20-PM-04_56_48
Last ObjectModification:
2012_02_02-PM-02_16_17
Home
Index