Step
*
1
2
1
1
1
1
of Lemma
rsc4-agreement-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. bag-no-repeats(Id;locs)
10. bag-size(locs) = ((coeff * flrs) + flrs + 1)
11. e1 : E
12. e2 : E
13. c1 : Cmd
14. n : 
15. <n, c1> 
rsc4_decided'base(Cmd)(e1)
16. x1 : Id
17. r1 :
18. L1 : Id List
19. no_repeats(Id;L1)
20. ||L1|| = ((coeff * flrs) + 1)
21. (
vtrL1.(
e':E. <x1, make-Msg(``rsc4 vote``; 
Cmd Id;<<<n, r1>, c1>, vtr>)> rsc4_Main(e'))
vtr locs)
22. x : Id
23. 0 
(coeff * flrs)
24. k :
25. k1:
((k1 < k)
(e':E. x,y:Id. c:Cmd.
(<x, make-Msg(``rsc4 vote``; Cmd Id;<<<n, (r1 + 1) + k1>, c>, y>)> rsc4_Main(e') (c = c1))))
26. e' : E
27. e3:E
((e3 < e')
(x,y:Id. c:Cmd.
(<x, make-Msg(``rsc4 vote``; Cmd Id;<<<n, (r1 + 1) + k>, c>, y>)> rsc4_Main(e3) (c = c1))))
28. x2 : Id
29. y : Id
30. c : Cmd
31. loc(e') locs
32. x2 locs
33. y = loc(e')
34. e3 : {e1:E| e1 loc e' }
35. a2 :
36. b2 : List
37. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e3)
38. (a2 < n) 
(n b2)
39. b : Cmd
40. e4 : {e1:E| e1 loc e' }
41. b4 :
42. b4 Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e4)
43. b4 < ((r1 + 1) + k)
44. True
45. <<n, (r1 + k) + 1>, c> rsc4_retry'base(Cmd)(e4)
46. e' = e4
47. (no rsc4_Notify(Cmd;clients) n between e3 and e')
48. True
49. <n, b> Base([propose]; Cmd)(e3)
(b1:. b3:Id. <<<n, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e3))
50. x3 : Id
51. cs : Cmd List
52. L : Id List
53. no_repeats(Id;L)
54. ||L|| = ((coeff * flrs) + 1)
55. ||cs|| = ||L||
56. i:||L||
((e':E. <x3, make-Msg(``rsc4 vote``; Cmd Id;<<<n, r1 + k>, cs[i]>, L[i]>)> rsc4_Main(e'))
L[i] locs)
57. c = (snd(poss-maj(cmdeq;cs;hd(cs))))
c = c1
BY
{ (Decide 
0 < k
THENA Auto) }
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. bag-no-repeats(Id;locs)
10. bag-size(locs) = ((coeff * flrs) + flrs + 1)
11. e1 : E
12. e2 : E
13. c1 : Cmd
14. n :
15. <n, c1> rsc4_decided'base(Cmd)(e1)
16. x1 : Id
17. r1 :
18. L1 : Id List
19. no_repeats(Id;L1)
20. ||L1|| = ((coeff * flrs) + 1)
21. (vtrL1.(e':E. <x1, make-Msg(``rsc4 vote``; Cmd Id;<<<n, r1>, c1>, vtr>)> rsc4_Main(e'))
vtr locs)
22. x : Id
23. 0 (coeff * flrs)
24. k :
25. k1:
((k1 < k)
(e':E. x,y:Id. c:Cmd.
(<x, make-Msg(``rsc4 vote``; Cmd Id;<<<n, (r1 + 1) + k1>, c>, y>)> rsc4_Main(e') (c = c1))))
26. e' : E
27. e3:E
((e3 < e')
(x,y:Id. c:Cmd.
(<x, make-Msg(``rsc4 vote``; Cmd Id;<<<n, (r1 + 1) + k>, c>, y>)> rsc4_Main(e3) (c = c1))))
28. x2 : Id
29. y : Id
30. c : Cmd
31. loc(e') locs
32. x2 locs
33. y = loc(e')
34. e3 : {e1:E| e1 loc e' }
35. a2 :
36. b2 : List
37. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e3)
38. (a2 < n) (n b2)
39. b : Cmd
40. e4 : {e1:E| e1 loc e' }
41. b4 :
42. b4 Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e4)
43. b4 < ((r1 + 1) + k)
44. True
45. <<n, (r1 + k) + 1>, c> rsc4_retry'base(Cmd)(e4)
46. e' = e4
47. (no rsc4_Notify(Cmd;clients) n between e3 and e')
48. True
49. <n, b> Base([propose]; Cmd)(e3)
(b1:. b3:Id. <<<n, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e3))
50. x3 : Id
51. cs : Cmd List
52. L : Id List
53. no_repeats(Id;L)
54. ||L|| = ((coeff * flrs) + 1)
55. ||cs|| = ||L||
56. i:||L||
((e':E. <x3, make-Msg(``rsc4 vote``; Cmd Id;<<<n, r1 + k>, cs[i]>, L[i]>)> rsc4_Main(e'))
L[i] locs)
57. c = (snd(poss-maj(cmdeq;cs;hd(cs))))
58. 0 < k
c = c1
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. bag-no-repeats(Id;locs)
10. bag-size(locs) = ((coeff * flrs) + flrs + 1)
11. e1 : E
12. e2 : E
13. c1 : Cmd
14. n :
15. <n, c1> rsc4_decided'base(Cmd)(e1)
16. x1 : Id
17. r1 :
18. L1 : Id List
19. no_repeats(Id;L1)
20. ||L1|| = ((coeff * flrs) + 1)
21. (vtrL1.(e':E. <x1, make-Msg(``rsc4 vote``; Cmd Id;<<<n, r1>, c1>, vtr>)> rsc4_Main(e'))
vtr locs)
22. x : Id
23. 0 (coeff * flrs)
24. k :
25. k1:
((k1 < k)
(e':E. x,y:Id. c:Cmd.
(<x, make-Msg(``rsc4 vote``; Cmd Id;<<<n, (r1 + 1) + k1>, c>, y>)> rsc4_Main(e') (c = c1))))
26. e' : E
27. e3:E
((e3 < e')
(x,y:Id. c:Cmd.
(<x, make-Msg(``rsc4 vote``; Cmd Id;<<<n, (r1 + 1) + k>, c>, y>)> rsc4_Main(e3) (c = c1))))
28. x2 : Id
29. y : Id
30. c : Cmd
31. loc(e') locs
32. x2 locs
33. y = loc(e')
34. e3 : {e1:E| e1 loc e' }
35. a2 :
36. b2 : List
37. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e3)
38. (a2 < n) (n b2)
39. b : Cmd
40. e4 : {e1:E| e1 loc e' }
41. b4 :
42. b4 Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e4)
43. b4 < ((r1 + 1) + k)
44. True
45. <<n, (r1 + k) + 1>, c> rsc4_retry'base(Cmd)(e4)
46. e' = e4
47. (no rsc4_Notify(Cmd;clients) n between e3 and e')
48. True
49. <n, b> Base([propose]; Cmd)(e3)
(b1:. b3:Id. <<<n, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e3))
50. x3 : Id
51. cs : Cmd List
52. L : Id List
53. no_repeats(Id;L)
54. ||L|| = ((coeff * flrs) + 1)
55. ||cs|| = ||L||
56. i:||L||
((e':E. <x3, make-Msg(``rsc4 vote``; Cmd Id;<<<n, r1 + k>, cs[i]>, L[i]>)> rsc4_Main(e'))
L[i] locs)
57. c = (snd(poss-maj(cmdeq;cs;hd(cs))))
58. 
(0 < k)
c = c1
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. bag-no-repeats(Id;locs)
10. bag-size(locs) = ((coeff * flrs) + flrs + 1)
11. e1 : E
12. e2 : E
13. c1 : Cmd
14. n : \mBbbZ{}
15. <n, c1> \mmember{} rsc4\_decided'base(Cmd)(e1)
16. x1 : Id
17. r1 : \mBbbN{}
18. L1 : Id List
19. no\_repeats(Id;L1)
20. ||L1|| = ((coeff * flrs) + 1)
21. (\mforall{}vtr\mmember{}L1.(\mdownarrow{}\mexists{}e':E
<x1, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, r1>, c1>, vtr>)> \mmember{} rsc4\_Main(e'))
\mwedge{} vtr \mdownarrow{}\mmember{} locs)
22. x : Id
23. 0 \mleq{} (coeff * flrs)
24. k : \mBbbN{}
25. \mforall{}k1:\mBbbN{}
((k1 < k)
{}\mRightarrow{} (\mforall{}e':E. \mforall{}x,y:Id. \mforall{}c:Cmd.
(<x, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, (r1 + 1) + k1>, c>, y>)> \mmember{}
rsc4\_Main(e')
{}\mRightarrow{} (c = c1))))
26. e' : E
27. \mforall{}e3:E
((e3 < e')
{}\mRightarrow{} (\mforall{}x,y:Id. \mforall{}c:Cmd.
(<x, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, (r1 + 1) + k>, c>, y>)> \mmember{}
rsc4\_Main(e3)
{}\mRightarrow{} (c = c1))))
28. x2 : Id
29. y : Id
30. c : Cmd
31. loc(e') \mdownarrow{}\mmember{} locs
32. x2 \mdownarrow{}\mmember{} locs
33. y = loc(e')
34. e3 : \{e1:E| e1 \mleq{}loc e' \}
35. a2 : \mBbbZ{}
36. b2 : \mBbbZ{} List
37. <a2, b2> \mmember{} Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init() ɘ, []>rsc4\_Proposal(Cmd))(e3)
38. (a2 < n) \mvee{} (n \mmember{} b2)
39. b : Cmd
40. e4 : \{e1:E| e1 \mleq{}loc e' \}
41. b4 : \mBbbZ{}
42. b4 \mmember{} Memory-class(rsc4\_update\_round(Cmd) n;rsc4\_init() 0;rsc4\_RoundInfo(Cmd))(e4)
43. b4 < ((r1 + 1) + k)
44. True
45. <<n, (r1 + k) + 1>, c> \mmember{} rsc4\_retry'base(Cmd)(e4)
46. e' = e4
47. (no rsc4\_Notify(Cmd;clients) n between e3 and e')
48. True
49. <n, b> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e3)
\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<n, b1>, b>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e3))
50. x3 : Id
51. cs : Cmd List
52. L : Id List
53. no\_repeats(Id;L)
54. ||L|| = ((coeff * flrs) + 1)
55. ||cs|| = ||L||
56. \mforall{}i:\mBbbN{}||L||
((\mdownarrow{}\mexists{}e':E
<x3, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, r1 + k>, cs[i]>, L[i]>)> \mmember{}
rsc4\_Main(e'))
\mwedge{} L[i] \mdownarrow{}\mmember{} locs)
57. c = (snd(poss-maj(cmdeq;cs;hd(cs))))
\mvdash{} c = c1
By
(Decide \mkleeneopen{}0 < k\mkleeneclose{}\mcdot{} THENA Auto)\mcdot{}
Home
Index