---

Step * 2 2 of Lemma reg-seq-adjust_wf


1. n : ℕ+
2. x : ℕ+ ⟶ ℤ
3. regular-seq(x)
4. ∀i:ℕ+. (i < n ⇒ (|x i| ≤ 4))
5. ¬(n = 1 ∈ ℤ)
6. ∀[g:ℕ+ ⟶ ℤ]. 4-regular-seq(g) supposing ∀n:ℕ+. (|(x n) - g n| ≤ 6)
7. n1 : ℕ+@i
8. ¬n1 < n
⊢ |(x n1) - x n1| ≤ 6
BY
{ (RW IntNormC 0 THEN Auto THEN RepUR ``absval`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  regular-seq(x)
4.  \mforall{}i:\mBbbN{}\msupplus{}.  (i  <  n  {}\mRightarrow{}  (|x  i|  \mleq{}  4))
5.  \mneg{}(n  =  1)
6.  \mforall{}[g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  4-regular-seq(g)  supposing  \mforall{}n:\mBbbN{}\msupplus{}.  (|(x  n)  -  g  n|  \mleq{}  6)
7.  n1  :  \mBbbN{}\msupplus{}@i
8.  \mneg{}n1  <  n
\mvdash{}  |(x  n1)  -  x  n1|  \mleq{}  6


By

---

Latex:
(RW  IntNormC  0  THEN  Auto  THEN  RepUR  ``absval``  0  THEN  Auto)

---

Home Index