---

Step * of Lemma rsc4_increasing_max

es:EO'. e1,e2:E. Cmd:ValueAllType. zl,z:  ( List).
  ((e1 <loc e2)
   zl  rsc4_ReplicaState(Cmd)(e1)
   z  rsc4_ReplicaState(Cmd)(e2)
   let max1,missing1 = zl 
     in let max2,missing2 = z 
        in (max1 z max2)
            (x:. ((int-list-member(x;missing2))  ((int-list-member(x;missing1))  (max1 <z x)))))
BY
{ MemoryOrdering }

---

\mforall{}es:EO'.  \mforall{}e1,e2:E.  \mforall{}Cmd:ValueAllType.  \mforall{}zl,z:\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List).
    ((e1  <loc  e2)
    {}\mRightarrow{}  zl  \mmember{}  rsc4\_ReplicaState(Cmd)(e1)
    {}\mRightarrow{}  z  \mmember{}  rsc4\_ReplicaState(Cmd)(e2)
    {}\mRightarrow{}  let  max1,missing1  =  zl 
          in  let  max2,missing2  =  z 
                in  (\muparrow{}max1  \mleq{}z  max2)
                      \mwedge{}  (\mforall{}x:\mBbbZ{}
                                ((\muparrow{}int-list-member(x;missing2))
                                {}\mRightarrow{}  ((\muparrow{}int-list-member(x;missing1))  \mvee{}  (\muparrow{}max1  <z  x)))))


By

---

MemoryOrdering



Home Index