---

Step * 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)
 c1 = c2
BY
{ (Decide r1 = rnd THENA Auto) }

1
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
 c1 = c2

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)
 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)
\mvdash{}  c1  =  c2


By

---

(Decide  \mkleeneopen{}r1  =  rnd\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{}



Home Index