---

Step * 2 1 of Lemma pv11_p1_leq_bnum_linorder


1. ldrs_uid : Id ─→ ℤ@i
2. Inj(Id;ℤ;ldrs_uid)@i
3. x : ℤ × Id@i
4. x1 : ℤ × Id@i
⊢ (↑(pv11_p1_leq_bnum'(ldrs_uid) x x1)) ∨ (↑(pv11_p1_leq_bnum'(ldrs_uid) x1 x))
BY
{ SimpleReasoningSteps }

---

Latex:

---

Latex:

1.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
2.  Inj(Id;\mBbbZ{};ldrs$_{uid}$)@i
3.  x  :  \mBbbZ{}  \mtimes{}  Id@i
4.  x1  :  \mBbbZ{}  \mtimes{}  Id@i
\mvdash{}  (\muparrow{}(pv11\_p1\_leq\_bnum'(ldrs$_{uid}$)  x  x1))  \mvee{}  (\muparrow{}(pv11\_p1\_leq\_bnum'(ldrs$\mbackslash{}ff5\000Cf{uid}$)  x1  x))


By

---

Latex:
SimpleReasoningSteps

---

Home Index