---

Step * 2 1 2 1 of Lemma regularize_wf


1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. ¬↑regular-upto(k;n;f)
5. ∃n:ℕ. (↑((λn.(¬bregular-upto(k;n;f))) n))
6. ∃n:ℕ. (↑¬bregular-upto(k;n;f))
7. v : ℕ
8. mu(λn.(¬bregular-upto(k;n;f))) = v ∈ ℕ
9. ¬↑regular-upto(k;v;f)
10. ∀[i:ℕ]. ¬↑¬bregular-upto(k;i;f) supposing i < v
11. ¬(v = 0 ∈ ℤ)
12. v = 1 ∈ ℤ
⊢ eval m = 1 - 1 in
  eval j = seq-min-upper(k;m;f) in
    (n * ((f j) + (2 * k))) ÷ k * j ∈ ℤ
BY
{ (D -4 THEN HypSubst' (-1) 0) }

1
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. ¬↑regular-upto(k;n;f)
5. ∃n:ℕ. (↑((λn.(¬bregular-upto(k;n;f))) n))
6. ∃n:ℕ. (↑¬bregular-upto(k;n;f))
7. v : ℕ
8. mu(λn.(¬bregular-upto(k;n;f))) = v ∈ ℕ
9. ∀[i:ℕ]. ¬↑¬bregular-upto(k;i;f) supposing i < v
10. ¬(v = 0 ∈ ℤ)
11. v = 1 ∈ ℤ
⊢ ↑regular-upto(k;1;f)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}\msupplus{}
4.  \mneg{}\muparrow{}regular-upto(k;n;f)
5.  \mexists{}n:\mBbbN{}.  (\muparrow{}((\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;n;f)))  n))
6.  \mexists{}n:\mBbbN{}.  (\muparrow{}\mneg{}\msubb{}regular-upto(k;n;f))
7.  v  :  \mBbbN{}
8.  mu(\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;n;f)))  =  v
9.  \mneg{}\muparrow{}regular-upto(k;v;f)
10.  \mforall{}[i:\mBbbN{}].  \mneg{}\muparrow{}\mneg{}\msubb{}regular-upto(k;i;f)  supposing  i  <  v
11.  \mneg{}(v  =  0)
12.  v  =  1
\mvdash{}  eval  m  =  1  -  1  in
    eval  j  =  seq-min-upper(k;m;f)  in
        (n  *  ((f  j)  +  (2  *  k)))  \mdiv{}  k  *  j  \mmember{}  \mBbbZ{}


By

---

Latex:
(D  -4  THEN  HypSubst'  (-1)  0)

---

Home Index