Step
*
3
of Lemma
rsc4-validity-property
1. Cmd : {T:Type| valueall-type(T)}
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs : 
7. es : EO'
8. StandardAssumptions(rsc4_Main) es
9. e : E
10. 
e1:E
((e1 < e)
((v:
Cmd. (v 
rsc4_decided'base(Cmd)(e1) (
e':E. ((e' < e1) 
v rsc4_propose'base(Cmd)(e')))))
(v: Cmd Id
(v rsc4_vote'base(Cmd)(e1)
(e':E. ((e' < e1) <fst(fst(fst(v))), snd(fst(v))> rsc4_propose'base(Cmd)(e')))))
(v: Cmd
(v rsc4_retry'base(Cmd)(e1)
(e':E. ((e' < e1) <fst(fst(v)), snd(v)> rsc4_propose'base(Cmd)(e')))))
(e2:E
(e2 c
e1
(cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
(<cs, L> rsc4_QuorumState(Cmd) <n, rnd>(e1)
(c cs)
(e':E. ((e' < e1) <n, c> rsc4_propose'base(Cmd)(e')))))))))
11. n1 :
12. n :
13. c : Cmd
14. <<n1, n>, c> rsc4_retry'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e') locs
18. loc(e) = loc(e')
19. e1 : {e1:E| e1 loc e' }
20. a :
21. a2 :
22. b2 : List
23. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
24. (a2 < a) 
(a b2)
25. b : Cmd
26. True
27. <a, b> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
28. ((b1:
((n = (b1 + 1))
(b2:Cmd
b3:Id
(<<<n1, 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))))
(c = (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> <<<n1, b1>, b2>, b3> <a2, b4>))))))))))
((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')))
((e2:{e1:E| e1 loc e' }
b:
((((b4:. (b4 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2) (b4 < b)))
(b1:Cmd
(<<a, b>, b1> Base(``rsc4 retry``; Cmd)(e2)
(b5:Id. <<<a, b>, b1>, b5> Base(``rsc4 vote``; Cmd Id)(e2)))))
(b1:
((n = (b1 + 1))
(b2:Cmd
b3:Id
(<<<n1, 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))))
(c = (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> <<<n1, b1>, b2>, b3> <a2, b4>)))))))))))
((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e2 and e'))))
(no rsc4_Notify(Cmd;clients) a between e1 and e'))
e':E. ((e' < e) <n1, c> rsc4_propose'base(Cmd)(e'))
BY
{ (RepeatFor 2 ((AllHypsThat (\t. member `c' (free_vars t)) DOr THEN SqExRepD)
)
THEN RenameTypedVars
[
Cmd List
, `cs'; Cmd, `cmd';Id List, `L'; Id,`loc']
THEN AllHyps h.FoldAbstracting [1;2] `rsc4_QuorumState` h ) }
1
1. Cmd : {T:Type| valueall-type(T)}
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs :
7. es : EO'
8. StandardAssumptions(rsc4_Main) es
9. e : E
10. e1:E
((e1 < e)
((v: Cmd. (v rsc4_decided'base(Cmd)(e1) (e':E. ((e' < e1) v rsc4_propose'base(Cmd)(e')))))
(v: Cmd Id
(v rsc4_vote'base(Cmd)(e1)
(e':E. ((e' < e1) <fst(fst(fst(v))), snd(fst(v))> rsc4_propose'base(Cmd)(e')))))
(v: Cmd
(v rsc4_retry'base(Cmd)(e1)
(e':E. ((e' < e1) <fst(fst(v)), snd(v)> rsc4_propose'base(Cmd)(e')))))
(e2:E
(e2 c e1
(cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
(<cs, L> rsc4_QuorumState(Cmd) <n, rnd>(e1)
(c cs)
(e':E. ((e' < e1) <n, c> rsc4_propose'base(Cmd)(e')))))))))
11. n1 :
12. n :
13. c2 : Cmd
14. <<n1, n>, c2> rsc4_retry'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e') locs
18. loc(e) = loc(e')
19. e1 : {e1:E| e1 loc e' }
20. a :
21. a2 :
22. b2 : List
23. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
24. (a2 < a) (a b2)
25. c1 : Cmd
26. True
27. <a, c1> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, c1>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
28. b1 :
29. n = (b1 + 1)
30. cmd : Cmd
31. loc : Id
32. <<<n1, b1>, cmd>, loc> Base(``rsc4 vote``; Cmd Id)(e')
33. cs : Cmd List
34. ||cs|| = (coeff * flrs)
35. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
36. c2 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
37. L : Id List
38. <cs, L> rsc4_QuorumState(Cmd) <a, 0>(e')
39. (rsc4_newvote(Cmd) <a, 0> <<<n1, b1>, cmd>, loc> <cs, L>)
40. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
e':E. ((e' < e) <n1, c2> rsc4_propose'base(Cmd)(e'))
2
1. Cmd : {T:Type| valueall-type(T)}
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs :
7. es : EO'
8. StandardAssumptions(rsc4_Main) es
9. e : E
10. e1:E
((e1 < e)
((v: Cmd. (v rsc4_decided'base(Cmd)(e1) (e':E. ((e' < e1) v rsc4_propose'base(Cmd)(e')))))
(v: Cmd Id
(v rsc4_vote'base(Cmd)(e1)
(e':E. ((e' < e1) <fst(fst(fst(v))), snd(fst(v))> rsc4_propose'base(Cmd)(e')))))
(v: Cmd
(v rsc4_retry'base(Cmd)(e1)
(e':E. ((e' < e1) <fst(fst(v)), snd(v)> rsc4_propose'base(Cmd)(e')))))
(e2:E
(e2 c e1
(cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
(<cs, L> rsc4_QuorumState(Cmd) <n, rnd>(e1)
(c cs)
(e':E. ((e' < e1) <n, c> rsc4_propose'base(Cmd)(e')))))))))
11. n1 :
12. n :
13. c3 : Cmd
14. <<n1, n>, c3> rsc4_retry'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e') locs
18. loc(e) = loc(e')
19. e1 : {e1:E| e1 loc e' }
20. a :
21. a2 :
22. b2 : List
23. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
24. (a2 < a) (a b2)
25. c2 : Cmd
26. True
27. <a, c2> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, c2>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
28. e2 : {e1:E| e1 loc e' }
29. b3 :
30. b6 :
31. b6 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
32. b6 < b3
33. c1 : Cmd
34. True
35. <<a, b3>, c1> Base(``rsc4 retry``; Cmd)(e2)
(b5@0:Id. <<<a, b3>, c1>, b5@0> Base(``rsc4 vote``; Cmd Id)(e2))
36. b1 :
37. n = (b1 + 1)
38. cmd : Cmd
39. loc : Id
40. <<<n1, b1>, cmd>, loc> Base(``rsc4 vote``; Cmd Id)(e')
41. cs : Cmd List
42. ||cs|| = (coeff * flrs)
43. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
44. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
45. L : Id List
46. <cs, L> rsc4_QuorumState(Cmd) <a, b3>(e')
47. (rsc4_newvote(Cmd) <a, b3> <<<n1, b1>, cmd>, loc> <cs, L>)
48. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
49. (no rsc4_Notify(Cmd;clients) a between e1 and e')
e':E. ((e' < e) <n1, c3> rsc4_propose'base(Cmd)(e'))
1. Cmd : \{T:Type| valueall-type(T)\}
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : \{2...\}
6. flrs : \mBbbN{}
7. es : EO'
8. StandardAssumptions(rsc4\_Main) es
9. e : E
10. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} ((\mforall{}v:\mBbbZ{} \mtimes{} Cmd
(v \mmember{} rsc4\_decided'base(Cmd)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} v \mmember{} rsc4\_propose'base(Cmd)(e')))))
\mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id
(v \mmember{} rsc4\_vote'base(Cmd)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' < e1) \mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{} rsc4\_propose'base(Cmd)(e')))))
\mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd
(v \mmember{} rsc4\_retry'base(Cmd)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} <fst(fst(v)), snd(v)> \mmember{} rsc4\_propose'base(Cmd)(e')))))
\mwedge{} (\mforall{}e2:E
(e2 c\mleq{} e1
{}\mRightarrow{} (\mforall{}cs:Cmd List. \mforall{}L:Id List. \mforall{}n,rnd:\mBbbZ{}. \mforall{}c:Cmd.
(<cs, L> \mmember{} rsc4\_QuorumState(Cmd) <n, rnd>(e1)
{}\mRightarrow{} (c \mmember{} cs)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} <n, c> \mmember{} rsc4\_propose'base(Cmd)(e')))))))))
11. n1 : \mBbbZ{}
12. n : \mBbbZ{}
13. c : Cmd
14. <<n1, n>, c> \mmember{} rsc4\_retry'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e') \mdownarrow{}\mmember{} locs
18. loc(e) = loc(e')
19. e1 : \{e1:E| e1 \mleq{}loc e' \}
20. a : \mBbbZ{}
21. a2 : \mBbbZ{}
22. b2 : \mBbbZ{} List
23. <a2, b2> \mmember{} Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init() ɘ, []>rsc4\_Proposal(Cmd))(e1)
24. (a2 < a) \mvee{} (a \mmember{} b2)
25. b : Cmd
26. True
27. <a, b> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e1)
\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, b>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e1))
28. ((\mdownarrow{}\mexists{}b1:\mBbbZ{}
((n = (b1 + 1))
\mwedge{} (\mexists{}b2:Cmd
\mexists{}b3:Id
(<<<n1, 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{} (c = (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> <<<n1, b1>, b2>, b3> <a2, b4>))))))))))
\mwedge{} (\mdownarrow{}(no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')))
\mvee{} ((\mdownarrow{}\mexists{}e2:\{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))(e2)
\mwedge{} (b4 < b)))
\mwedge{} (\mexists{}b1:Cmd
(<<a, b>, b1> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e2)
\mdownarrow{}\mvee{} (\mexists{}b5:Id. <<<a, b>, b1>, b5> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e2)))))
\mwedge{} (\mdownarrow{}\mexists{}b1:\mBbbZ{}
((n = (b1 + 1))
\mwedge{} (\mexists{}b2:Cmd
\mexists{}b3:Id
(<<<n1, 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{} (c = (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> <<<n1, b1>, b2>, b3> <a2, b4>)))))))))))
\mwedge{} (\mdownarrow{}(no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e2 and e'))))
\mwedge{} (no rsc4\_Notify(Cmd;clients) a between e1 and e'))
\mvdash{} \mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <n1, c> \mmember{} rsc4\_propose'base(Cmd)(e'))
By
(RepeatFor 2 ((AllHypsThat (\mbackslash{}t. member `c' (free\_vars t)) DOr THEN SqExRepD)\mcdot{})\mcdot{}
THEN RenameTypedVars
[\mkleeneopen{}Cmd List\mkleeneclose{}, `cs'; \mkleeneopen{}Cmd\mkleeneclose{}, `cmd';\mkleeneopen{}Id List\mkleeneclose{}, `L'; \mkleeneopen{}Id\mkleeneclose{},`loc']\mcdot{}
THEN AllHyps h.FoldAbstracting [1;2] `rsc4\_QuorumState` h )\mcdot{}
Home
Index