---

Step * 1 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. ∀b1,b2:pv11_p1_Ballot_Num().  ((↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ∨ (↑(pv11_p1_leq_bnum(ldrs_uid) b2 b1)))
⊢ ↑(b'  < b)
BY
{ (InstHyp [⌈b⌉;⌈b'⌉] (-1)⋅ THENA Auto) }

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)))
8. (↑(pv11_p1_leq_bnum(ldrs_uid) b b')) ∨ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))
⊢ ↑(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.  \mforall{}b1,b2:pv11\_p1\_Ballot\_Num().
          ((\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b1  b2))  \mvee{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$\mbackslash{}\000Cff5f{uid}$)  b2  b1)))
\mvdash{}  \muparrow{}(b'    <  b)


By

---

Latex:
(InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)

---

Home Index