Step
*
2
1
2
1
1
1
1
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. ∀[i:ℕ]. ¬↑¬bregular-upto(k;i;f) supposing i < v
10. ¬(v = 0 ∈ ℤ)
11. v = 1 ∈ ℤ
12. i : ℤ
13. j : ℤ
14. i = 0 ∈ ℤ
15. j = 0 ∈ ℤ
⊢ |0| ≤ ((2 * k) * 2)
BY
{ (Reduce 0 THEN Auto) }
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. \mforall{}[i:\mBbbN{}]. \mneg{}\muparrow{}\mneg{}\msubb{}regular-upto(k;i;f) supposing i < v
10. \mneg{}(v = 0)
11. v = 1
12. i : \mBbbZ{}
13. j : \mBbbZ{}
14. i = 0
15. j = 0
\mvdash{} |0| \mleq{} ((2 * k) * 2)
By
Latex:
(Reduce 0 THEN Auto)
Home
Index