---

Step * 2 of Lemma regularize_wf


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 ∈ ℤ
BY
{ ((Assert ∃n:ℕ. (↑((λn.(¬bregular-upto(k;n;f))) n)) BY
          (Reduce 0⋅ THEN RW assert_pushdownC 0 THEN Auto))
   THEN DupHyp (-1)
   THEN Reduce -1
   THEN (InstLemma `mu-property` [⌜λn.(¬bregular-upto(k;n;f))⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜mu(λn.(¬bregular-upto(k;n;f)))⌝⋅ THENA Auto)
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN D -1) }

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. ↑¬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 ∈ ℤ

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}\msupplus{}
4.  \mneg{}\muparrow{}regular-upto(k;n;f)
\mvdash{}  eval  m  =  mu(\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;n;f)))  -  1  in
    eval  j  =  seq-min-upper(k;m;f)  in
        (n  *  ((f  j)  +  (2  *  k)))  \mdiv{}  k  *  j  \mmember{}  \mBbbZ{}


By

---

Latex:
((Assert  \mexists{}n:\mBbbN{}.  (\muparrow{}((\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;n;f)))  n))  BY
                (Reduce  0\mcdot{}  THEN  RW  assert\_pushdownC  0  THEN  Auto))
  THEN  DupHyp  (-1)
  THEN  Reduce  -1
  THEN  (InstLemma  `mu-property`  [\mkleeneopen{}\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;n;f))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}mu(\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;n;f)))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  D  -1)

---

Home Index