---

Step * of Lemma rsc4_positive_max

es:EO'. e1:E. Cmd:ValueAllType. v1:  ( List).
  (v1  rsc4_ReplicaState(Cmd)(e1)
   let max,missing = v1 
     in (0 z max)  (x:. ((int-list-member(x;missing))  ((0 <z x)  (x <z max)))))
BY
{ MemoryInvariant }

---

\mforall{}es:EO'.  \mforall{}e1:E.  \mforall{}Cmd:ValueAllType.  \mforall{}v1:\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List).
    (v1  \mmember{}  rsc4\_ReplicaState(Cmd)(e1)
    {}\mRightarrow{}  let  max,missing  =  v1 
          in  (\muparrow{}0  \mleq{}z  max)  \mwedge{}  (\mforall{}x:\mBbbZ{}.  ((\muparrow{}int-list-member(x;missing))  {}\mRightarrow{}  ((\muparrow{}0  <z  x)  \mwedge{}  (\muparrow{}x  <z  max)))))


By

---

MemoryInvariant



Home Index