---

Step * of Lemma new_23_sig_rounds_mem_fun

∀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,round:ℤ. ∀cmd:Cmd.
  ((e1 <loc e2)
  ⇒ <<n, round>, cmd> ∈ new_23_sig_RoundInfo(Cmd;notify;propose;f)(e1)
  ⇒ (round ≤ new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e2)))
BY
{ (Unfold `vatype` 0
   THEN Auto
   THEN InstLemma `new_23_sig_rounds_mem` [⌈Cmd⌉;⌈notify⌉;⌈propose⌉;⌈f⌉;⌈es⌉;⌈e1⌉;⌈e2⌉;⌈n⌉;
   ⌈new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e1)⌉;
   ⌈new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e2)⌉;⌈<<n, round>, cmd>⌉]⋅
   THEN AllReduce
   THEN Auto
   THEN BLemma `new_23_sig_NewRoundsState-classrel`
   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,round:\mBbbZ{}.  \mforall{}cmd:Cmd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  <<n,  round>,  cmd>  \mmember{}  new\_23\_sig\_RoundInfo(Cmd;notify;propose;f)(e1)
    {}\mRightarrow{}  (round  \mleq{}  new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e2)))


By

---

Latex:
(Unfold  `vatype`  0
  THEN  Auto
  THEN  InstLemma  `new\_23\_sig\_rounds\_mem`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};
  \mkleeneopen{}new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e1)\mkleeneclose{};
  \mkleeneopen{}new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es;e2)\mkleeneclose{};\mkleeneopen{}<<n,  round>,  cmd>\mkleeneclose{}]\mcdot{}
  THEN  AllReduce
  THEN  Auto
  THEN  BLemma  `new\_23\_sig\_NewRoundsState-classrel`
  THEN  Auto)

---

Home Index