---

Step * of Lemma not-pv11_p1_leq_bnum

∀ldrs_uid:Id ─→ ℤ. ∀b,b':pv11_p1_Ballot_Num().
  (Inj(Id;ℤ;ldrs_uid) ⇒ (¬↑(pv11_p1_leq_bnum(ldrs_uid) b b')) ⇒ (↑(b'  < b)))
BY
{ (Auto THEN (InstLemma `pv11_p1_leq_bnum_linorder` [⌈ldrs_uid⌉]⋅ 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. Linorder(pv11_p1_Ballot_Num();b1,b2.↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2))
⊢ ↑(b'  < b)

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b,b':pv11\_p1\_Ballot\_Num().
    (Inj(Id;\mBbbZ{};ldrs$_{uid}$)  {}\mRightarrow{}  (\mneg{}\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}\mbackslash{}ff\000C24)  b  b'))  {}\mRightarrow{}  (\muparrow{}(b'    <  b)))


By

---

Latex:
(Auto  THEN  (InstLemma  `pv11\_p1\_leq\_bnum\_linorder`  [\mkleeneopen{}ldrs$_{uid}$\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index