---

Step * of Lemma pv11_p1_lt_bnum_upd

∀ldrs_uid:Id ─→ ℤ. ∀b:pv11_p1_Ballot_Num(). ∀l:Id.  ((↑(pv11_p1_is_bnum() b)) ⇒ (↑(b  < (pv11_p1_upd_bnum() b l))))
BY
{ (Auto THEN SimpleReasoningSteps) }

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b:pv11\_p1\_Ballot\_Num().  \mforall{}l:Id.
    ((\muparrow{}(pv11\_p1\_is\_bnum()  b))  {}\mRightarrow{}  (\muparrow{}(b    <  (pv11\_p1\_upd\_bnum()  b  l))))


By

---

Latex:
(Auto  THEN  SimpleReasoningSteps)

---

Home Index