---

Step * 2 of Lemma pv11_p1_leq_bnum_linorder


1. ldrs_uid : Id ─→ ℤ@i
2. Inj(Id;ℤ;ldrs_uid)@i
3. b1 : pv11_p1_Ballot_Num()@i
4. b2 : pv11_p1_Ballot_Num()@i
⊢ (↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ∨ (↑(pv11_p1_leq_bnum(ldrs_uid) b2 b1))
BY
{ (DVar `b1' THEN DVar `b2' THEN RepUR ``pv11_p1_leq_bnum`` 0 THEN Auto) }

1
1. ldrs_uid : Id ─→ ℤ@i
2. Inj(Id;ℤ;ldrs_uid)@i
3. x : ℤ × Id@i
4. x1 : ℤ × Id@i
⊢ (↑(pv11_p1_leq_bnum'(ldrs_uid) x x1)) ∨ (↑(pv11_p1_leq_bnum'(ldrs_uid) x1 x))

---

Latex:

---

Latex:

1.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
2.  Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
3.  b1  :  pv11\_p1\_Ballot\_Num()@i
4.  b2  :  pv11\_p1\_Ballot\_Num()@i
\mvdash{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b1  b2))  \mvee{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_\000C{uid}$)  b2  b1))


By

---

Latex:
(DVar  `b1'  THEN  DVar  `b2'  THEN  RepUR  ``pv11\_p1\_leq\_bnum``  0  THEN  Auto)

---

Home Index