---

Step * of Lemma pv11_p1_max_bnum_comm

∀[ldrs_uid:Id ─→ ℤ]. ∀[b1,b2:pv11_p1_Ballot_Num()].
  (pv11_p1_max_bnum(ldrs_uid) b1 b2) = (pv11_p1_max_bnum(ldrs_uid) b2 b1) ∈ pv11_p1_Ballot_Num() 
  supposing Inj(Id;ℤ;ldrs_uid)
BY
{ (RepUR ``pv11_p1_Ballot_Num pv11_p1_max_bnum pv11_p1_dummy_ballot`` 0
   THEN (Auto THEN DVar `b2' THEN DVar `b1' THEN RepUR ``pv11_p1_leq_bnum`` 0)
   THEN ((D 3 THEN D 2 THEN Progress(RepUR ``pv11_p1_leq_bnum\'`` 0)) ORELSE (EqCD THEN Auto)⋅)) }

1
1. ldrs_uid : Id ─→ ℤ
2. x4 : ℤ
3. x5 : Id
4. x2 : ℤ
5. x3 : Id
6. Inj(Id;ℤ;ldrs_uid)
⊢ if x4 <z x2 ∨b((x4 =z x2) ∧b ldrs_uid x5 ≤z ldrs_uid x3) then inl <x2, x3> else inl <x4, x5> fi 
= if x2 <z x4 ∨b((x2 =z x4) ∧b ldrs_uid x3 ≤z ldrs_uid x5) then inl <x4, x5> else inl <x2, x3> fi 
∈ (ℤ × Id?)

---

Latex:

---

Latex:
\mforall{}[ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[b1,b2:pv11\_p1\_Ballot\_Num()].
    (pv11\_p1\_max\_bnum(ldrs$_{uid}$)  b1  b2)  =  (pv11\_p1\_max\_bnum(ldrs$_{\000Cuid}$)  b2  b1)  supposing  Inj(Id;\mBbbZ{};ldrs$_{uid}$)


By

---

Latex:
(RepUR  ``pv11\_p1\_Ballot\_Num  pv11\_p1\_max\_bnum  pv11\_p1\_dummy\_ballot``  0
  THEN  (Auto  THEN  DVar  `b2'  THEN  DVar  `b1'  THEN  RepUR  ``pv11\_p1\_leq\_bnum``  0)
  THEN  ((D  3  THEN  D  2  THEN  Progress(RepUR  ``pv11\_p1\_leq\_bnum\mbackslash{}'``  0))  ORELSE  (EqCD  THEN  Auto)\mcdot{}))

---

Home Index