Step * of Lemma pv11_p1_max_bnum_if_leq

ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().
  ((↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2))  ((pv11_p1_max_bnum(ldrs_uid) b1 b2) b2 ∈ pv11_p1_Ballot_Num()))
BY
(RepUR ``pv11_p1_Ballot_Num pv11_p1_max_bnum pv11_p1_dummy_ballot`` THEN Auto THEN SimpleReasoningSteps) }


Latex:



Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b1,b2:pv11\_p1\_Ballot\_Num().
    ((\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b1  b2))  {}\mRightarrow{}  ((pv11\_p1\_max\_bnum(ldrs$\mbackslash{}ff5\000Cf{uid}$)  b1  b2)  =  b2))


By


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




Home Index