---

Step * of Lemma new_23_sig_vote_with_ballot_and_id-forward

∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[start:E]. ∀[Cmd,propose,notify,e,n,r,i:Top].
  (new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es.start;e;n;r;i) 
  ~ new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``new_23_sig_vote_with_ballot_and_id new_23_sig_vote'base`` 0
   THEN (RWO "eo-forward-member-eclass" 0 THENA Auto)
   THEN RWO "eo-forward-info-body" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[start:E].  \mforall{}[Cmd,propose,notify,e,n,r,i:Top].
    (new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es.start;e;n;r;i) 
    \msim{}  new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e;n;r;i))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``new\_23\_sig\_vote\_with\_ballot\_and\_id  new\_23\_sig\_vote'base``  0
  THEN  (RWO  "eo-forward-member-eclass"  0  THENA  Auto)
  THEN  RWO  "eo-forward-info-body"  0
  THEN  Auto)

---

Home Index