---

Step * of Lemma rsc4_replica_state_mem

es:EO'. e1,e2:E. Cmd:ValueAllType. z1,z2:  ( List). v:  Cmd.
  ((e1 <loc e2)
   v  rsc4_Proposal(Cmd)(e1)
   z1  rsc4_ReplicaState(Cmd)(e1)
   z2  rsc4_ReplicaState(Cmd)(e2)
   let num,c = v 
     in let max1,missing1 = z1 
        in let max2,missing2 = z2 
           in (num  max2)
               (int-list-member(num;missing2))
               (max1 z max2)
               (x:. ((int-list-member(x;missing2))  ((int-list-member(x;missing1))  (max1 <z x)))))
BY
{ MemoryMemHints ``rsc4_pos_max_missing`` }

---

\mforall{}es:EO'.  \mforall{}e1,e2:E.  \mforall{}Cmd:ValueAllType.  \mforall{}z1,z2:\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List).  \mforall{}v:\mBbbZ{}  \mtimes{}  Cmd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  v  \mmember{}  rsc4\_Proposal(Cmd)(e1)
    {}\mRightarrow{}  z1  \mmember{}  rsc4\_ReplicaState(Cmd)(e1)
    {}\mRightarrow{}  z2  \mmember{}  rsc4\_ReplicaState(Cmd)(e2)
    {}\mRightarrow{}  let  num,c  =  v 
          in  let  max1,missing1  =  z1 
                in  let  max2,missing2  =  z2 
                      in  (num  \mleq{}  max2)
                            \mwedge{}  (\mneg{}\muparrow{}int-list-member(num;missing2))
                            \mwedge{}  (\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

---

MemoryMemHints  ``rsc4\_pos\_max\_missing``



Home Index