---

Step * of Lemma radd-approx

∀[a,b:ℝ]. ∀[n:ℕ+].  ((a + b) n ~ ((a (4 * n)) + (b (4 * n))) ÷ 4)
BY
{ (Auto
   THEN RepUR ``radd reg-seq-list-add accelerate`` 0
   THEN RepeatFor 2 ((RecUnfold `cbv_list_accum` 0 THEN RepeatFor 2 (((CallByValueReduce 0 THENA Auto) THEN Reduce 0))))
   THEN RecUnfold `cbv_list_accum` 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    ((a  +  b)  n  \msim{}  ((a  (4  *  n))  +  (b  (4  *  n)))  \mdiv{}  4)


By

---

Latex:
(Auto
  THEN  RepUR  ``radd  reg-seq-list-add  accelerate``  0
  THEN  RepeatFor  2  ((RecUnfold  `cbv\_list\_accum`  0
                                        THEN  RepeatFor  2  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))
                                        ))
  THEN  RecUnfold  `cbv\_list\_accum`  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index