---

Step * of Lemma rsc4_strict_inc_rounds

es:EO'. e1,e2:E. Cmd:ValueAllType. n,round1,round2:.
  ((x:    Cmd
     e:E
      round:
       (e1 loc e 
        (e <loc e2)
        x  rsc4_RoundInfo(Cmd)(e)
        round  rsc4_NewRoundsState(Cmd) n(e)
        let ni,c = x 
         in let a1,a2 = ni 
            in (round < a2)  (n = a1)))
   (e1 <loc e2)
   round1  rsc4_NewRoundsState(Cmd) n(e1)
   round2  rsc4_NewRoundsState(Cmd) n(e2)
   (round1 <z round2))
BY
{ MemoryProgress2 }

---

\mforall{}es:EO'.  \mforall{}e1,e2:E.  \mforall{}Cmd:ValueAllType.  \mforall{}n,round1,round2:\mBbbZ{}.
    ((\mexists{}x:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd
          \mexists{}e:E
            \mexists{}round:\mBbbZ{}
              (e1  \mleq{}loc  e 
              \mwedge{}  (e  <loc  e2)
              \mwedge{}  x  \mmember{}  rsc4\_RoundInfo(Cmd)(e)
              \mwedge{}  round  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e)
              \mwedge{}  let  ni,c  =  x 
                  in  let  a1,a2  =  ni 
                        in  (round  <  a2)  \mwedge{}  (n  =  a1)))
    {}\mRightarrow{}  (e1  <loc  e2)
    {}\mRightarrow{}  round1  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e1)
    {}\mRightarrow{}  round2  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e2)
    {}\mRightarrow{}  (\muparrow{}round1  <z  round2))


By

---

MemoryProgress2



Home Index