---

Step * 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. ↑¬bregular-upto(k;v;f)
10. ∀[i:ℕ]. ¬↑¬bregular-upto(k;i;f) supposing i < v
⊢ eval m = v - 1 in
  eval j = seq-min-upper(k;m;f) in
    (n * ((f j) + (2 * k))) ÷ k * j ∈ ℤ
BY
{ ((RW assert_pushdownC (-2) THENA Auto) THEN CaseNat 0 `v') }

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. ¬↑regular-upto(k;v;f)
10. ∀[i:ℕ]. ¬↑¬bregular-upto(k;i;f) supposing i < v
11. v = 0 ∈ ℤ
⊢ eval m = 0 - 1 in
  eval j = seq-min-upper(k;m;f) in
    (n * ((f j) + (2 * k))) ÷ k * j ∈ ℤ

2
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 ∈ ℤ)
⊢ eval m = v - 1 in
  eval j = seq-min-upper(k;m;f) in
    (n * ((f j) + (2 * k))) ÷ k * j ∈ ℤ

---

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.  \muparrow{}\mneg{}\msubb{}regular-upto(k;v;f)
10.  \mforall{}[i:\mBbbN{}].  \mneg{}\muparrow{}\mneg{}\msubb{}regular-upto(k;i;f)  supposing  i  <  v
\mvdash{}  eval  m  =  v  -  1  in
    eval  j  =  seq-min-upper(k;m;f)  in
        (n  *  ((f  j)  +  (2  *  k)))  \mdiv{}  k  *  j  \mmember{}  \mBbbZ{}


By

---

Latex:
((RW  assert\_pushdownC  (-2)  THENA  Auto)  THEN  CaseNat  0  `v')

---

Home Index