---

Step * 1 of Lemma reg-seq-list-add_functionality_wrt_bdd-diff


∀L,L':(ℕ+ ⟶ ℤ) List.
  ((||L|| = ||L'|| ∈ ℤ)
  ⇒ (∀i:ℕ||L||. bdd-diff(L[i];L'[i]))
  ⇒ bdd-diff(λn.l_sum(map(λx.(x n);L));λn.l_sum(map(λx.(x n);L'))))
BY
{ (RepeatFor 2 (InductionOnList)
   THEN Reduce 0
   THEN Auto'
   THEN Try ((BLemma `trivial-bdd-diff` THEN Reduce 0 THEN Complete (Auto)))
   THEN (Thin (-3)
         THEN (InstHyp [⌜v1⌝] 3⋅
               THENA (Auto THEN InstHyp [⌜i + 1⌝] (-2)⋅ THEN Auto THEN NthHypEq (-1) THEN EqCD THEN Auto)
               )
         )⋅
   THEN Thin 3
   THEN (InstHyp [⌜0⌝] (-2)⋅ THENA Auto)
   THEN Thin (-3)
   THEN Reduce (-1)
   THEN D (-2)
   THEN D -1
   THEN With ⌜B + B1⌝ (D 0)⋅
   THEN Auto
   THEN All Reduce)⋅ }

1
1. u : ℕ+ ⟶ ℤ
2. v : (ℕ+ ⟶ ℤ) List
3. u1 : ℕ+ ⟶ ℤ
4. v1 : (ℕ+ ⟶ ℤ) List
5. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
6. B : ℕ
7. ∀n:ℕ+. (|l_sum(map(λx.(x n);v)) - l_sum(map(λx.(x n);v1))| ≤ B)
8. B1 : ℕ
9. ∀n:ℕ+. (|(u n) - u1 n| ≤ B1)
10. n : ℕ+
⊢ |((u n) + l_sum(map(λx.(x n);v))) - (u1 n) + l_sum(map(λx.(x n);v1))| ≤ (B + B1)

---

Latex:

---

Latex:

\mforall{}L,L':(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  List.
    ((||L||  =  ||L'||)
    {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||L||.  bdd-diff(L[i];L'[i]))
    {}\mRightarrow{}  bdd-diff(\mlambda{}n.l\_sum(map(\mlambda{}x.(x  n);L));\mlambda{}n.l\_sum(map(\mlambda{}x.(x  n);L'))))


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  Reduce  0
  THEN  Auto'
  THEN  Try  ((BLemma  `trivial-bdd-diff`  THEN  Reduce  0  THEN  Complete  (Auto)))
  THEN  (Thin  (-3)
              THEN  (InstHyp  [\mkleeneopen{}v1\mkleeneclose{}]  3\mcdot{}
                          THENA  (Auto
                                        THEN  InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  (-2)\mcdot{}
                                        THEN  Auto
                                        THEN  NthHypEq  (-1)
                                        THEN  EqCD
                                        THEN  Auto)
                          )
              )\mcdot{}
  THEN  Thin  3
  THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  Reduce  (-1)
  THEN  D  (-2)
  THEN  D  -1
  THEN  With  \mkleeneopen{}B  +  B1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  All  Reduce)\mcdot{}

---

Home Index