---

Step * of Lemma radd-list_functionality

∀[L1,L2:ℝ List].  radd-list(L1) = radd-list(L2) supposing (||L1|| = ||L2|| ∈ ℤ) ∧ (∀i:ℕ||L1||. (L1[i] = L2[i]))
BY
{ (Auto
   THEN RepUR ``radd-list`` 0
   THEN (CallByValueReduceOnTypes [⌜ℝ List⌝] 0⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN AutoSplit
   THEN ((BLemma `req-iff-bdd-diff`⋅ THENM RWO "accelerate-bdd-diff" 0) THENA Auto)
   THEN ((RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto) THEN Thin (-4))⋅) }

1
1. L1 : ℝ List
2. L2 : ℝ List
3. ||L1|| = ||L2|| ∈ ℤ
4. ∀i:ℕ||L1||. (L1[i] = L2[i])
⊢ bdd-diff(λn.l_sum(map(λx.(x n);L1));λn.l_sum(map(λx.(x n);L2)))

---

Latex:

---

Latex:
\mforall{}[L1,L2:\mBbbR{}  List].
    radd-list(L1)  =  radd-list(L2)  supposing  (||L1||  =  ||L2||)  \mwedge{}  (\mforall{}i:\mBbbN{}||L1||.  (L1[i]  =  L2[i]))


By

---

Latex:
(Auto
  THEN  RepUR  ``radd-list``  0
  THEN  (CallByValueReduceOnTypes  [\mkleeneopen{}\mBbbR{}  List\mkleeneclose{}]  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  AutoSplit
  THEN  ((BLemma  `req-iff-bdd-diff`\mcdot{}  THENM  RWO  "accelerate-bdd-diff"  0)  THENA  Auto)
  THEN  ((RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)  THEN  Thin  (-4))\mcdot{})

---

Home Index