---

Step * 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(reg-seq-list-add(L);reg-seq-list-add(L')))
BY
{ (Auto THEN (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto) THEN MoveToConcl 2 THEN MoveToConcl 1) }

1
∀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'))))

---

Latex:

---

Latex:
\mforall{}L,L':(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  List.
    (((||L||  =  ||L'||)  \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  bdd-diff(L[i];L'[i])))
    {}\mRightarrow{}  bdd-diff(reg-seq-list-add(L);reg-seq-list-add(L')))


By

---

Latex:
(Auto  THEN  (RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)  THEN  MoveToConcl  2  THEN  MoveToConcl  1)

---

Home Index