---

Step * 1 1 of Lemma pv11_p1_pmax_desc


1. ldrs_uid : Id ─→ ℤ@i
2. y1 : pv11_p1_Ballot_Num()
3. b' : pv11_p1_Ballot_Num()@i
⊢ (¬↑(pv11_p1_leq_bnum(ldrs_uid) b' y1)) ⇒ (↑(y1  < b'))
BY
{ (D 2 THEN D 3 THEN RepUR ``pv11_p1_leq_bnum pv11_p1_lt_bnum`` 0) }

1
1. ldrs_uid : Id ─→ ℤ@i
2. x : ℤ × Id
3. x1 : ℤ × Id@i
⊢ (¬↑(pv11_p1_leq_bnum'(ldrs_uid) x1 x)) ⇒ (↑(pv11_p1_lt_bnum'(ldrs_uid) x x1))

2
1. ldrs_uid : Id ─→ ℤ@i
2. x : ℤ × Id
3. y : Unit@i
⊢ (¬True) ⇒ False

3
1. ldrs_uid : Id ─→ ℤ@i
2. y : Unit
3. x : ℤ × Id@i
⊢ (¬False) ⇒ True

4
1. ldrs_uid : Id ─→ ℤ@i
2. y : Unit
3. y1 : Unit@i
⊢ (¬True) ⇒ False

---

Latex:

---

Latex:

1.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
2.  y1  :  pv11\_p1\_Ballot\_Num()
3.  b'  :  pv11\_p1\_Ballot\_Num()@i
\mvdash{}  (\mneg{}\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b'  y1))  {}\mRightarrow{}  (\muparrow{}(y1    <  b'))


By

---

Latex:
(D  2  THEN  D  3  THEN  RepUR  ``pv11\_p1\_leq\_bnum  pv11\_p1\_lt\_bnum``  0)

---

Home Index