---

Step * 2 1 1 2 1 2 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. b1 : 
29. c1 : Cmd
30. lastloc : Id
31. <<<n, b1>, c1>, lastloc>  Base(``rsc4 vote``;    Cmd  Id)(e')
32. cs : Cmd List
33. ||cs|| = (coeff * flrs)
34. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
35. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
36. L : Id List
37. <cs, L>  Memory-class(rsc4_add_to_quorum(Cmd) <a, 0>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
38. a = n
39. 0 = b1
40. (lastloc  L)
41. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
42. c1 = c
43. z:Cmd. ((z  cs)  (z = c))
44. ||cs|| = ||L||
45. no_repeats(Id;L)
46. <cs, L>  rsc4_QuorumState(Cmd) <a, 0>(e')
47. no_repeats(Id;L)
48. ||L|| = ||cs||
49. i:||L||. (e:E. (e loc e'   <<<a, 0>, cs[i]>, L[i]>  rsc4_vote'base(Cmd)(e)))
50. vtr : Id
51. i : 
52. i < ||L||
53. vtr = L[i]
54. e2 : E
55. e2 loc e' 
56. <<<n, 0>, c>, vtr>  rsc4_vote'base(Cmd)(e2)
57. make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, 0>, c>, vtr>)
= make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, 0>, c>, vtr>)
 (msg-header(info(e2)) = [notify])  (msg-header(info(e2))  [``rsc4 decided``; ``rsc4 retry``; ``rsc4 vote``])
BY
{ (RepeatFor 3 (((OrRight THENA (MaAuto THEN Try (Fold `name` 0) THEN BLemma `msg-header_wf` THEN MaAuto))
                 THEN GenListD 0
                 ))
   THEN (OrLeft THENA (MaAuto THEN Try (Fold `name` 0) THEN BLemma `msg-header_wf` THEN MaAuto))
   THEN MaUseClassRel'' (-2)
   THEN Unfold `es-header` (-4)
   THEN (RWO "eo-forward-info" (-4) THENA Auto)
   THEN Try (Fold `msg-header` (-4))
   THEN Auto) }

---

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.  b1  :  \mBbbZ{}
29.  c1  :  Cmd
30.  lastloc  :  Id
31.  <<<n,  b1>,  c1>,  lastloc>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e')
32.  cs  :  Cmd  List
33.  ||cs||  =  (coeff  *  flrs)
34.  (fst(poss-maj(cmdeq;[c1  /  cs];c1)))  =  ((coeff  *  flrs)  +  1)
35.  c  =  (snd(poss-maj(cmdeq;[c1  /  cs];c1)))
36.  L  :  Id  List
37.  <cs,  L>  \mmember{}  Memory-class(rsc4\_add\_to\_quorum(Cmd)  <a,  0>rsc4\_init()  <[],  []>rsc4\_vote'base(Cmd))(
                            e')
38.  a  =  n
39.  0  =  b1
40.  \mneg{}(lastloc  \mmember{}  L)
41.  (no  rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  0>  between  e1  and  e')
42.  c1  =  c
43.  \mforall{}z:Cmd.  ((z  \mmember{}  cs)  {}\mRightarrow{}  (z  =  c))
44.  ||cs||  =  ||L||
45.  no\_repeats(Id;L)
46.  <cs,  L>  \mmember{}  rsc4\_QuorumState(Cmd)  <a,  0>(e')
47.  no\_repeats(Id;L)
48.  ||L||  =  ||cs||
49.  \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)))
50.  vtr  :  Id
51.  i  :  \mBbbN{}
52.  i  <  ||L||
53.  vtr  =  L[i]
54.  e2  :  E
55.  e2  \mleq{}loc  e' 
56.  <<<n,  0>,  c>,  vtr>  \mmember{}  rsc4\_vote'base(Cmd)(e2)
57.  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<n,  0>,  c>,  vtr>)
=  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<n,  0>,  c>,  vtr>)
\mvdash{}  (msg-header(info(e2))  =  [notify])
\mvee{}  (msg-header(info(e2))  \mmember{}  [``rsc4  decided``;  ``rsc4  retry``;  ``rsc4  vote``])


By

---

(RepeatFor  3  (((OrRight
                                THENA  (MaAuto  THEN  Try  (Fold  `name`  0)  THEN  BLemma  `msg-header\_wf`  THEN  MaAuto)
                                )
                              THEN  GenListD  0
                              ))
  THEN  (OrLeft  THENA  (MaAuto  THEN  Try  (Fold  `name`  0)  THEN  BLemma  `msg-header\_wf`  THEN  MaAuto))
  THEN  MaUseClassRel''  (-2)
  THEN  Unfold  `es-header`  (-4)
  THEN  (RWO  "eo-forward-info"  (-4)  THENA  Auto)
  THEN  Try  (Fold  `msg-header`  (-4))
  THEN  Auto)



Home Index