---

Step * of Lemma rsc4-agreement-property

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff:{2...}]. [flrs:]. [es:EO'].
  ((StandardAssumptions(rsc4_Main) es)
   bag-no-repeats(Id;locs)
   (bag-size(locs) = ((coeff * flrs) + flrs + 1))
   any v1,v2 from rsc4_decided'base(Cmd) satisfy
     ((fst(v1)) = (fst(v2)))  ((snd(v1)) = (snd(v2))))
BY
{ (Unfold `vatype` 0
   THEN Auto
   THEN D 0
   THEN Auto
   THEN D -5
   THEN D -4
   THEN All Reduce
   THEN (HypSubst' -1 -3 THENA Auto)
   THEN Thin (-1)
   THEN Thin (-6)
   THEN RenameVar `c1' (-5)
   THEN RenameVar `c2' (-3)
   THEN RenameVar `n' (-4)
   THEN RepeatFor 2 ((FLemma `rsc4-decided-property` [8;-2] THENA Auto))
   THEN SquashExRepD) }

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

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[locs,clients:bag(Id)].  \mforall{}[coeff:\{2...\}].  \mforall{}[flrs:\mBbbN{}].
\mforall{}[es:EO'].
    ((StandardAssumptions(rsc4\_Main)  es)
    {}\mRightarrow{}  bag-no-repeats(Id;locs)
    {}\mRightarrow{}  (bag-size(locs)  =  ((coeff  *  flrs)  +  flrs  +  1))
    {}\mRightarrow{}  any  v1,v2  from  rsc4\_decided'base(Cmd)  satisfy
          ((fst(v1))  =  (fst(v2)))  {}\mRightarrow{}  ((snd(v1))  =  (snd(v2))))


By

---

(Unfold  `vatype`  0
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  D  -5
  THEN  D  -4
  THEN  All  Reduce
  THEN  (HypSubst'  -1  -3  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Thin  (-6)
  THEN  RenameVar  `c1'  (-5)
  THEN  RenameVar  `c2'  (-3)
  THEN  RenameVar  `n'  (-4)
  THEN  RepeatFor  2  ((FLemma  `rsc4-decided-property`  [8;-2]  THENA  Auto))
  THEN  SquashExRepD)



Home Index