---

Step * of Lemma reg-seq-inv_wf

∀[b:ℕ+]. ∀[x:{f:ℕ+ ⟶ ℤ| b-regular-seq(f)} ]. ∀[k:ℕ+].
  reg-seq-inv(x) ∈ {f:ℕ+ ⟶ ℤ| b * ((k * k) + 1)-regular-seq(f)}  supposing ∀m:ℕ+. ((2 * m) ≤ (k * |x m|))
BY
{ ((Auto
    THEN D 2
    THEN (Assert ∀m:ℕ+. (¬((x m) = 0 ∈ ℤ)) BY
                (Auto
                 THEN SupposeNot
                 THEN (InstHyp [⌜m⌝] (-3)⋅ THENA Auto)
                 THEN (D 0 THENA Auto)
                 THEN Subst ⌜|x m| ~ 0⌝ (-2)⋅
                 THEN Auto)))
   THEN (Assert reg-seq-inv(x) ∈ ℕ+ ⟶ ℤ BY
               ProveWfLemma)
   THEN MemTypeCD
   THEN Auto
   THEN D 0
   THEN Auto) }

1
1. b : ℕ+
2. x : ℕ+ ⟶ ℤ
3. b-regular-seq(x)
4. k : ℕ+
5. ∀m:ℕ+. ((2 * m) ≤ (k * |x m|))
6. ∀m:ℕ+. (¬((x m) = 0 ∈ ℤ))
7. reg-seq-inv(x) ∈ ℕ+ ⟶ ℤ
8. n : ℕ+
9. m : ℕ+
⊢ |(m * (reg-seq-inv(x) n)) - n * (reg-seq-inv(x) m)| ≤ ((2 * b * ((k * k) + 1)) * (n + m))

---

Latex:

---

Latex:
\mforall{}[b:\mBbbN{}\msupplus{}].  \mforall{}[x:\{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  b-regular-seq(f)\}  ].  \mforall{}[k:\mBbbN{}\msupplus{}].
    reg-seq-inv(x)  \mmember{}  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  b  *  ((k  *  k)  +  1)-regular-seq(f)\}    supposing  \mforall{}m:\mBbbN{}\msupplus{}.  ((2  *  m)  \mleq{}  (k  *  |\000Cx  m|))


By

---

Latex:
((Auto
    THEN  D  2
    THEN  (Assert  \mforall{}m:\mBbbN{}\msupplus{}.  (\mneg{}((x  m)  =  0))  BY
                            (Auto
                              THEN  SupposeNot
                              THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
                              THEN  (D  0  THENA  Auto)
                              THEN  Subst  \mkleeneopen{}|x  m|  \msim{}  0\mkleeneclose{}  (-2)\mcdot{}
                              THEN  Auto)))
  THEN  (Assert  reg-seq-inv(x)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}  BY
                          ProveWfLemma)
  THEN  MemTypeCD
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index