---

Step * 1 1 of Lemma not-pv11_p1_leq_bnum


1. ldrs_uid : Id ─→ ℤ@i
2. b : pv11_p1_Ballot_Num()@i
3. b' : pv11_p1_Ballot_Num()@i
4. Inj(Id;ℤ;ldrs_uid)@i
5. ¬↑(pv11_p1_leq_bnum(ldrs_uid) b b')@i
6. Order(pv11_p1_Ballot_Num();b1,b2.↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2))
7. Connex(pv11_p1_Ballot_Num();b1,b2.↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2))
⊢ ↑(b'  < b)
BY
{ UnfoldTopAb (-1) }

1
1. ldrs_uid : Id ─→ ℤ@i
2. b : pv11_p1_Ballot_Num()@i
3. b' : pv11_p1_Ballot_Num()@i
4. Inj(Id;ℤ;ldrs_uid)@i
5. ¬↑(pv11_p1_leq_bnum(ldrs_uid) b b')@i
6. Order(pv11_p1_Ballot_Num();b1,b2.↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2))
7. ∀b1,b2:pv11_p1_Ballot_Num().  ((↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ∨ (↑(pv11_p1_leq_bnum(ldrs_uid) b2 b1)))
⊢ ↑(b'  < b)

---

Latex:

---

Latex:

1.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
2.  b  :  pv11\_p1\_Ballot\_Num()@i
3.  b'  :  pv11\_p1\_Ballot\_Num()@i
4.  Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
5.  \mneg{}\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b  b')@i
6.  Order(pv11\_p1\_Ballot\_Num();b1,b2.\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b1  b2))
7.  Connex(pv11\_p1\_Ballot\_Num();b1,b2.\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b1  b2))
\mvdash{}  \muparrow{}(b'    <  b)


By

---

Latex:
UnfoldTopAb  (-1)

---

Home Index