---

Step * 1 of Lemma pv11_p1_leq_bnum_linorder


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()
BY
{ (Unfold `pv11_p1_Ballot_Num` 0 THEN RepeatFor 2 (EqCD) THEN Auto THEN BackThruHyp' 2 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
2.  Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
3.  Trans(pv11\_p1\_Ballot\_Num();b1,b2.\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b1  b2))
4.  x4  :  \mBbbZ{}@i
5.  x5  :  Id@i
6.  x2  :  \mBbbZ{}@i
7.  x3  :  Id@i
8.  x4  =  x2
9.  (ldrs$_{uid}$  x5)  \mleq{}  (ldrs$_{uid}$  x3)
10.  x2  =  x4
11.  (ldrs$_{uid}$  x3)  \mleq{}  (ldrs$_{uid}$  x5)
\mvdash{}  (inl  <x4,  x5>)  =  (inl  <x2,  x3>)


By

---

Latex:
(Unfold  `pv11\_p1\_Ballot\_Num`  0  THEN  RepeatFor  2  (EqCD)  THEN  Auto  THEN  BackThruHyp'  2  THEN  Auto)\mcdot{}

---

Home Index