---

Step * of Lemma regularize-2-regular

∀f:ℤ ⟶ ℤ. 2-regular-seq(regularize(f))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN RepUR ``regularize`` 0
   THEN RepeatFor 2 (AutoSplit)
   THEN Try (((InstLemma `mu-property` [⌜λn.(¬bregular-upto(n;f))⌝]⋅
               THENA (Auto THEN Reduce 0 THEN RW assert_pushdownC 0 THEN Complete (Auto))
               )
              THEN Reduce (-1)
              THEN MoveToConcl (-1)
              THEN (GenConclTerm ⌜mu(λn.(¬bregular-upto(n;f)))⌝⋅
                    THENA (Auto THEN Reduce 0 THEN RW assert_pushdownC 0 THEN Auto)
                    )
              THEN Thin (-1)
              THEN (D 0 THENA Auto)
              THEN (RW assert_pushdownC (-1)  THENA Auto)
              THEN (Assert ¬(v = 1 ∈ ℤ) BY
                          (D 0
                           THEN Auto
                           THEN D -3
                           THEN HypSubst' (-1) 0
                           THEN RWO "assert-regular-upto" 0
                           THEN Auto
                           THEN (Subst' i ~ 1 0 THENA Auto)
                           THEN (Subst' j ~ 1 0 THENA Auto)
                           THEN RW IntNormC 0
                           THEN Auto
                           THEN RepUR ``absval`` 0
                           THEN Auto))
              THEN (CallByValueReduce 0 THENA Auto)
              THEN D -2
              THEN (Assert ¬(v = 0 ∈ ℤ) BY
                          ((D 0 THENA Auto)
                           THEN D -4
                           THEN HypSubst' (-1) 0 
                           THEN (RWO "assert-regular-upto" 0 THENA Auto)
                           THEN Auto))
              THEN (GenConcl ⌜(v - 1) = k ∈ ℕ+⌝⋅ THENA Auto)))) }

1
1. f : ℤ ⟶ ℤ@i
2. n : ℕ+@i
3. m : ℕ+@i
4. ↑regular-upto(n;f)
5. ↑regular-upto(m;f)
⊢ |(m * (f n)) - n * (f m)| ≤ (4 * (n + m))

2
1. f : ℤ ⟶ ℤ@i
2. n : ℕ+@i
3. m : ℕ+@i
4. ¬↑regular-upto(m;f)
5. ↑regular-upto(n;f)
6. v : ℕ@i
7. ¬↑regular-upto(v;f)@i
8. ∀[i:ℕ]. ¬¬↑regular-upto(i;f) supposing i < v@i
9. ¬(v = 1 ∈ ℤ)
10. ¬(v = 0 ∈ ℤ)
11. k : ℕ+@i
12. (v - 1) = k ∈ ℕ+@i
⊢ |(m * (f n)) - n * ((m * (f k)) ÷ k)| ≤ (4 * (n + m))

3
1. f : ℤ ⟶ ℤ@i
2. n : ℕ+@i
3. ¬↑regular-upto(n;f)
4. m : ℕ+@i
5. ↑regular-upto(m;f)
6. v : ℕ@i
7. ¬↑regular-upto(v;f)@i
8. ∀[i:ℕ]. ¬¬↑regular-upto(i;f) supposing i < v@i
9. ¬(v = 1 ∈ ℤ)
10. ¬(v = 0 ∈ ℤ)
11. k : ℕ+@i
12. (v - 1) = k ∈ ℕ+@i
⊢ |(m * ((n * (f k)) ÷ k)) - n * (f m)| ≤ (4 * (n + m))

4
1. f : ℤ ⟶ ℤ@i
2. n : ℕ+@i
3. ¬↑regular-upto(n;f)
4. m : ℕ+@i
5. ¬↑regular-upto(m;f)
6. v : ℕ@i
7. ¬↑regular-upto(v;f)@i
8. ∀[i:ℕ]. ¬¬↑regular-upto(i;f) supposing i < v@i
9. ¬(v = 1 ∈ ℤ)
10. ¬(v = 0 ∈ ℤ)
11. k : ℕ+@i
12. (v - 1) = k ∈ ℕ+@i
⊢ |(m * ((n * (f k)) ÷ k)) - n * ((m * (f k)) ÷ k)| ≤ (4 * (n + m))

---

Latex:

---

Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  2-regular-seq(regularize(f))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``regularize``  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Try  (((InstLemma  `mu-property`  [\mkleeneopen{}\mlambda{}n.(\mneg{}\msubb{}regular-upto(n;f))\mkleeneclose{}]\mcdot{}
                          THENA  (Auto  THEN  Reduce  0  THEN  RW  assert\_pushdownC  0  THEN  Complete  (Auto))
                          )
                        THEN  Reduce  (-1)
                        THEN  MoveToConcl  (-1)
                        THEN  (GenConclTerm  \mkleeneopen{}mu(\mlambda{}n.(\mneg{}\msubb{}regular-upto(n;f)))\mkleeneclose{}\mcdot{}
                                    THENA  (Auto  THEN  Reduce  0  THEN  RW  assert\_pushdownC  0  THEN  Auto)
                                    )
                        THEN  Thin  (-1)
                        THEN  (D  0  THENA  Auto)
                        THEN  (RW  assert\_pushdownC  (-1)    THENA  Auto)
                        THEN  (Assert  \mneg{}(v  =  1)  BY
                                                (D  0
                                                  THEN  Auto
                                                  THEN  D  -3
                                                  THEN  HypSubst'  (-1)  0
                                                  THEN  RWO  "assert-regular-upto"  0
                                                  THEN  Auto
                                                  THEN  (Subst'  i  \msim{}  1  0  THENA  Auto)
                                                  THEN  (Subst'  j  \msim{}  1  0  THENA  Auto)
                                                  THEN  RW  IntNormC  0
                                                  THEN  Auto
                                                  THEN  RepUR  ``absval``  0
                                                  THEN  Auto))
                        THEN  (CallByValueReduce  0  THENA  Auto)
                        THEN  D  -2
                        THEN  (Assert  \mneg{}(v  =  0)  BY
                                                ((D  0  THENA  Auto)
                                                  THEN  D  -4
                                                  THEN  HypSubst'  (-1)  0 
                                                  THEN  (RWO  "assert-regular-upto"  0  THENA  Auto)
                                                  THEN  Auto))
                        THEN  (GenConcl  \mkleeneopen{}(v  -  1)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto))))

---

Home Index