---

Step * of Lemma rsc4-agreement

[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 Base([notify];  Cmd) satisfy
     ((fst(v1)) = (fst(v2)))  ((snd(v1)) = (snd(v2))))
BY
{ (Auto
   THEN MaAuto
   THEN (InstLemma `rsc4-agreement-property`  [Cmd;cmdeq;locs;clients;coeff;flrs;es] THENA Auto)
   THEN Unfold `vatype` 1
   THEN ParallelLast
   THEN MaAuto
   THEN AllHyps h.DProduct h 
   THEN AllHyps h.((UseMessageConstraint h THENM RWO "rsc4-notify" (-1)) THENA MaAuto) 
   THEN ExRepD
   THEN OnMaybeHyp 11 (\h. ((InstHyp [e3;e'] h THENA Auto)
                            THEN (BHyp (-1) THEN Auto)
                            THEN Unfold `rsc4_decided\'base` 0
                            THEN Complete (Auto)))) }

---

\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  Base([notify];\mBbbZ{}  \mtimes{}  Cmd)  satisfy
          ((fst(v1))  =  (fst(v2)))  {}\mRightarrow{}  ((snd(v1))  =  (snd(v2))))


By

---

(Auto
  THEN  MaAuto
  THEN  (InstLemma  `rsc4-agreement-property` 
              [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}cmdeq\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}clients\mkleeneclose{};\mkleeneopen{}coeff\mkleeneclose{};\mkleeneopen{}flrs\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Unfold  `vatype`  1
  THEN  ParallelLast
  THEN  MaAuto
  THEN  AllHyps  h.DProduct  h\mcdot{} 
  THEN  AllHyps  h.((UseMessageConstraint  h  THENM  RWO  "rsc4-notify"  (-1))  THENA  MaAuto) 
  THEN  ExRepD
  THEN  OnMaybeHyp  11  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}e3\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                                    THEN  (BHyp  (-1)  THEN  Auto)
                                                    THEN  Unfold  `rsc4\_decided\mbackslash{}'base`  0
                                                    THEN  Complete  (Auto))))



Home Index