---

Step * of Lemma new_23_sig_quorum_inv_vote_fun

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀i:ℕ||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||.
  (↓∃e':E
     ((e' <loc e)
     ∧ <<ni, fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]>
       , snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]
       > ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')))
BY
{ (Auto
   THEN InstLemma `new_23_sig_quorum_inv_vote` [⌈Cmd⌉;⌈notify⌉;⌈propose⌉;⌈f⌉;
   ⌈⌈es⌉;⌈e⌉;⌈ni⌉;⌈new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)⌉]⋅⌉
   THEN Auto
   THEN Try (BLemma `new_23_sig_QuorumState-classrel`)
   THEN Auto
   THEN UsePairEta [1] (-1)
   THEN RepD
   THEN InstHyp [⌈i⌉] (-1)⋅
   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{}e:E.  \mforall{}ni:\mBbbZ{}  \mtimes{}  \mBbbZ{}.
\mforall{}i:\mBbbN{}||snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||.
    (\mdownarrow{}\mexists{}e':E
          ((e'  <loc  e)
          \mwedge{}  <<ni,  fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]>
              ,  snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]
              >  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')))


By

---

Latex:
(Auto
  THEN  InstLemma  `new\_23\_sig\_quorum\_inv\_vote`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};
  \mkleeneopen{}\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}ni\mkleeneclose{};\mkleeneopen{}new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)\mkleeneclose{}]\mcdot{}\mkleeneclose{}
  THEN  Auto
  THEN  Try  (BLemma  `new\_23\_sig\_QuorumState-classrel`)
  THEN  Auto
  THEN  UsePairEta  [1]  (-1)
  THEN  RepD
  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index