---

Step * of Lemma radd-list-cons

∀[L:ℝ List]. ∀[x:ℝ].  (radd-list([x / L]) = (x + radd-list(L)))
BY
{ ((Auto THEN (BLemma `req-iff-bdd-diff` THENA Auto))
   THEN ((Unfold `radd` 0
          THEN (RWW "accelerate-bdd-diff" 0 THENA Auto)
          THEN (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto))
         THEN Reduce 0⋅
         )
   ) }

1
1. L : ℝ List
2. x : ℝ
⊢ bdd-diff(radd-list([x / L]);λn.((x n) + (radd-list(L) n) + 0))

---

Latex:

---

Latex:
\mforall{}[L:\mBbbR{}  List].  \mforall{}[x:\mBbbR{}].    (radd-list([x  /  L])  =  (x  +  radd-list(L)))


By

---

Latex:
((Auto  THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto))
  THEN  ((Unfold  `radd`  0
                THEN  (RWW  "accelerate-bdd-diff"  0  THENA  Auto)
                THEN  (RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto))
              THEN  Reduce  0\mcdot{}
              )
  )

---

Home Index