Step
*
1
2
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)
k:. e':E. x,y:Id. c:Cmd.
(<x, make-Msg(``rsc4 vote``; Cmd Id;<<<n, (r1 + 1) + k>, c>, y>)> rsc4_Main(e') 
(c = c1))
BY
{ ((CompleteInductionOnNat THEN VrCausalInd'
)
THEN MaAuto
THEN (RWO "rsc4-vote" (-1) THENA MaAuto)
THEN SquashExRepD
THEN (D (-3) THEN Auto')
THEN SquashExRepD
THEN D -5
THEN SquashExRepD
THEN AllHyps h.(Fold `rsc4_retry\'base` h
THEN (Subst 
(r1 + 1) + k ~ (r1 + k) + 1
h THEN Auto)
THEN (FLemma `rsc4-retry-property` [8;h] THENA Auto)
THEN SquashExRepD) ) }
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))))
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. b5 : Id
46. <<<n, (r1 + 1) + k>, c>, b5> Base(``rsc4 vote``; Cmd Id)(e4)
47. e' = e4
48. (no rsc4_Notify(Cmd;clients) n between e3 and e')
49. True
50. <n, b> Base([propose]; Cmd)(e3)
(b1:. b3:Id. <<<n, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e3))
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)
\mvdash{} \mforall{}k:\mBbbN{}. \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) + k>, c>, y>)> \mmember{} rsc4\_Main(e')
{}\mRightarrow{} (c = c1))
By
((CompleteInductionOnNat THEN VrCausalInd'\mcdot{})
THEN MaAuto
THEN (RWO "rsc4-vote" (-1) THENA MaAuto)
THEN SquashExRepD
THEN (D (-3) THEN Auto')
THEN SquashExRepD
THEN D -5
THEN SquashExRepD
THEN AllHyps h.(Fold `rsc4\_retry\mbackslash{}'base` h
THEN (Subst \mkleeneopen{}(r1 + 1) + k \msim{} (r1 + k) + 1\mkleeneclose{} h\mcdot{} THEN Auto)
THEN (FLemma `rsc4-retry-property` [8;h] THENA Auto)
THEN SquashExRepD) \mcdot{})\mcdot{}
Home
Index