---

Step * of Lemma pv11_p1_leq_bnum_linorder

∀ldrs_uid:Id ─→ ℤ. (Inj(Id;ℤ;ldrs_uid) ⇒ Linorder(pv11_p1_Ballot_Num();b1,b2.↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)))
BY
{ (Auto THEN RepeatFor 2 (D 0) THEN Auto THEN Try (D 0) THEN Auto THEN SimpleReasoningSteps) }

1
1. ldrs_uid : Id ─→ ℤ@i
2. Inj(Id;ℤ;ldrs_uid)@i
3. Trans(pv11_p1_Ballot_Num();b1,b2.↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2))
4. x4 : ℤ@i
5. x5 : Id@i
6. x2 : ℤ@i
7. x3 : Id@i
8. x4 = x2 ∈ ℤ
9. (ldrs_uid x5) ≤ (ldrs_uid x3)
10. x2 = x4 ∈ ℤ
11. (ldrs_uid x3) ≤ (ldrs_uid x5)
⊢ (inl <x4, x5>) = (inl <x2, x3>) ∈ pv11_p1_Ballot_Num()

2
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))

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}
    (Inj(Id;\mBbbZ{};ldrs$_{uid}$)  {}\mRightarrow{}  Linorder(pv11\_p1\_Ballot\_Num();b1,b2.\muparrow{}(pv11\_p1\_leq\_b\000Cnum(ldrs$_{uid}$)  b1  b2)))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  0)  THEN  Auto  THEN  Try  (D  0)  THEN  Auto  THEN  SimpleReasoningSteps)

---

Home Index