Step
*
1
2
1
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. n :
12. c3 : Cmd
13. <n, c3> rsc4_decided'base(Cmd)(e)
14. e' : E
15. (e' < e)
16. loc(e') locs
17. loc(e) = loc(e')
18. e1 : {e1:E| e1 loc e' }
19. a :
20. a2 :
21. b2 : List
22. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
23. (a2 < a) 
(a b2)
24. c2 : Cmd
25. True
26. <a, c2> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, c2>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
27. e2 : {e1:E| e1 loc e' }
28. b3 :
29. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
30. b5 :
31. c1 : Cmd
32. loc : Id
33. <<<n, b5>, c1>, loc> Base(``rsc4 vote``; Cmd Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
37. c3 = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
38. L : Id List
39. <cs, L> rsc4_QuorumState(Cmd) <a, b3>(e')
40. 
(rsc4_newvote(Cmd) <a, b3> <<<n, b5>, c1>, loc> <cs, L>)
41. cmd : Cmd
42. True
43. <<a, b3>, cmd> Base(``rsc4 retry``; Cmd)(e2)
(b5:Id. <<<a, b3>, cmd>, b5> Base(``rsc4 vote``; Cmd Id)(e2))
44. b4 :
45. b4 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
46. b4 < b3
47. (no rsc4_Notify(Cmd;clients) a between e1 and e')
48. (c3 = c1) (c3 cs)
e':E. ((e' < e) <n, c3> rsc4_propose'base(Cmd)(e'))
BY
{ (AllHyps h.((Unfold `rsc4_newvote` h THEN Reduce h) THEN RW assert_pushdownC h THEN Auto)
THEN ((InstHyp [
e'
] 10 
THENM ExRepD) THENA MaAuto)
THEN (D -5
THEN skip{(Try (((InstHyp [e1;cs;L;a;0;c2] (-1) THENA MaAuto)
THEN RepeatFor 3 (ParallelLast)
THEN MaAuto))
THEN RepUR ``rsc4_vote'base`` -3
THEN OnMaybeHyp 30 (\h. ((FHyp (-3) [h] THENA Auto)
THEN Reduce (-1)
THEN RepeatFor 3 (ParallelLast)
THEN Complete (MaAuto))))}
)) }
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. n :
12. c3 : Cmd
13. <n, c3> rsc4_decided'base(Cmd)(e)
14. e' : E
15. (e' < e)
16. loc(e') locs
17. loc(e) = loc(e')
18. e1 : {e1:E| e1 loc e' }
19. a :
20. a2 :
21. b2 : List
22. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
23. (a2 < a) (a b2)
24. c2 : Cmd
25. True
26. <a, c2> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, c2>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
27. e2 : {e1:E| e1 loc e' }
28. b3 :
29. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
30. b5 :
31. c1 : Cmd
32. loc : Id
33. <<<n, b5>, c1>, loc> Base(``rsc4 vote``; Cmd Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
37. c3 = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
38. L : Id List
39. <cs, L> rsc4_QuorumState(Cmd) <a, b3>(e')
40. a = n
41. b3 = b5
42. 
(loc L)
43. cmd : Cmd
44. True
45. <<a, b3>, cmd> Base(``rsc4 retry``; Cmd)(e2)
(b5:Id. <<<a, b3>, cmd>, b5> Base(``rsc4 vote``; Cmd Id)(e2))
46. b4 :
47. b4 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
48. b4 < b3
49. (no rsc4_Notify(Cmd;clients) a between e1 and e')
50. c3 = c1
51. v: Cmd. (v rsc4_decided'base(Cmd)(e') (e'@0:E. ((e'@0 < e') v rsc4_propose'base(Cmd)(e'@0))))
52. v: Cmd Id
(v rsc4_vote'base(Cmd)(e')
(e'@0:E. ((e'@0 < e') <fst(fst(fst(v))), snd(fst(v))> rsc4_propose'base(Cmd)(e'@0))))
53. v: Cmd
(v rsc4_retry'base(Cmd)(e') (e'@0:E. ((e'@0 < e') <fst(fst(v)), snd(v)> rsc4_propose'base(Cmd)(e'@0))))
54. e2:E
(e2 c e'
(cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
(<cs, L> rsc4_QuorumState(Cmd) <n, rnd>(e')
(c cs)
(e'@0:E. ((e'@0 < e') <n, c> rsc4_propose'base(Cmd)(e'@0))))))
e':E. ((e' < e) <n, c3> 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. n :
12. c3 : Cmd
13. <n, c3> rsc4_decided'base(Cmd)(e)
14. e' : E
15. (e' < e)
16. loc(e') locs
17. loc(e) = loc(e')
18. e1 : {e1:E| e1 loc e' }
19. a :
20. a2 :
21. b2 : List
22. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
23. (a2 < a) (a b2)
24. c2 : Cmd
25. True
26. <a, c2> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, c2>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
27. e2 : {e1:E| e1 loc e' }
28. b3 :
29. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
30. b5 :
31. c1 : Cmd
32. loc : Id
33. <<<n, b5>, c1>, loc> Base(``rsc4 vote``; Cmd Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
37. c3 = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
38. L : Id List
39. <cs, L> rsc4_QuorumState(Cmd) <a, b3>(e')
40. a = n
41. b3 = b5
42. (loc L)
43. cmd : Cmd
44. True
45. <<a, b3>, cmd> Base(``rsc4 retry``; Cmd)(e2)
(b5:Id. <<<a, b3>, cmd>, b5> Base(``rsc4 vote``; Cmd Id)(e2))
46. b4 :
47. b4 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
48. b4 < b3
49. (no rsc4_Notify(Cmd;clients) a between e1 and e')
50. (c3 cs)
51. v: Cmd. (v rsc4_decided'base(Cmd)(e') (e'@0:E. ((e'@0 < e') v rsc4_propose'base(Cmd)(e'@0))))
52. v: Cmd Id
(v rsc4_vote'base(Cmd)(e')
(e'@0:E. ((e'@0 < e') <fst(fst(fst(v))), snd(fst(v))> rsc4_propose'base(Cmd)(e'@0))))
53. v: Cmd
(v rsc4_retry'base(Cmd)(e') (e'@0:E. ((e'@0 < e') <fst(fst(v)), snd(v)> rsc4_propose'base(Cmd)(e'@0))))
54. e2:E
(e2 c e'
(cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
(<cs, L> rsc4_QuorumState(Cmd) <n, rnd>(e')
(c cs)
(e'@0:E. ((e'@0 < e') <n, c> rsc4_propose'base(Cmd)(e'@0))))))
e':E. ((e' < e) <n, 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. n : \mBbbZ{}
12. c3 : Cmd
13. <n, c3> \mmember{} rsc4\_decided'base(Cmd)(e)
14. e' : E
15. (e' < e)
16. loc(e') \mdownarrow{}\mmember{} locs
17. loc(e) = loc(e')
18. e1 : \{e1:E| e1 \mleq{}loc e' \}
19. a : \mBbbZ{}
20. a2 : \mBbbZ{}
21. b2 : \mBbbZ{} List
22. <a2, b2> \mmember{} Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init() ɘ, []>rsc4\_Proposal(Cmd))(e1)
23. (a2 < a) \mvee{} (a \mmember{} b2)
24. c2 : Cmd
25. True
26. <a, c2> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e1)
\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, c2>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e1))
27. e2 : \{e1:E| e1 \mleq{}loc e' \}
28. b3 : \mBbbZ{}
29. (no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
30. b5 : \mBbbZ{}
31. c1 : Cmd
32. loc : Id
33. <<<n, b5>, c1>, loc> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
37. c3 = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
38. L : Id List
39. <cs, L> \mmember{} rsc4\_QuorumState(Cmd) <a, b3>(e')
40. \muparrow{}(rsc4\_newvote(Cmd) <a, b3> <<<n, b5>, c1>, loc> <cs, L>)
41. cmd : Cmd
42. True
43. <<a, b3>, cmd> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e2)
\mvee{} (\mexists{}b5:Id. <<<a, b3>, cmd>, b5> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e2))
44. b4 : \mBbbZ{}
45. b4 \mmember{} Memory-class(rsc4\_update\_round(Cmd) a;rsc4\_init() 0;rsc4\_RoundInfo(Cmd))(e2)
46. b4 < b3
47. (no rsc4\_Notify(Cmd;clients) a between e1 and e')
48. (c3 = c1) \mvee{} (c3 \mmember{} cs)
\mvdash{} \mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <n, c3> \mmember{} rsc4\_propose'base(Cmd)(e'))
By
(AllHyps h.((Unfold `rsc4\_newvote` h THEN Reduce h) THEN RW assert\_pushdownC h THEN Auto)
THEN ((InstHyp [\mkleeneopen{}e'\mkleeneclose{}] 10 \mcdot{} THENM ExRepD) THENA MaAuto)
THEN (D -5
THEN skip\{(Try (((InstHyp [\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}cs\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{}] (-1)\mcdot{} THENA MaAuto)
THEN RepeatFor 3 (ParallelLast)
THEN MaAuto))
THEN RepUR ``rsc4\_vote'base`` -3
THEN OnMaybeHyp 30 (\mbackslash{}h. ((FHyp (-3) [h] THENA Auto)
THEN Reduce (-1)
THEN RepeatFor 3 (ParallelLast)
THEN Complete (MaAuto))))\}
)\mcdot{})\mcdot{}
Home
Index