---

Step * of Lemma reg-seq-add_functionality_wrt_bdd-diff

∀x,x',y,y':ℕ+ ⟶ ℤ.  (bdd-diff(x;x') ⇒ bdd-diff(y;y') ⇒ bdd-diff(reg-seq-add(x;y);reg-seq-add(x';y')))
BY
{ (Auto THEN (InstLemma `reg-seq-list-add_functionality_wrt_bdd-diff` [⌜[x; y]⌝;[x'; y']]⋅ THENA Auto)) }

1
1. x : ℕ+ ⟶ ℤ
2. x' : ℕ+ ⟶ ℤ
3. y : ℕ+ ⟶ ℤ
4. y' : ℕ+ ⟶ ℤ
5. bdd-diff(x;x')
6. bdd-diff(y;y')
7. ||[x; y]|| = ||[x'; y']|| ∈ ℤ
8. i : ℕ||[x; y]||
⊢ bdd-diff([x; y][i];[x'; y'][i])

2
1. x : ℕ+ ⟶ ℤ
2. x' : ℕ+ ⟶ ℤ
3. y : ℕ+ ⟶ ℤ
4. y' : ℕ+ ⟶ ℤ
5. bdd-diff(x;x')
6. bdd-diff(y;y')
7. bdd-diff(reg-seq-list-add([x; y]);reg-seq-list-add([x'; y']))
⊢ bdd-diff(reg-seq-add(x;y);reg-seq-add(x';y'))

---

Latex:

---

Latex:
\mforall{}x,x',y,y':\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.
    (bdd-diff(x;x')  {}\mRightarrow{}  bdd-diff(y;y')  {}\mRightarrow{}  bdd-diff(reg-seq-add(x;y);reg-seq-add(x';y')))


By

---

Latex:
(Auto
  THEN  (InstLemma  `reg-seq-list-add\_functionality\_wrt\_bdd-diff`  [\mkleeneopen{}[x;  y]\mkleeneclose{};[x';  y']]\mcdot{}  THENA  Auto)
  )

---

Home Index