---

Step * 2 1 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) - 2| ≤ 6
BY
{ Assert ⌜|(x n1) - 2| ≤ (|x n1| + |-2|)⌝⋅ }

1
.....assertion..... 
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) - 2| ≤ (|x n1| + |-2|)

2
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
9. |(x n1) - 2| ≤ (|x n1| + |-2|)
⊢ |(x n1) - 2| ≤ 6

---

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.  n1  <  n
\mvdash{}  |(x  n1)  -  2|  \mleq{}  6


By

---

Latex:
Assert  \mkleeneopen{}|(x  n1)  -  2|  \mleq{}  (|x  n1|  +  |-2|)\mkleeneclose{}\mcdot{}

---

Home Index