---

Step * of Lemma pv11_p1_lt_bnum_implies_not3

∀ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().  ((↑(pv11_p1_leq_bnum(ldrs_uid) b2 b1)) ⇒ (↑(b1  < b2)) ⇒ False)
BY
{ (Auto
   THEN All
   (RepUR ``pv11_p1_leq_bnum pv11_p1_lt_bnum``)⋅
   THEN (D 3 THEN D 2)
   THEN All Reduce
   THEN (Try (Trivial) THEN D 3 THEN D 2)
   THEN All
   (RepUR ``pv11_p1_leq_bnum\' pv11_p1_lt_bnum\'``)⋅
   THEN All
   (RW assert_pushdownC)⋅
   THEN Auto
   THEN SplitOrHyps
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b1,b2:pv11\_p1\_Ballot\_Num().
    ((\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b2  b1))  {}\mRightarrow{}  (\muparrow{}(b1    <  b2))  {}\mRightarrow{}  False)


By

---

Latex:
(Auto
  THEN  All
  (RepUR  ``pv11\_p1\_leq\_bnum  pv11\_p1\_lt\_bnum``)\mcdot{}
  THEN  (D  3  THEN  D  2)
  THEN  All  Reduce
  THEN  (Try  (Trivial)  THEN  D  3  THEN  D  2)
  THEN  All
  (RepUR  ``pv11\_p1\_leq\_bnum\mbackslash{}'  pv11\_p1\_lt\_bnum\mbackslash{}'``)\mcdot{}
  THEN  All
  (RW  assert\_pushdownC)\mcdot{}
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index