---

Step * of Lemma pv11_p1_leq_bnum_dummy_eq

∀ldrs_uid:Id ⟶ ℤ. ∀b:pv11_p1_Ballot_Num().  (pv11_p1_leq_bnum(ldrs_uid) pv11_p1_dummy_ballot() b ~ tt)
BY
{ (RepUR ``pv11_p1_Ballot_Num pv11_p1_dummy_ballot`` 0 THEN Auto THEN SimpleReasoningSteps) }

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b:pv11\_p1\_Ballot\_Num().
    (pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  pv11\_p1\_dummy\_ballot()  b  \msim{}  tt)


By

---

Latex:
(RepUR  ``pv11\_p1\_Ballot\_Num  pv11\_p1\_dummy\_ballot``  0  THEN  Auto  THEN  SimpleReasoningSteps)

---

Home Index