---

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


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)
BY
{ (∀h:hyp. ((InstHyp [⌜n⌝] h⋅ THENA Auto) THEN MoveToConcl (-1)) 
   THEN GenConclAtAddr [1;1;1;1]
   THEN GenConclAtAddr [1;1;1;2]
   THEN GenConclAtAddr [2;1;1;1;1]
   THEN GenConclAtAddr [2;1;1;1;2]
   THEN All Thin) }

1
1. B : ℕ
2. B1 : ℕ
3. v2 : ℤ
4. v3 : ℤ
5. v4 : ℤ
6. v5 : ℤ
⊢ (|v2 - v3| ≤ B) ⇒ (|v4 - v5| ≤ B1) ⇒ (|(v4 + v2) - v5 + v3| ≤ (B + B1))

---

Latex:

---

Latex:

1.  u  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  v  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  List
3.  u1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  v1  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  List
5.  (||v||  +  1)  =  (||v1||  +  1)
6.  B  :  \mBbbN{}
7.  \mforall{}n:\mBbbN{}\msupplus{}.  (|l\_sum(map(\mlambda{}x.(x  n);v))  -  l\_sum(map(\mlambda{}x.(x  n);v1))|  \mleq{}  B)
8.  B1  :  \mBbbN{}
9.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(u  n)  -  u1  n|  \mleq{}  B1)
10.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  |((u  n)  +  l\_sum(map(\mlambda{}x.(x  n);v)))  -  (u1  n)  +  l\_sum(map(\mlambda{}x.(x  n);v1))|  \mleq{}  (B  +  B1)


By

---

Latex:
(\mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  THEN  MoveToConcl  (-1)) 
  THEN  GenConclAtAddr  [1;1;1;1]
  THEN  GenConclAtAddr  [1;1;1;2]
  THEN  GenConclAtAddr  [2;1;1;1;1]
  THEN  GenConclAtAddr  [2;1;1;1;2]
  THEN  All  Thin)

---

Home Index