---

Step * 6 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. c3 : Cmd
13. n : 
14. r : 
15. <<n, r + 1>, c3>  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. c2 : Cmd
27. True
28. <a, c2>  Base([propose];  Cmd)(e1)
 (b1:. b3:Id. <<<a, b1>, c2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e1))
29. e2 : {e1:E| e1 loc e' } 
30. b3 : 
31. b6 : 
32. b6  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
33. b6 < b3
34. c1 : Cmd
35. True
36. <<a, b3>, c1>  Base(``rsc4 retry``;    Cmd)(e2)
 (b5@0:Id. <<<a, b3>, c1>, b5@0>  Base(``rsc4 vote``;    Cmd  Id)(e2))
37. b1 : 
38. (r + 1) = (b1 + 1)
39. cmd : Cmd
40. loc : Id
41. <<<n, b1>, cmd>, loc>  Base(``rsc4 vote``;    Cmd  Id)(e')
42. cs : Cmd List
43. ||cs|| = (coeff * flrs)
44. ((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
45. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
46. L : Id List
47. <cs, L>  rsc4_QuorumState(Cmd) <a, b3>(e')
48. a = n
49. b3 = b1
50. (loc  L)
51. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
52. (no rsc4_Notify(Cmd;clients) a between e1 and e')
53. no_repeats(Id;L)
54. ||L|| = ||cs||
55. i:||L||. (e:E. (e loc e'   <<<a, b3>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e)))
56. 0  (coeff * flrs)
57. L1 : Id List
58. no_repeats(Id;L1)
59. ||L1|| = ((coeff * flrs) + 1)
60. (||cs|| + 1) = ||L1||
61. i : ||L1||
62. e'@0 : E
 i < ||[cmd / cs]||
BY
{ (SqExRepD THEN RWW "rsc4-vote" (-1) THEN Auto THEN (Reduce 0 THEN MaAuto)) }

---

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.  c3  :  Cmd
13.  n  :  \mBbbZ{}
14.  r  :  \mBbbZ{}
15.  <<n,  r  +  1>,  c3>  \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.  c2  :  Cmd
27.  True
28.  <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))
29.  e2  :  \{e1:E|  e1  \mleq{}loc  e'  \} 
30.  b3  :  \mBbbZ{}
31.  b6  :  \mBbbZ{}
32.  b6  \mmember{}  Memory-class(rsc4\_update\_round(Cmd)  a;rsc4\_init()  0;rsc4\_RoundInfo(Cmd))(e2)
33.  b6  <  b3
34.  c1  :  Cmd
35.  True
36.  <<a,  b3>,  c1>  \mmember{}  Base(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e2)
\mvee{}  (\mexists{}b5@0:Id.  <<<a,  b3>,  c1>,  b5@0>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e2))
37.  b1  :  \mBbbZ{}
38.  (r  +  1)  =  (b1  +  1)
39.  cmd  :  Cmd
40.  loc  :  Id
41.  <<<n,  b1>,  cmd>,  loc>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e')
42.  cs  :  Cmd  List
43.  ||cs||  =  (coeff  *  flrs)
44.  \mneg{}((fst(poss-maj(cmdeq;[cmd  /  cs];cmd)))  =  ((coeff  *  flrs)  +  1))
45.  c3  =  (snd(poss-maj(cmdeq;[cmd  /  cs];cmd)))
46.  L  :  Id  List
47.  <cs,  L>  \mmember{}  rsc4\_QuorumState(Cmd)  <a,  b3>(e')
48.  a  =  n
49.  b3  =  b1
50.  \mneg{}(loc  \mmember{}  L)
51.  (no  rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  b3>  between  e2  and  e')
52.  (no  rsc4\_Notify(Cmd;clients)  a  between  e1  and  e')
53.  no\_repeats(Id;L)
54.  ||L||  =  ||cs||
55.  \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)))
56.  0  \mleq{}  (coeff  *  flrs)
57.  L1  :  Id  List
58.  no\_repeats(Id;L1)
59.  ||L1||  =  ((coeff  *  flrs)  +  1)
60.  (||cs||  +  1)  =  ||L1||
61.  i  :  \mBbbN{}||L1||
62.  e'@0  :  E
\mvdash{}  i  <  ||[cmd  /  cs]||


By

---

(SqExRepD  THEN  RWW  "rsc4-vote"  (-1)  THEN  Auto  THEN  (Reduce  0  THEN  MaAuto))\mcdot{}



Home Index