---

Step * 1 of Lemma pv11_p1_leq_bnum_implies_eq_or_lt


1. ldrs_uid : Id ─→ ℤ@i
2. x : ℤ × Id@i
3. x1 : ℤ × Id@i
4. Inj(Id;ℤ;ldrs_uid)@i
5. ↑(pv11_p1_leq_bnum'(ldrs_uid) x x1)@i
⊢ ((inl x) = (inl x1) ∈ (ℤ × Id?)) ∨ (↑(pv11_p1_lt_bnum'(ldrs_uid) x x1))
BY
{ (D 3 THEN D 2 THEN All (RepUR ``pv11_p1_leq_bnum\' pv11_p1_lt_bnum\'``)) }

1
1. ldrs_uid : Id ─→ ℤ@i
2. x4 : ℤ@i
3. x5 : Id@i
4. x2 : ℤ@i
5. x3 : Id@i
6. Inj(Id;ℤ;ldrs_uid)@i
7. ↑(x4 <z x2 ∨b((x4 =z x2) ∧b ldrs_uid x5 ≤z ldrs_uid x3))@i
⊢ ((inl <x4, x5>) = (inl <x2, x3>) ∈ (ℤ × Id?)) ∨ (↑(x4 <z x2 ∨b((x4 =z x2) ∧b ldrs_uid x5 <z ldrs_uid x3)))

---

Latex:

---

Latex:

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


By

---

Latex:
(D  3  THEN  D  2  THEN  All  (RepUR  ``pv11\_p1\_leq\_bnum\mbackslash{}'  pv11\_p1\_lt\_bnum\mbackslash{}'``))

---

Home Index