---

Step * of Lemma new_23_sig_rounds_strict_inc

∀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
     ∃round:ℤ
      ∃e:E
       (e1 ≤loc e 
       ∧ (e <loc e2)
       ∧ z ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e)
       ∧ round ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e)
       ∧ let z,cmd = z 
         in let n',round' = z 
            in (n' = n ∈ ℤ) ∧ round < round'))
  ⇒ (e1 <loc e2)
  ⇒ round1 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e1)
  ⇒ round2 ∈ new_23_sig_NewRoundsState(Cmd;notify;propose;f) n(e2)
  ⇒ round1 < round2)
BY
{ (MemoryProgHints ``new_23_sig_rounds_pos`` THEN StartEmlProof THEN Auto) }

---

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{}.
    ((\mexists{}z:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd
          \mexists{}round:\mBbbZ{}
            \mexists{}e:E
              (e1  \mleq{}loc  e 
              \mwedge{}  (e  <loc  e2)
              \mwedge{}  z  \mmember{}  new\_23\_sig\_RoundInfo(Cmd;notify;propose;f)(e)
              \mwedge{}  round  \mmember{}  new\_23\_sig\_NewRoundsState(Cmd;notify;propose;f)  n(e)
              \mwedge{}  let  z,cmd  =  z 
                  in  let  n',round'  =  z 
                        in  (n'  =  n)  \mwedge{}  round  <  round'))
    {}\mRightarrow{}  (e1  <loc  e2)
    {}\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{}  round1  <  round2)


By

---

Latex:
(MemoryProgHints  ``new\_23\_sig\_rounds\_pos``  THEN  StartEmlProof  THEN  Auto)

---

Home Index