---

Step * of Lemma reg-seq-adjust_wf

∀[n:ℕ+]. ∀[x:ℝ].  reg-seq-adjust(n;x) ∈ {f:ℕ+ ⟶ ℤ| if (n =z 1) then 1 else 4 fi -regular-seq(f)}  supposing ∀i:ℕ+. (i <\000C n ⇒ (|x i| ≤ 4))
BY
{ (Auto THEN D -2 THEN MemTypeCD THEN Auto THEN ProveWfLemma⋅) }

1
.....truecase..... 
1. n : ℕ+
2. x : ℕ+ ⟶ ℤ
3. regular-seq(x)
4. ∀i:ℕ+. (i < n ⇒ (|x i| ≤ 4))
5. n = 1 ∈ ℤ
⊢ regular-seq(λi.if (i) < (n)  then 2  else (x i))

2
.....falsecase..... 
1. n : ℕ+
2. x : ℕ+ ⟶ ℤ
3. regular-seq(x)
4. ∀i:ℕ+. (i < n ⇒ (|x i| ≤ 4))
5. ¬(n = 1 ∈ ℤ)
⊢ 4-regular-seq(λi.if (i) < (n)  then 2  else (x i))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbR{}].
    reg-seq-adjust(n;x)  \mmember{}  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  if  (n  =\msubz{}  1)  then  1  else  4  fi  -regular-seq(f)\}    supposing  \mforall{}i:\mBbbN{}\msupplus{}.  \000C(i  <  n  {}\mRightarrow{}  (|x  i|  \mleq{}  4))


By

---

Latex:
(Auto  THEN  D  -2  THEN  MemTypeCD  THEN  Auto  THEN  ProveWfLemma\mcdot{})

---

Home Index