---

Step * 2 of Lemma reg-seq-adjust_wf

.....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))
BY
{ ((InstLemma `bdd-diff-regular-int-seq` [⌜1⌝;⌜3⌝;⌜x⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN BHyp -1
   THEN Auto
   THEN Reduce 0
   THEN AutoSplit) }

1
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

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
⊢ |(x n1) - x n1| ≤ 6

---

Latex:

---

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


By

---

Latex:
((InstLemma  `bdd-diff-regular-int-seq`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}3\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  BHyp  -1
  THEN  Auto
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index