---

Step * 1 2 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. c2 : Cmd
16. <n, c1>  rsc4_decided'base(Cmd)(e1)
17. <n, c2>  rsc4_decided'base(Cmd)(e2)
18. x1 : Id
19. r1 : 
20. L1 : Id List
21. no_repeats(Id;L1)
22. ||L1|| = ((coeff * flrs) + 1)
23. (vtrL1.(e':E. <x1, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, r1>, c1>, vtr>)>  rsc4_Main(e'))
          vtr  locs)
24. x : Id
25. rnd : 
26. L : Id List
27. no_repeats(Id;L)
28. ||L|| = ((coeff * flrs) + 1)
29. (vtrL.(e':E. <x, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, rnd>, c2>, vtr>)>  rsc4_Main(e'))  vtr  locs)
30. (r1 = rnd)
31. 0  (coeff * flrs)
32. r1 < rnd
 c1 = c2
BY
{ Assert 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)) }

1
.....assertion..... 
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. c2 : Cmd
16. <n, c1>  rsc4_decided'base(Cmd)(e1)
17. <n, c2>  rsc4_decided'base(Cmd)(e2)
18. x1 : Id
19. r1 : 
20. L1 : Id List
21. no_repeats(Id;L1)
22. ||L1|| = ((coeff * flrs) + 1)
23. (vtrL1.(e':E. <x1, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, r1>, c1>, vtr>)>  rsc4_Main(e'))
          vtr  locs)
24. x : Id
25. rnd : 
26. L : Id List
27. no_repeats(Id;L)
28. ||L|| = ((coeff * flrs) + 1)
29. (vtrL.(e':E. <x, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, rnd>, c2>, vtr>)>  rsc4_Main(e'))  vtr  locs)
30. (r1 = rnd)
31. 0  (coeff * flrs)
32. r1 < rnd
 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))

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. c2 : Cmd
16. <n, c1>  rsc4_decided'base(Cmd)(e1)
17. <n, c2>  rsc4_decided'base(Cmd)(e2)
18. x1 : Id
19. r1 : 
20. L1 : Id List
21. no_repeats(Id;L1)
22. ||L1|| = ((coeff * flrs) + 1)
23. (vtrL1.(e':E. <x1, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, r1>, c1>, vtr>)>  rsc4_Main(e'))
          vtr  locs)
24. x : Id
25. rnd : 
26. L : Id List
27. no_repeats(Id;L)
28. ||L|| = ((coeff * flrs) + 1)
29. (vtrL.(e':E. <x, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, rnd>, c2>, vtr>)>  rsc4_Main(e'))  vtr  locs)
30. (r1 = rnd)
31. 0  (coeff * flrs)
32. r1 < rnd
33. 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))
 c1 = c2

---

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.  c2  :  Cmd
16.  <n,  c1>  \mmember{}  rsc4\_decided'base(Cmd)(e1)
17.  <n,  c2>  \mmember{}  rsc4\_decided'base(Cmd)(e2)
18.  x1  :  Id
19.  r1  :  \mBbbN{}
20.  L1  :  Id  List
21.  no\_repeats(Id;L1)
22.  ||L1||  =  ((coeff  *  flrs)  +  1)
23.  (\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)
24.  x  :  Id
25.  rnd  :  \mBbbN{}
26.  L  :  Id  List
27.  no\_repeats(Id;L)
28.  ||L||  =  ((coeff  *  flrs)  +  1)
29.  (\mforall{}vtr\mmember{}L.(\mdownarrow{}\mexists{}e':E
                              <x,  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<n,  rnd>,  c2>,  vtr>)>  \mmember{}  rsc4\_Main(e'))
                  \mwedge{}  vtr  \mdownarrow{}\mmember{}  locs)
30.  \mneg{}(r1  =  rnd)
31.  0  \mleq{}  (coeff  *  flrs)
32.  r1  <  rnd
\mvdash{}  c1  =  c2


By

---

Assert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}



Home Index