---

Step * of Lemma rsc4-decided-property

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff,flrs:]. [es:EO'].
  ((StandardAssumptions(rsc4_Main) es)
   (e:E. c:Cmd. n:.
        (<n, c>  rsc4_decided'base(Cmd)(e)
         (x:Id
              rnd:
               L:Id List
                ((no_repeats(Id;L)  (||L|| = ((coeff * flrs) + 1)))
                 (vtrL.(e':E. <x, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, rnd>, c>, vtr>)>  rsc4_Main(e'))
                        vtr  locs))))))
BY
{ (Unfold `vatype` 0
   THEN (Auto THEN AllHyps h.DVaType h )
   THEN (UseMessageConstraint (-1) THENA MaAuto)
   THEN (RWO "rsc4-decided" (-1) THENA MaAuto)
   THEN SquashExRepD
   THEN D (-1)
   THEN SquashExRepD
   THEN RenameTo `cs' `a3'
   THEN ((RenameTo `c1' `b6' ORELSE RenameTo `c1' `b3') THEN (RenameTo `L' `b7' ORELSE RenameTo `L' `b4'))
   THEN (InstLemma `poss-maj-unanimous` [Cmd;cmdeq;[c1 / cs];c1;c]
         THENA Complete ((Auto
                          THEN (RW (AddrC [2] (LemmaC `pair-eta`)) 0 THENA MaAuto)
                          THEN EqCD
                          THEN Auto
                          THEN Reduce 0
                          THEN Auto
                          THEN All Thin
                          THEN GenConclAtAddr [2;1]
                          THEN Auto'))
         )
   THEN Assert (||cs|| = ||L||)  no_repeats(Id;L)
   THEN Try (RenameTo `lastloc' `b3@0')) }

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. 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. (rsc4_newvote(Cmd) <a, 0> <<<n, b1>, c1>, lastloc> <cs, L>)
39. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
40. (z[c1 / cs].z = c)
 (||cs|| = ||L||)  no_repeats(Id;L)

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. 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. (rsc4_newvote(Cmd) <a, 0> <<<n, b1>, c1>, lastloc> <cs, L>)
39. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e1 and e')
40. (z[c1 / cs].z = c)
41. (||cs|| = ||L||)  no_repeats(Id;L)
 x:Id
    rnd:
     L:Id List
      ((no_repeats(Id;L)  (||L|| = ((coeff * flrs) + 1)))
       (vtrL.(e':E. <x, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, rnd>, c>, vtr>)>  rsc4_Main(e'))
              vtr  locs))

3
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. e2 : {e1:E| e1 loc e' } 
29. b3 : 
30. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
31. b5 : 
32. c1 : Cmd
33. lastloc : Id
34. <<<n, b5>, c1>, lastloc>  Base(``rsc4 vote``;    Cmd  Id)(e')
35. cs : Cmd List
36. ||cs|| = (coeff * flrs)
37. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
38. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
39. L : Id List
40. <cs, L>  Memory-class(rsc4_add_to_quorum(Cmd) <a, b3>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
41. (rsc4_newvote(Cmd) <a, b3> <<<n, b5>, c1>, lastloc> <cs, L>)
42. b1 : Cmd
43. True
44. <<a, b3>, b1>  Base(``rsc4 retry``;    Cmd)(e2)
 (b5:Id. <<<a, b3>, b1>, b5>  Base(``rsc4 vote``;    Cmd  Id)(e2))
45. b4 : 
46. b4  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
47. b4 < b3
48. (no rsc4_Notify(Cmd;clients) a between e1 and e')
49. (z[c1 / cs].z = c)
 (||cs|| = ||L||)  no_repeats(Id;L)

4
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. e2 : {e1:E| e1 loc e' } 
29. b3 : 
30. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
31. b5 : 
32. c1 : Cmd
33. lastloc : Id
34. <<<n, b5>, c1>, lastloc>  Base(``rsc4 vote``;    Cmd  Id)(e')
35. cs : Cmd List
36. ||cs|| = (coeff * flrs)
37. (fst(poss-maj(cmdeq;[c1 / cs];c1))) = ((coeff * flrs) + 1)
38. c = (snd(poss-maj(cmdeq;[c1 / cs];c1)))
39. L : Id List
40. <cs, L>  Memory-class(rsc4_add_to_quorum(Cmd) <a, b3>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e')
41. (rsc4_newvote(Cmd) <a, b3> <<<n, b5>, c1>, lastloc> <cs, L>)
42. b1 : Cmd
43. True
44. <<a, b3>, b1>  Base(``rsc4 retry``;    Cmd)(e2)
 (b5:Id. <<<a, b3>, b1>, b5>  Base(``rsc4 vote``;    Cmd  Id)(e2))
45. b4 : 
46. b4  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
47. b4 < b3
48. (no rsc4_Notify(Cmd;clients) a between e1 and e')
49. (z[c1 / cs].z = c)
50. (||cs|| = ||L||)  no_repeats(Id;L)
 x:Id
    rnd:
     L:Id List
      ((no_repeats(Id;L)  (||L|| = ((coeff * flrs) + 1)))
       (vtrL.(e':E. <x, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, rnd>, c>, vtr>)>  rsc4_Main(e'))
              vtr  locs))

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[locs,clients:bag(Id)].  \mforall{}[coeff,flrs:\mBbbZ{}].  \mforall{}[es:EO'].
    ((StandardAssumptions(rsc4\_Main)  es)
    {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}c:Cmd.  \mforall{}n:\mBbbZ{}.
                (<n,  c>  \mmember{}  rsc4\_decided'base(Cmd)(e)
                {}\mRightarrow{}  (\mdownarrow{}\mexists{}x:Id
                            \mexists{}rnd:\mBbbN{}
                              \mexists{}L:Id  List
                                ((no\_repeats(Id;L)  \mwedge{}  (||L||  =  ((coeff  *  flrs)  +  1)))
                                \mwedge{}  (\mforall{}vtr\mmember{}L.(\mdownarrow{}\mexists{}e':E
                                                          <x,  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<n,  rnd>,  c>,  vtr>)>  \mmember{}
                                                            rsc4\_Main(e'))
                                              \mwedge{}  vtr  \mdownarrow{}\mmember{}  locs))))))


By

---

(Unfold  `vatype`  0
  THEN  (Auto  THEN  AllHyps  h.DVaType  h  )
  THEN  (UseMessageConstraint  (-1)  THENA  MaAuto)
  THEN  (RWO  "rsc4-decided"  (-1)  THENA  MaAuto)
  THEN  SquashExRepD
  THEN  D  (-1)
  THEN  SquashExRepD
  THEN  RenameTo  `cs'  `a3'\mcdot{}
  THEN  ((RenameTo  `c1'  `b6'  ORELSE  RenameTo  `c1'  `b3')
              THEN  (RenameTo  `L'  `b7'\mcdot{}  ORELSE  RenameTo  `L'  `b4')
              )
  THEN  (InstLemma  `poss-maj-unanimous`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}cmdeq\mkleeneclose{};\mkleeneopen{}[c1  /  cs]\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
              THENA  Complete  ((Auto
                                                THEN  (RW  (AddrC  [2]  (LemmaC  `pair-eta`))  0  THENA  MaAuto)\mcdot{}
                                                THEN  EqCD
                                                THEN  Auto
                                                THEN  Reduce  0
                                                THEN  Auto
                                                THEN  All  Thin
                                                THEN  GenConclAtAddr  [2;1]
                                                THEN  Auto'))
              )
  THEN  Assert  \mkleeneopen{}(||cs||  =  ||L||)  \mwedge{}  no\_repeats(Id;L)\mkleeneclose{}\mcdot{}
  THEN  Try  (RenameTo  `lastloc'  `b3@0'))



Home Index