---

Step * 1 of Lemma reg-seq-adjust_wf

.....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))
BY
{ (Subst ⌜(λi.if (i) < (n)  then 2  else (x i)) = x ∈ (ℕ+ ⟶ ℤ)⌝ 0⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:
.....truecase..... 
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.  n  =  1
\mvdash{}  regular-seq(\mlambda{}i.if  (i)  <  (n)    then  2    else  (x  i))


By

---

Latex:
(Subst  \mkleeneopen{}(\mlambda{}i.if  (i)  <  (n)    then  2    else  (x  i))  =  x\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index