Step
*
1
1
of Lemma
rsc4-retry-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. c2 : Cmd
13. n : 
14. r :
15. <<n, r + 1>, c2> rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e') 
locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 
loc e' }
21. a :
22. a2 :
23. b2 : List
24. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a) 
(a b2)
26. c1 : Cmd
27. True
28. <a, c1> Base([propose]; 
Cmd)(e1)
(
b1:. b3:Id. <<<a, b1>, c1>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
29. b1 :
30. (r + 1) = (b1 + 1)
31. cmd : Cmd
32. loc : Id
33. <<<n, b1>, cmd>, loc> Base(``rsc4 vote``; Cmd Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. 
((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
37. c2 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
38. L : Id List
39. <cs, L> rsc4_QuorumState(Cmd) <a, 0>(e')
40. a = n
41. 0 = b1
42. (loc L)
43. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
44. no_repeats(Id;L)
45. ||L|| = ||cs||
46. 
i:||L||. (e:E. (e loc e' 
<<<a, 0>, cs[i]>, L[i]> rsc4_vote'base(Cmd)(e)))
47. 0 (coeff * flrs)
48. i : ||L|| + 1
49. i:||L||. (e:E. (e loc e' <<<a, 0>, cs[i]>, L[i]> Base(``rsc4 vote``; Cmd Id)(e)))
e'@0:E
<loc(e'), make-Msg(``rsc4 vote``; Cmd Id;<<<n, r>, [cmd / cs][i]>, [loc / L][i]>)> rsc4_Main(e'@0)
BY
{ (Thin (-4)
THEN CaseNat 0 `i'
THEN Reduce 0
THEN Try (((RWO "select_cons_tl" 0 THENA MaAuto) THEN ((InstHyp [
i - 1
] (-2)
THENM SqExRepD) THENA Auto)))) }
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. c2 : Cmd
13. n :
14. r :
15. <<n, r + 1>, c2> rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e') locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 loc e' }
21. a :
22. a2 :
23. b2 : List
24. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a) (a b2)
26. c1 : Cmd
27. True
28. <a, c1> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, c1>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
29. b1 :
30. (r + 1) = (b1 + 1)
31. cmd : Cmd
32. loc : Id
33. <<<n, b1>, cmd>, loc> Base(``rsc4 vote``; Cmd Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
37. c2 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
38. L : Id List
39. <cs, L> rsc4_QuorumState(Cmd) <a, 0>(e')
40. a = n
41. 0 = b1
42. (loc L)
43. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
44. no_repeats(Id;L)
45. ||L|| = ||cs||
46. 0 (coeff * flrs)
47. i : ||L|| + 1
48. i:||L||. (e:E. (e loc e' <<<a, 0>, cs[i]>, L[i]> Base(``rsc4 vote``; Cmd Id)(e)))
49. i = 0
e'@0:E. <loc(e'), make-Msg(``rsc4 vote``; Cmd Id;<<<n, r>, cmd>, loc>)> 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. c2 : Cmd
13. n :
14. r :
15. <<n, r + 1>, c2> rsc4_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e') locs
19. loc(e) = loc(e')
20. e1 : {e1:E| e1 loc e' }
21. a :
22. a2 :
23. b2 : List
24. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
25. (a2 < a) (a b2)
26. c1 : Cmd
27. True
28. <a, c1> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, c1>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
29. b1 :
30. (r + 1) = (b1 + 1)
31. cmd : Cmd
32. loc : Id
33. <<<n, b1>, cmd>, loc> Base(``rsc4 vote``; Cmd Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
37. c2 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
38. L : Id List
39. <cs, L> rsc4_QuorumState(Cmd) <a, 0>(e')
40. a = n
41. 0 = b1
42. (loc L)
43. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
44. no_repeats(Id;L)
45. ||L|| = ||cs||
46. 0 (coeff * flrs)
47. i : ||L|| + 1
48. i:||L||. (e:E. (e loc e' <<<a, 0>, cs[i]>, L[i]> Base(``rsc4 vote``; Cmd Id)(e)))
49. (i = 0)
50. e2 : E
51. e2 loc e'
52. <<<a, 0>, cs[i - 1]>, L[i - 1]> Base(``rsc4 vote``; Cmd Id)(e2)
e'@0:E. <loc(e'), make-Msg(``rsc4 vote``; Cmd Id;<<<n, r>, cs[i - 1]>, L[i - 1]>)> rsc4_Main(e'@0)
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 : \mBbbN{}
8. flrs : \mBbbN{}
9. es : EO'
10. StandardAssumptions(rsc4\_Main) es
11. e : E
12. c2 : Cmd
13. n : \mBbbZ{}
14. r : \mBbbZ{}
15. <<n, r + 1>, c2> \mmember{} rsc4\_retry'base(Cmd)(e)
16. e' : E
17. (e' < e)
18. loc(e') \mdownarrow{}\mmember{} locs
19. loc(e) = loc(e')
20. e1 : \{e1:E| e1 \mleq{}loc e' \}
21. a : \mBbbZ{}
22. a2 : \mBbbZ{}
23. b2 : \mBbbZ{} List
24. <a2, b2> \mmember{} Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init() ɘ, []>rsc4\_Proposal(Cmd))(e1)
25. (a2 < a) \mvee{} (a \mmember{} b2)
26. c1 : Cmd
27. True
28. <a, c1> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e1)
\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, c1>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e1))
29. b1 : \mBbbZ{}
30. (r + 1) = (b1 + 1)
31. cmd : Cmd
32. loc : Id
33. <<<n, b1>, cmd>, loc> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e')
34. cs : Cmd List
35. ||cs|| = (coeff * flrs)
36. \mneg{}((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
37. c2 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
38. L : Id List
39. <cs, L> \mmember{} rsc4\_QuorumState(Cmd) <a, 0>(e')
40. a = n
41. 0 = b1
42. \mneg{}(loc \mmember{} L)
43. (no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
44. no\_repeats(Id;L)
45. ||L|| = ||cs||
46. \mforall{}i:\mBbbN{}||L||. (\mdownarrow{}\mexists{}e:E. (e \mleq{}loc e' \mwedge{} <<<a, 0>, cs[i]>, L[i]> \mmember{} rsc4\_vote'base(Cmd)(e)))
47. 0 \mleq{} (coeff * flrs)
48. i : \mBbbN{}||L|| + 1
49. \mforall{}i:\mBbbN{}||L||
(\mdownarrow{}\mexists{}e:E. (e \mleq{}loc e' \mwedge{} <<<a, 0>, cs[i]>, L[i]> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)))
\mvdash{} \mdownarrow{}\mexists{}e'@0:E
<loc(e'), make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, r>, [cmd / cs][i]>, [loc / L][i]>)> \mmember{}
rsc4\_Main(e'@0)
By
(Thin (-4)
THEN CaseNat 0 `i'
THEN Reduce 0
THEN Try (((RWO "select\_cons\_tl" 0 THENA MaAuto)
THEN ((InstHyp [\mkleeneopen{}i - 1\mkleeneclose{}] (-2)\mcdot{} THENM SqExRepD) THENA Auto)
)))
Home
Index