Step
*
4
2
1
1
of Lemma
rsc4-decided-property
1. Cmd : Type
2. Cmd 
ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff : 
8. flrs :
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c : Cmd
13. n :
14. <n, c> rsc4_decided'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. e2 : {e1:E| e1 loc e' }
29. b3 :
30. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
31. b5 :
32. c1 : Cmd
33. lastloc : Id
34. <<<n, b5>, c1>, lastloc> Base(``rsc4 vote``; Cmd Id)(e')
35. cs : Cmd List
36. ||cs|| = (coeff * flrs)
37. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
38. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
39. L : Id List
40. <cs, L> Memory-class(rsc4_add_to_quorum(Cmd) <a, b3>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
41. a = n
42. b3 = b5
43. 
(lastloc L)
44. b1 : Cmd
45. True
46. <<a, b3>, b1> Base(``rsc4 retry``; Cmd)(e2)
(b5:Id. <<<a, b3>, b1>, b5> Base(``rsc4 vote``; Cmd Id)(e2))
47. b4 :
48. b4 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
49. b4 < b3
50. (no rsc4_Notify(Cmd;clients) a between e1 and e')
51. (
z[c1 / cs].z = c)
52. ||cs|| = ||L||
53. no_repeats(Id;L)
54. <cs, L> rsc4_QuorumState(Cmd) <a, b3>(e')
55. no_repeats(Id;L)
56. ||L|| = ||cs||
57. i:
||L||. (e:E. (e loc e' 
<<<a, b3>, cs[i]>, L[i]> rsc4_vote'base(Cmd)(e)))
58. vtr : Id
59. vtr = lastloc
(e'@0:E. <loc(e'), make-Msg(``rsc4 vote``; Cmd Id;<<<n, b3>, c>, vtr>)> rsc4_Main(e'@0)) vtr locs
BY
{ ((UseMessageConstraint 34 THENA MaAuto) THEN TrySquashExRepD (-1) THEN MaAuto) }
1
1. Cmd : Type
2. Cmd ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff :
8. flrs :
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c : Cmd
13. n :
14. <n, c> rsc4_decided'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. e2 : {e1:E| e1 loc e' }
29. b3 :
30. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
31. b5 :
32. c1 : Cmd
33. lastloc : Id
34. <<<n, b5>, c1>, lastloc> Base(``rsc4 vote``; Cmd Id)(e')
35. cs : Cmd List
36. ||cs|| = (coeff * flrs)
37. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
38. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
39. L : Id List
40. <cs, L> Memory-class(rsc4_add_to_quorum(Cmd) <a, b3>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
41. a = n
42. b3 = b5
43. (lastloc L)
44. b1 : Cmd
45. True
46. <<a, b3>, b1> Base(``rsc4 retry``; Cmd)(e2)
(b5:Id. <<<a, b3>, b1>, b5> Base(``rsc4 vote``; Cmd Id)(e2))
47. b4 :
48. b4 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
49. b4 < b3
50. (no rsc4_Notify(Cmd;clients) a between e1 and e')
51. (z[c1 / cs].z = c)
52. ||cs|| = ||L||
53. no_repeats(Id;L)
54. <cs, L> rsc4_QuorumState(Cmd) <a, b3>(e')
55. no_repeats(Id;L)
56. ||L|| = ||cs||
57. i:||L||. (e:E. (e loc e' <<<a, b3>, cs[i]>, L[i]> rsc4_vote'base(Cmd)(e)))
58. vtr : Id
59. vtr = lastloc
60. e'@0 : E
61. (e'@0 < e')
62. <loc(e'), make-Msg(``rsc4 vote``; Cmd Id;<<<n, b5>, c1>, lastloc>)> rsc4_Main(e'@0)
e'@0:E. <loc(e'), make-Msg(``rsc4 vote``; Cmd Id;<<<n, b3>, c>, vtr>)> rsc4_Main(e'@0)
2
1. Cmd : Type
2. Cmd ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff :
8. flrs :
9. es : EO'
10. StandardAssumptions(rsc4_Main) es
11. e : E
12. c : Cmd
13. n :
14. <n, c> rsc4_decided'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. e2 : {e1:E| e1 loc e' }
29. b3 :
30. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
31. b5 :
32. c1 : Cmd
33. lastloc : Id
34. <<<n, b5>, c1>, lastloc> Base(``rsc4 vote``; Cmd Id)(e')
35. cs : Cmd List
36. ||cs|| = (coeff * flrs)
37. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
38. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
39. L : Id List
40. <cs, L> Memory-class(rsc4_add_to_quorum(Cmd) <a, b3>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
41. a = n
42. b3 = b5
43. (lastloc L)
44. b1 : Cmd
45. True
46. <<a, b3>, b1> Base(``rsc4 retry``; Cmd)(e2)
(b5:Id. <<<a, b3>, b1>, b5> Base(``rsc4 vote``; Cmd Id)(e2))
47. b4 :
48. b4 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
49. b4 < b3
50. (no rsc4_Notify(Cmd;clients) a between e1 and e')
51. (z[c1 / cs].z = c)
52. ||cs|| = ||L||
53. no_repeats(Id;L)
54. <cs, L> rsc4_QuorumState(Cmd) <a, b3>(e')
55. no_repeats(Id;L)
56. ||L|| = ||cs||
57. i:||L||. (e:E. (e loc e' <<<a, b3>, cs[i]>, L[i]> rsc4_vote'base(Cmd)(e)))
58. vtr : Id
59. vtr = lastloc
60. e'@0 : E
61. (e'@0 < e')
62. <loc(e'), make-Msg(``rsc4 vote``; Cmd Id;<<<n, b5>, c1>, lastloc>)> rsc4_Main(e'@0)
63. e'@0:E. <loc(e'), make-Msg(``rsc4 vote``; Cmd Id;<<<n, b3>, c>, vtr>)> rsc4_Main(e'@0)
vtr locs
1. Cmd : Type
2. Cmd \mmember{} ValueAllType
3. valueall-type(Cmd)
4. cmdeq : EqDecider(Cmd)
5. locs : bag(Id)
6. clients : bag(Id)
7. coeff : \mBbbZ{}
8. flrs : \mBbbZ{}
9. es : EO'
10. StandardAssumptions(rsc4\_Main) es
11. e : E
12. c : Cmd
13. n : \mBbbZ{}
14. <n, c> \mmember{} rsc4\_decided'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. e2 : \{e1:E| e1 \mleq{}loc e' \}
29. b3 : \mBbbZ{}
30. (no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
31. b5 : \mBbbZ{}
32. c1 : Cmd
33. lastloc : Id
34. <<<n, b5>, c1>, lastloc> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e')
35. cs : Cmd List
36. ||cs|| = (coeff * flrs)
37. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
38. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
39. L : Id List
40. <cs, L> \mmember{} Memory-class(rsc4\_add\_to\_quorum(Cmd) <a, b3>rsc4\_init()
<[], []>rsc4\_vote'base(Cmd))(e')
41. a = n
42. b3 = b5
43. \mneg{}(lastloc \mmember{} L)
44. b1 : Cmd
45. True
46. <<a, b3>, b1> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e2)
\mvee{} (\mexists{}b5:Id. <<<a, b3>, b1>, b5> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e2))
47. b4 : \mBbbZ{}
48. b4 \mmember{} Memory-class(rsc4\_update\_round(Cmd) a;rsc4\_init() 0;rsc4\_RoundInfo(Cmd))(e2)
49. b4 < b3
50. (no rsc4\_Notify(Cmd;clients) a between e1 and e')
51. (\mforall{}z\mmember{}[c1 / cs].z = c)
52. ||cs|| = ||L||
53. no\_repeats(Id;L)
54. <cs, L> \mmember{} rsc4\_QuorumState(Cmd) <a, b3>(e')
55. no\_repeats(Id;L)
56. ||L|| = ||cs||
57. \mforall{}i:\mBbbN{}||L||. (\mdownarrow{}\mexists{}e:E. (e \mleq{}loc e' \mwedge{} <<<a, b3>, cs[i]>, L[i]> \mmember{} rsc4\_vote'base(Cmd)(e)))
58. vtr : Id
59. vtr = lastloc
\mvdash{} (\mdownarrow{}\mexists{}e'@0:E
<loc(e'), make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, b3>, c>, vtr>)> \mmember{} rsc4\_Main(e'@0))
\mwedge{} vtr \mdownarrow{}\mmember{} locs
By
((UseMessageConstraint 34 THENA MaAuto) THEN TrySquashExRepD (-1) THEN MaAuto)
Home
Index