---

Step * of Lemma rsc4_rounds_state_mem

es:EO'. e1,e2:E. Cmd:ValueAllType. n,round1,round2:. x:    Cmd.
  ((e1 <loc e2)
   x  rsc4_RoundInfo(Cmd)(e1)
   round1  rsc4_NewRoundsState(Cmd) n(e1)
   round2  rsc4_NewRoundsState(Cmd) n(e2)
   let ni,c = x 
     in let m,i = ni 
        in (n = m)  (i  round2))
BY
{ MemoryMemory }

---

\mforall{}es:EO'.  \mforall{}e1,e2:E.  \mforall{}Cmd:ValueAllType.  \mforall{}n,round1,round2:\mBbbZ{}.  \mforall{}x:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  x  \mmember{}  rsc4\_RoundInfo(Cmd)(e1)
    {}\mRightarrow{}  round1  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e1)
    {}\mRightarrow{}  round2  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e2)
    {}\mRightarrow{}  let  ni,c  =  x 
          in  let  m,i  =  ni 
                in  (n  =  m)  {}\mRightarrow{}  (i  \mleq{}  round2))


By

---

MemoryMemory



Home Index