---

Step * of Lemma rsc4_quorum_invariant

es:EO'. e1:E. Cmd:ValueAllType. n,round:. p:Cmd List  (Id List).
  (p  rsc4_QuorumState(Cmd) <n, round>(e1)
   let cmds,locs = p 
     in no_repeats(Id;locs)
         (||locs|| = ||cmds||)
         (i:||locs||. (e:E. ((e <loc e1)  <<<n, round>, cmds[i]>, locs[i]>  rsc4_vote'base(Cmd)(e)))))
BY
{ (MemoryInvariant
   THEN (Decide i = 0 THENA Auto)
   THEN Try (((RWO "select_cons_tl" 0 THENA Auto) THEN BackThruSomeHyp THEN Auto))
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN Reduce 0
   THEN D 0
   THEN InstConcl [e']
   THEN Auto) }

---

\mforall{}es:EO'.  \mforall{}e1:E.  \mforall{}Cmd:ValueAllType.  \mforall{}n,round:\mBbbZ{}.  \mforall{}p:Cmd  List  \mtimes{}  (Id  List).
    (p  \mmember{}  rsc4\_QuorumState(Cmd)  <n,  round>(e1)
    {}\mRightarrow{}  let  cmds,locs  =  p 
          in  no\_repeats(Id;locs)
                \mwedge{}  (||locs||  =  ||cmds||)
                \mwedge{}  (\mforall{}i:\mBbbN{}||locs||
                          (\mdownarrow{}\mexists{}e:E.  ((e  <loc  e1)  \mwedge{}  <<<n,  round>,  cmds[i]>,  locs[i]>  \mmember{}  rsc4\_vote'base(Cmd)(e)))))


By

---

(MemoryInvariant
  THEN  (Decide  i  =  0  THENA  Auto)\mcdot{}
  THEN  Try  (((RWO  "select\_cons\_tl"  0  THENA  Auto)  THEN  BackThruSomeHyp  THEN  Auto)\mcdot{})
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  Reduce  0
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}
  THEN  Auto)



Home Index