---

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


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])
BY
{ (Reduce (-1) THEN IntSegCases (-1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  x'  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  y'  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
5.  bdd-diff(x;x')
6.  bdd-diff(y;y')
7.  ||[x;  y]||  =  ||[x';  y']||
8.  i  :  \mBbbN{}||[x;  y]||
\mvdash{}  bdd-diff([x;  y][i];[x';  y'][i])


By

---

Latex:
(Reduce  (-1)  THEN  IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto)

---

Home Index