---

Step * of Lemma new_23_sig_rounds_mem

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀n,round1,round2:ℤ. ∀z:ℤ × ℤ × Cmd.
  ((e1 <loc e2)
  ⇒ z ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e1)
  ⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
  ⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
  ⇒ let z,cmd = z 
     in let n',round' = z 
        in (n = n' ∈ ℤ) ⇒ (round' ≤ round2))
BY
{ MemoryMemHints ``new_23_sig_rounds_pos`` }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}notify,propose:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.  \mforall{}n,round1,round2:\mBbbZ{}.  \mforall{}z:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  z  \mmember{}  new\_23\_sig\_RoundInfo(Cmd;notify;propose;f)(e1)
    {}\mRightarrow{}  round1  \mmember{}  new\_23\_sig\_NewRoundsState(Cmd;notify;propose;f)  n(e1)
    {}\mRightarrow{}  round2  \mmember{}  new\_23\_sig\_NewRoundsState(Cmd;notify;propose;f)  n(e2)
    {}\mRightarrow{}  let  z,cmd  =  z 
          in  let  n',round'  =  z 
                in  (n  =  n')  {}\mRightarrow{}  (round'  \mleq{}  round2))


By

---

Latex:
MemoryMemHints  ``new\_23\_sig\_rounds\_pos``

---

Home Index