Nuprl Lemma : RSC_decided
[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [flrs:
]. [locs:bag(Id)]. [es:EO']. [e:E].
[i:Id]. [k:]. [v:Cmd].
(<i, make-Msg(``sc decided``; 
Cmd;<k, v>)> 
RSC_main(Cmd;clients;cmdeq;flrs;locs)(e)
loc(e) 
locs
(i = loc(e))
(
e':{e':E| e' 
loc e }
z:
((z1:Cmd
((b:
b1: List
(<b, b1> Prior(Accum-class(
v,state.
if RSC_new_proposal() v state
then RSC_onnewpropose() v state
else state
fi ;RSC_init() <0, []>;RSC_Proposal(Cmd)))?RSC_init() <0, []>(e')
(
(RSC_new_proposal() <z, z1> <b, b1>))))
(<z, z1> Base(``sc propose``; Cmd)(e')
(a3:. a5:Id. <<<z, a3>, z1>, a5> Base(``sc vote``; Cmd Id)(e')))))
(((a1:
a2:Cmd
a3:Id
(<<<k, a1>, a2>, a3> Base(``sc vote``; Cmd Id)(e)
(b:Cmd List
((((||b|| = (2 * flrs)) ((fst(poss-maj(cmdeq;[a2 / b];a2))) = ((2 * flrs) + 1)))
(v = (snd(poss-maj(cmdeq;[a2 / b];a2)))))
(b1:Id List
(<b, b1> Prior(Accum-class(v,state.
if RSC_newvote(Cmd) <z, 0> v state
then RSC_addvote() v state
else state
fi ;RSC_init() <[], []>;RSC_Vote(Cmd)))?RSC_init() <[], []>(
e)
((RSC_newvote(Cmd) <z, 0> <<<k, a1>, a2>, a3> <b, b1>))))))))
(no RSC_Quorum(Cmd;cmdeq;flrs) <z, 0> between e' and e))
((e1:{e1:E| e1 loc e }
z2,z3:
(((z4:Cmd
((b:{x:| x = 0}
(b Prior(Accum-class(v,state.
if RSC_round_increase() z v state
then RSC_incround() v state
else state
fi ;RSC_init() 0;RSC_RoundInfo(Cmd)))?RSC_init() 0(e1)
((RSC_round_increase() z <<z2, z3>, z4> b))))
(<<z2, z3>, z4> Base(``sc retry``; Cmd)(e1)
(a6:Id. <<<z2, z3>, z4>, a6> Base(``sc vote``; Cmd Id)(e1)))))
(a1:
a2:Cmd
a3:Id
(<<<k, a1>, a2>, a3> Base(``sc vote``; Cmd Id)(e)
(b:Cmd List
((((||b|| = (2 * flrs)) ((fst(poss-maj(cmdeq;[a2 / b];a2))) = ((2 * flrs) + 1)))
(v = (snd(poss-maj(cmdeq;[a2 / b];a2)))))
(b1:Id List
(<b, b1> Prior(Accum-class(v,state.
if RSC_newvote(Cmd) <z2, z3> v state
then RSC_addvote() v state
else state
fi ;RSC_init() <[], []>;RSC_Vote(Cmd)))?RSC_init()
<[], []>(e)
((RSC_newvote(Cmd) <z2, z3> <<<k, a1>, a2>, a3> <b, b1>)))))))))
((no RSC_Quorum(Cmd;cmdeq;flrs) <z2, z3> between e1 and e))))
(no RSC_Notify(Cmd;clients) z between e' and e))))))
Proof not projected
Error : references
\mforall{}[Cmd:ValueAllType]. \mforall{}[clients:bag(Id)]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[flrs:\mBbbZ{}]. \mforall{}[locs:bag(Id)].
\mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[k:\mBbbZ{}]. \mforall{}[v:Cmd].
(<i, make-Msg(``sc decided``;\mBbbZ{} \mtimes{} Cmd;<k, v>)> \mmember{} RSC\_main(Cmd;clients;cmdeq;flrs;locs)(e)
\mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} locs
\mwedge{} (i = loc(e))
\mwedge{} (\mdownarrow{}\mexists{}e':\{e':E| e' \mleq{}loc e \}
\mexists{}z:\mBbbZ{}
((\mexists{}z1:Cmd
((\mdownarrow{}\mexists{}b:\mBbbZ{}
\mexists{}b1:\mBbbZ{} List
(<b, b1> \mmember{} Prior(Accum-class(\mlambda{}v,state.
if RSC\_new\_proposal() v state
then RSC\_onnewpropose() v state
else state
fi ;RSC\_init()
ɘ, []>RSC\_Proposal(Cmd)))?RSC\_init()
ɘ, []>(e')
\mwedge{} (\muparrow{}(RSC\_new\_proposal() <z, z1> <b, b1>))))
\mwedge{} (<z, z1> \mmember{} Base(``sc propose``;\mBbbZ{} \mtimes{} Cmd)(e')
\mdownarrow{}\mvee{} (\mexists{}a3:\mBbbZ{}. \mexists{}a5:Id. <<<z, a3>, z1>, a5> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e')))))
\mwedge{} (\mdownarrow{}((\mdownarrow{}\mexists{}a1:\mBbbZ{}
\mexists{}a2:Cmd
\mexists{}a3:Id
(<<<k, a1>, a2>, a3> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)
\mwedge{} (\mexists{}b:Cmd List
((((||b|| = (2 * flrs))
\mwedge{} ((fst(poss-maj(cmdeq;[a2 / b];a2))) = ((2 * flrs) + 1)))
\mwedge{} (v = (snd(poss-maj(cmdeq;[a2 / b];a2)))))
\mwedge{} (\mexists{}b1:Id List
(<b, b1> \mmember{} Prior(Accum-class(\mlambda{}v,state.
if RSC\_newvote(Cmd) <z, 0> v state
then RSC\_addvote() v state
else state
fi ;RSC\_init()
<[], []>RSC\_Vote(Cmd)))?RSC\_init()
<[], []>(e)
\mwedge{} (\muparrow{}(RSC\_newvote(Cmd) <z, 0> <<<k, a1>, a2>, a3> <b, b1>))))))))
\mwedge{} (no RSC\_Quorum(Cmd;cmdeq;flrs) <z, 0> between e' and e))
\mvee{} ((\mdownarrow{}\mexists{}e1:\{e1:E| e1 \mleq{}loc e \}
\mexists{}z2,z3:\mBbbZ{}
(((\mexists{}z4:Cmd
((\mdownarrow{}\mexists{}b:\{x:\mBbbZ{}| x = 0\}
(b \mmember{} Prior(Accum-class(\mlambda{}v,state.
if RSC\_round\_increase() z v state
then RSC\_incround() v state
else state
fi ;RSC\_init()
0;RSC\_RoundInfo(Cmd)))?RSC\_init() 0(e1)
\mwedge{} (\muparrow{}(RSC\_round\_increase() z <<z2, z3>, z4> b))))
\mwedge{} (<<z2, z3>, z4> \mmember{} Base(``sc retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e1)
\mdownarrow{}\mvee{} (\mexists{}a6:Id
<<<z2, z3>, z4>, a6> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e1)))))
\mwedge{} (\mdownarrow{}\mexists{}a1:\mBbbZ{}
\mexists{}a2:Cmd
\mexists{}a3:Id
(<<<k, a1>, a2>, a3> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)
\mwedge{} (\mexists{}b:Cmd List
((((||b|| = (2 * flrs))
\mwedge{} ((fst(poss-maj(cmdeq;[a2 / b];a2))) = ((2 * flrs) + 1)))
\mwedge{} (v = (snd(poss-maj(cmdeq;[a2 / b];a2)))))
\mwedge{} (\mexists{}b1:Id List
(<b, b1> \mmember{}
Prior(Accum-class(\mlambda{}v,state.
if RSC\_newvote(Cmd) <z2, z3> v state
then RSC\_addvote() v state
else state
fi ;RSC\_init()
<[], []>RSC\_Vote(Cmd)))?RSC\_init()
<[], []>(e)
\mwedge{} (\muparrow{}(RSC\_newvote(Cmd) <z2, z3> <<<k, a1>, a2>, a3>
<b, b1>)))))))))
\mwedge{} (\mdownarrow{}(no RSC\_Quorum(Cmd;cmdeq;flrs) <z2, z3> between e1 and e))))
\mwedge{} (no RSC\_Notify(Cmd;clients) z between e' and e))))))
Date html generated:
2012_02_20-PM-07_50_59
Last ObjectModification:
2012_02_02-PM-01_59_21
Home
Index