---

Step * of Lemma new_23_sig_assert_newvote

∀[Cmd:ValueAllType]
  ∀ni:ℤ × ℤ. ∀vote:ℤ × ℤ × Cmd × Id. ∀quorum:Cmd List × (Id List).
    (↑(new_23_sig_newvote(Cmd) ni vote quorum) ⇐⇒ (ni = (fst(fst(vote))) ∈ (ℤ × ℤ)) ∧ (¬(snd(vote) ∈ snd(quorum))))
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA Auto)
   THEN RepUR ``new_23_sig_newvote`` 0
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN AllPushDown
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType]
    \mforall{}ni:\mBbbZ{}  \mtimes{}  \mBbbZ{}.  \mforall{}vote:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id.  \mforall{}quorum:Cmd  List  \mtimes{}  (Id  List).
        (\muparrow{}(new\_23\_sig\_newvote(Cmd)  ni  vote  quorum)
        \mLeftarrow{}{}\mRightarrow{}  (ni  =  (fst(fst(vote))))  \mwedge{}  (\mneg{}(snd(vote)  \mmember{}  snd(quorum))))


By

---

Latex:
(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  RepUR  ``new\_23\_sig\_newvote``  0
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  AllPushDown
  THEN  Auto)

---

Home Index