---

Step * 1 1 1 of Lemma reg-seq-list-add_functionality_wrt_bdd-diff


1. B : ℕ
2. B1 : ℕ
3. v2 : ℤ
4. v3 : ℤ
5. v4 : ℤ
6. v5 : ℤ
⊢ (|v2 - v3| ≤ B) ⇒ (|v4 - v5| ≤ B1) ⇒ (|(v4 + v2) - v5 + v3| ≤ (B + B1))
BY
{ (Auto
   THEN (Assert |(v4 + v2) - v5 + v3| ≤ (|v4 - v5| + |v2 - v3|) BY
               (RWO "int-triangle-inequality<" 0 THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}
2.  B1  :  \mBbbN{}
3.  v2  :  \mBbbZ{}
4.  v3  :  \mBbbZ{}
5.  v4  :  \mBbbZ{}
6.  v5  :  \mBbbZ{}
\mvdash{}  (|v2  -  v3|  \mleq{}  B)  {}\mRightarrow{}  (|v4  -  v5|  \mleq{}  B1)  {}\mRightarrow{}  (|(v4  +  v2)  -  v5  +  v3|  \mleq{}  (B  +  B1))


By

---

Latex:
(Auto
  THEN  (Assert  |(v4  +  v2)  -  v5  +  v3|  \mleq{}  (|v4  -  v5|  +  |v2  -  v3|)  BY
                          (RWO  "int-triangle-inequality<"  0  THEN  Auto))
  THEN  Auto)

---

Home Index