---

Step * of Lemma pv11_p1_leq_bnum_implies_eq_or_lt

∀ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().
  (Inj(Id;ℤ;ldrs_uid) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ⇒ ((b1 = b2 ∈ pv11_p1_Ballot_Num()) ∨ (↑(b1  < b2))))
BY
{ ((Unfold `pv11_p1_Ballot_Num` 0 THEN Auto)
   THEN DVar `b1'
   THEN DVar `b2'
   THEN All (RepUR ``pv11_p1_lt_bnum pv11_p1_leq_bnum``)
   THEN Try (Trivial)) }

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

2
1. ldrs_uid : Id ─→ ℤ@i
2. y : Unit@i
3. x : ℤ × Id@i
4. Inj(Id;ℤ;ldrs_uid)@i
5. True@i
⊢ ((inr y ) = (inl x) ∈ (ℤ × Id?)) ∨ True

3
1. ldrs_uid : Id ─→ ℤ@i
2. y : Unit@i
3. y1 : Unit@i
4. Inj(Id;ℤ;ldrs_uid)@i
5. True@i
⊢ ((inr y ) = (inr y1 ) ∈ (ℤ × Id?)) ∨ False

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b1,b2:pv11\_p1\_Ballot\_Num().
    (Inj(Id;\mBbbZ{};ldrs$_{uid}$)  {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}\mbackslash{}ff2\000C4)  b1  b2))  {}\mRightarrow{}  ((b1  =  b2)  \mvee{}  (\muparrow{}(b1    <  b2))))


By

---

Latex:
((Unfold  `pv11\_p1\_Ballot\_Num`  0  THEN  Auto)
  THEN  DVar  `b1'
  THEN  DVar  `b2'
  THEN  All  (RepUR  ``pv11\_p1\_lt\_bnum  pv11\_p1\_leq\_bnum``)
  THEN  Try  (Trivial))

---

Home Index