---

Step * of Lemma regularize_wf

∀[k:ℕ+]. ∀[f:ℕ+ ⟶ ℤ].  (regularize(k;f) ∈ ℕ+ ⟶ ℤ)
BY
{ (Intros THEN Unfold `regularize` 0 THEN (MemCD THENA Auto) THEN (BoolCase ⌜regular-upto(k;n;f)⌝⋅ THENA Auto)) }

1
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. ↑regular-upto(k;n;f)
⊢ f n ∈ ℤ

2
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. ¬↑regular-upto(k;n;f)
⊢ eval m = mu(λn.(¬bregular-upto(k;n;f))) - 1 in
  eval j = seq-min-upper(k;m;f) in
    (n * ((f j) + (2 * k))) ÷ k * j ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].    (regularize(k;f)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})


By

---

Latex:
(Intros
  THEN  Unfold  `regularize`  0
  THEN  (MemCD  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}regular-upto(k;n;f)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index