---

Step * of Lemma new_23_sig_quorum_inv_vote2_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:ℤ × ℤ.
  (no_repeats(Id;snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)))
  ∧ (||snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||
    = ||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))||
       (↓∃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')
          ∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
                                       (¬<<ni, c>, snd(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))[i]> ∈
                                          new_23_sig_vote'base(Cmd;notify;propose;f)(e'')))))))
BY
{ (StartEmlProof
   THEN InstLemma `new_23_sig_quorum_inv_vote2` [⌈Cmd⌉;⌈notify⌉;⌈propose⌉;⌈f⌉;⌈es⌉;⌈e⌉;⌈ni⌉;
   ⌈new_23_sig_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)⌉]⋅
   THEN Auto
   THEN Try (Complete ((UsePairEta [1] (-1) THEN Auto)))
   THEN Try (Complete ((UsePairEta [1] (-2) THEN Auto)))
   THEN Try (Complete ((UsePairEta [1] (-4) THEN Auto)))
   THEN Try ((BLemma `new_23_sig_QuorumState-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{}e:E.  \mforall{}ni:\mBbbZ{}  \mtimes{}  \mBbbZ{}.
    (no\_repeats(Id;snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)))
    \mwedge{}  (||snd(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||
        =  ||fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;ni;es;e))||)
    \mwedge{}  (\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')
                    \mwedge{}  (\mforall{}e''\mmember{}[es-init(es;e);e').
                                  \mforall{}c:Cmd
                                      (\mneg{}<<ni,  c>,  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:
(StartEmlProof
  THEN  InstLemma  `new\_23\_sig\_quorum\_inv\_vote2`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}ni\mkleeneclose{};
  \mkleeneopen{}new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;ni;es;e)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((UsePairEta  [1]  (-1)  THEN  Auto)))
  THEN  Try  (Complete  ((UsePairEta  [1]  (-2)  THEN  Auto)))
  THEN  Try  (Complete  ((UsePairEta  [1]  (-4)  THEN  Auto)))
  THEN  Try  ((BLemma  `new\_23\_sig\_QuorumState-classrel`  THEN  Auto)))

---

Home Index