---

Step * of Lemma pv11_p1_leq_bnum_max

∀ldrs_uid:Id ⟶ ℤ. ∀b,b':pv11_p1_Ballot_Num().  (↑(pv11_p1_leq_bnum(ldrs_uid) b (pv11_p1_max_bnum(ldrs_uid) b' b)))
BY
{ (RepUR ``pv11_p1_Ballot_Num pv11_p1_max_bnum`` 0 THEN Auto THEN SimpleReasoningSteps) }

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b,b':pv11\_p1\_Ballot\_Num().
    (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b  (pv11\_p1\_max\_bnum(ldrs$_{uid\mbackslash{}f\000Cf7d$)  b'  b)))


By

---

Latex:
(RepUR  ``pv11\_p1\_Ballot\_Num  pv11\_p1\_max\_bnum``  0  THEN  Auto  THEN  SimpleReasoningSteps)

---

Home Index