---

Step * 1 1 1 of Lemma pv11_p1_pmax_desc


1. ldrs_uid : Id ─→ ℤ@i
2. x : ℤ × Id
3. x1 : ℤ × Id@i
⊢ (¬↑(pv11_p1_leq_bnum'(ldrs_uid) x1 x)) ⇒ (↑(pv11_p1_lt_bnum'(ldrs_uid) x x1))
BY
{ ((D 2 THEN D -1) THEN RepUR ``pv11_p1_leq_bnum\' pv11_p1_lt_bnum\'`` 0) }

1
1. ldrs_uid : Id ─→ ℤ@i
2. x2 : ℤ
3. x3 : Id
4. x4 : ℤ@i
5. x5 : Id@i
⊢ (¬↑(x4 <z x2 ∨b((x4 =z x2) ∧b ldrs_uid x5 ≤z ldrs_uid x3)))
⇒ (↑(x2 <z x4 ∨b((x2 =z x4) ∧b ldrs_uid x3 <z ldrs_uid x5)))

---

Latex:

---

Latex:

1.  ldrs$_{uid}$  :  Id  {}\mrightarrow{}  \mBbbZ{}@i
2.  x  :  \mBbbZ{}  \mtimes{}  Id
3.  x1  :  \mBbbZ{}  \mtimes{}  Id@i
\mvdash{}  (\mneg{}\muparrow{}(pv11\_p1\_leq\_bnum'(ldrs$_{uid}$)  x1  x))  {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_lt\_bnum'(ldrs$\mbackslash{}ff\000C5f{uid}$)  x  x1))


By

---

Latex:
((D  2  THEN  D  -1)  THEN  RepUR  ``pv11\_p1\_leq\_bnum\mbackslash{}'  pv11\_p1\_lt\_bnum\mbackslash{}'``  0)

---

Home Index