Proof of Nuprl Lemma : regularize-k-regular

Step * of Lemma regularize-k-regular

No Annotations
∀k:ℕ⁺. ∀f:ℕ⁺ ⟶ ℤ.  k-regular-seq(regularize(k;f))
BY
{ (Auto
   THEN (RWO "regular-int-seq-iff" 0 THEN Auto)
   THEN RepUR ``regularize`` 0
   THEN RepeatFor 2 (AutoSplit)
   THEN Try (((InstLemma `mu-property` [⌜λn.(¬_bregular-upto(k;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(k;n;f)))⌝⋅
                    THENA (Auto THEN Reduce 0 THEN RW assert_pushdownC 0 THEN Auto)
                    )
              THEN Thin (-1)
              THEN (D 0 THENA Auto)
              THEN D -1
              THEN (RW assert_pushdownC (-2)  THENA Auto)
              THEN (Assert ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v BY
                          (ParallelLast THEN RW assert_pushdownC (-1) THEN Auto))
              THEN Thin (-2)
              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 (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) = j ∈ ℕ⁺⌝⋅ THENA Auto)))) }

1
1. k : ℕ⁺
2. f : ℕ⁺ ⟶ ℤ
3. n : ℕ⁺
4. m : ℕ⁺
5. ↑regular-upto(k;n;f)
6. ↑regular-upto(k;m;f)
⊢ ∃z:ℝ

   ((((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((f n) + (2 * k))/r((2 * k) * n))))

∧ ((r((f m) - 2 * k)/r((2 * k) * m)) ≤ z)
∧ (z ≤ (r((f m) + (2 * k))/r((2 * k) * m))))

2
1. k : ℕ⁺
2. f : ℕ⁺ ⟶ ℤ
3. n : ℕ⁺
4. m : ℕ⁺
5. ¬↑regular-upto(k;m;f)
6. ↑regular-upto(k;n;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ⁺
13. (v - 1) = j ∈ ℕ⁺
⊢ ∃z@0:ℝ

   ((((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z@0) ∧ (z@0 ≤ (r((f n) + (2 * k))/r((2 * k) * n))))

∧ ((r(eval j = seq-min-upper(k;j;f) in
k * ((m * ((f j) + (2 * k))) ÷ j * k) - 2 * k)/r((2 * k) * m)) ≤ z@0)

   ∧ (z@0 ≤ (r(eval j = seq-min-upper(k;j;f) in k * ((m * ((f j) + (2 * k))) ÷ j * k) + (2 * k))/r((2 * k) * m))))

3
1. k : ℕ⁺
2. f : ℕ⁺ ⟶ ℤ
3. n : ℕ⁺
4. ¬↑regular-upto(k;n;f)
5. m : ℕ⁺
6. ↑regular-upto(k;m;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ⁺
13. (v - 1) = j ∈ ℕ⁺
⊢ ∃z@0:ℝ
((((r(eval j = seq-min-upper(k;j;f) in
k * ((n * ((f j) + (2 * k))) ÷ j * k) - 2 * k)/r((2 * k) * n)) ≤ z@0)

    ∧ (z@0 ≤ (r(eval j = seq-min-upper(k;j;f) in k * ((n * ((f j) + (2 * k))) ÷ j * k) + (2 * k))/r((2 * k) * n))))

   ∧ ((r((f m) - 2 * k)/r((2 * k) * m)) ≤ z@0)
   ∧ (z@0 ≤ (r((f m) + (2 * k))/r((2 * k) * m))))

4
1. k : ℕ⁺
2. f : ℕ⁺ ⟶ ℤ
3. n : ℕ⁺
4. ¬↑regular-upto(k;n;f)
5. m : ℕ⁺
6. ¬↑regular-upto(k;m;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ⁺
13. (v - 1) = j ∈ ℕ⁺
⊢ ∃z@0:ℝ
   ((((r(eval j = seq-min-upper(k;j;f) in
         k * ((n * ((f j) + (2 * k))) ÷ j * k) - 2 * k)/r((2 * k) * n)) ≤ z@0)

    ∧ (z@0 ≤ (r(eval j = seq-min-upper(k;j;f) in k * ((n * ((f j) + (2 * k))) ÷ j * k) + (2 * k))/r((2 * k) * n))))

∧ ((r(eval j = seq-min-upper(k;j;f) in
k * ((m * ((f j) + (2 * k))) ÷ j * k) - 2 * k)/r((2 * k) * m)) ≤ z@0)

   ∧ (z@0 ≤ (r(eval j = seq-min-upper(k;j;f) in k * ((m * ((f j) + (2 * k))) ÷ j * k) + (2 * k))/r((2 * k) * m))))

Latex:

Latex:
No Annotations \mforall{}k:\mBbbN{}\msupplus{}. \mforall{}f:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}. k-regular-seq(regularize(k;f)) By Latex: (Auto THEN (RWO "regular-int-seq-iff" 0 THEN Auto) THEN RepUR ``regularize`` 0 THEN RepeatFor 2 (AutoSplit) THEN Try (((InstLemma `mu-property` [\mkleeneopen{}\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;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(k;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 D -1 THEN (RW assert\_pushdownC (-2) THENA Auto) THEN (Assert \mforall{}[i:\mBbbN{}]. \mneg{}\mneg{}\muparrow{}regular-upto(k;i;f) supposing i < v BY (ParallelLast THEN RW assert\_pushdownC (-1) THEN Auto)) THEN Thin (-2) 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 (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) = j\mkleeneclose{}\mcdot{} THENA Auto)))) Home Index