---

Step * 1 of Lemma canon-bnd_wf


1. x : ℕ+ ⟶ ℤ
2. regular-seq(x)
3. n : ℕ+
⊢ |x n| ≤ (n * (|x 1| + 3))
BY
{ ((D 2 With ⌜n⌝  THENA Auto) THEN (D -1 With ⌜1⌝  THENA Auto)) }

1
1. x : ℕ+ ⟶ ℤ
2. n : ℕ+
3. |(1 * (x n)) - n * (x 1)| ≤ ((2 * 1) * (n + 1))
⊢ |x n| ≤ (n * (|x 1| + 3))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  regular-seq(x)
3.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  |x  n|  \mleq{}  (n  *  (|x  1|  +  3))


By

---

Latex:
((D  2  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)  THEN  (D  -1  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto))

---

Home Index