---

Step * 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. rleq2(x1;y1)@i
⊢ rleq2(x2;y2)
BY
{ (All (RWO "rleq2-iff-rnonneg2") THENA Auto) }

1
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)))

---

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.  rleq2(x1;y1)@i
\mvdash{}  rleq2(x2;y2)


By

---

Latex:
(All  (RWO  "rleq2-iff-rnonneg2")  THENA  Auto)

---

Home Index