---

Step * of Lemma pv11_p1_leq_bnum_implies_eq

∀ldrs_uid:Id ⟶ ℤ. ∀b,b':pv11_p1_Ballot_Num().
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b b'))
  ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))
  ⇒ (b = b' ∈ pv11_p1_Ballot_Num()))
BY
{ (Auto
   THEN D 3
   THEN D 2
   THEN All (RepUR ``pv11_p1_leq_bnum pv11_p1_Ballot_Num pv11_p1_leq_bnum\'``)
   THEN Try (Trivial)
   THEN ((EqCD THEN Auto) THEN D 3 THEN D 2 THEN All Reduce)⋅) }

1
1. ldrs_uid : Id ⟶ ℤ@i
2. x4 : ℤ@i
3. x5 : Id@i
4. x2 : ℤ@i
5. x3 : Id@i
6. Inj(Id;ℤ;ldrs_uid)@i
7. ↑(x4 <z x2 ∨b((x4 =z x2) ∧b ldrs_uid x5 ≤z ldrs_uid x3))@i
8. ↑(x2 <z x4 ∨b((x2 =z x4) ∧b ldrs_uid x3 ≤z ldrs_uid x5))@i
⊢ <x4, x5> = <x2, x3> ∈ (ℤ × Id)

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b,b':pv11\_p1\_Ballot\_Num().
    (Inj(Id;\mBbbZ{};ldrs$_{uid}$)
    {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b  b'))
    {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b'  b))
    {}\mRightarrow{}  (b  =  b'))


By

---

Latex:
(Auto
  THEN  D  3
  THEN  D  2
  THEN  All  (RepUR  ``pv11\_p1\_leq\_bnum  pv11\_p1\_Ballot\_Num  pv11\_p1\_leq\_bnum\mbackslash{}'``)
  THEN  Try  (Trivial)
  THEN  ((EqCD  THEN  Auto)  THEN  D  3  THEN  D  2  THEN  All  Reduce)\mcdot{})

---

Home Index