---

Step * of Lemma radd-bdd-diff

∀a,b:ℝ.  bdd-diff(a + b;λn.((a n) + (b n)))
BY
{ (Auto
   THEN Unfold `radd` 0
   THEN RWO "accelerate-bdd-diff" 0
   THEN Auto
   THEN With ⌜0⌝ (D 0)⋅
   THEN Auto
   THEN (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto)
   THEN Reduce 0
   THEN RW IntNormC 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    bdd-diff(a  +  b;\mlambda{}n.((a  n)  +  (b  n)))


By

---

Latex:
(Auto
  THEN  Unfold  `radd`  0
  THEN  RWO  "accelerate-bdd-diff"  0
  THEN  Auto
  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RW  IntNormC  0
  THEN  Auto)

---

Home Index