---

Step * 1 1 of Lemma rleq2_functionality


1. x1 : ℕ+ ⟶ ℤ@i
2. y1 : ℕ+ ⟶ ℤ@i
3. x2 : ℕ+ ⟶ ℤ@i
4. y2 : ℕ+ ⟶ ℤ@i
5. bdd-diff(x1;x2)@i
6. bdd-diff(y1;y2)@i
7. rnonneg2(reg-seq-add(y1;-(x1)))
⊢ rnonneg2(reg-seq-add(y2;-(x2)))
BY
{ (RWO "-3 -2" (-1) THEN Try (Complete (Auto)) THEN RepUR ``reg-seq-add rminus`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
2.  y1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
3.  x2  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
4.  y2  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
5.  bdd-diff(x1;x2)@i
6.  bdd-diff(y1;y2)@i
7.  rnonneg2(reg-seq-add(y1;-(x1)))
\mvdash{}  rnonneg2(reg-seq-add(y2;-(x2)))


By

---

Latex:
(RWO  "-3  -2"  (-1)  THEN  Try  (Complete  (Auto))  THEN  RepUR  ``reg-seq-add  rminus``  0  THEN  Auto)

---

Home Index