---

Step * of Lemma regular-upto-regularize

∀f:ℕ+ ⟶ ℤ. ∀k,m:ℕ.  ((↑regular-upto(k;m + 1;f)) ⇒ {∀n:ℕ. ((n ≤ m) ⇒ (regularize(k;f) n ~ f n))})
BY
{ (Auto
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN Unfold `regularize` 0
   THEN Reduce 0
   THEN (Subst' regular-upto(k;n;f) ~ tt 0 THENM (Reduce 0 THEN Auto))) }

1
.....equality..... 
1. f : ℕ+ ⟶ ℤ
2. k : ℕ
3. m : ℕ
4. ↑regular-upto(k;m + 1;f)
5. n : ℕ
6. n ≤ m
⊢ regular-upto(k;n;f) ~ tt

---

Latex:

---

Latex:
\mforall{}f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}k,m:\mBbbN{}.    ((\muparrow{}regular-upto(k;m  +  1;f))  {}\mRightarrow{}  \{\mforall{}n:\mBbbN{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (regularize(k;f)  n  \msim{}  f  n))\})


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unfold  `regularize`  0
  THEN  Reduce  0
  THEN  (Subst'  regular-upto(k;n;f)  \msim{}  tt  0  THENM  (Reduce  0  THEN  Auto)))

---

Home Index