---

Step * of Lemma bdd-diff-add

∀[f1,f2,g1,g2:ℕ+ ⟶ ℤ].  (bdd-diff(f1;f2) ⇒ bdd-diff(g1;g2) ⇒ bdd-diff(λn.(f1[n] + g1[n]);λn.(f2[n] + g2[n])))
BY
{ (Auto THEN All (Unfold `bdd-diff`) THEN ExRepD THEN With ⌜B + B1⌝ (D 0)⋅ THEN Auto THEN Reduce 0) }

1
1. f1 : ℕ+ ⟶ ℤ
2. f2 : ℕ+ ⟶ ℤ
3. g1 : ℕ+ ⟶ ℤ
4. g2 : ℕ+ ⟶ ℤ
5. B1 : ℕ
6. ∀n:ℕ+. (|(f1 n) - f2 n| ≤ B1)
7. B : ℕ
8. ∀n:ℕ+. (|(g1 n) - g2 n| ≤ B)
9. n : ℕ+
⊢ |(f1[n] + g1[n]) - f2[n] + g2[n]| ≤ (B + B1)

---

Latex:

---

Latex:
\mforall{}[f1,f2,g1,g2:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].
    (bdd-diff(f1;f2)  {}\mRightarrow{}  bdd-diff(g1;g2)  {}\mRightarrow{}  bdd-diff(\mlambda{}n.(f1[n]  +  g1[n]);\mlambda{}n.(f2[n]  +  g2[n])))


By

---

Latex:
(Auto  THEN  All  (Unfold  `bdd-diff`)  THEN  ExRepD  THEN  With  \mkleeneopen{}B  +  B1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Reduce  0)

---

Home Index