---

Step * of Lemma pv11_p1_leq_bnum_refl

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

---

Latex:

---

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


By

---

Latex:
(Unfold  `pv11\_p1\_Ballot\_Num`  0  THEN  Auto  THEN  SimpleReasoningSteps)

---

Home Index