---

Step * of Lemma accelerate_wf

No Annotations
∀[k:ℕ+]. ∀[f:{f:ℕ+ ⟶ ℤ| k-regular-seq(f)} ].  (accelerate(k;f) ∈ ℝ)
BY
{ TACTIC:(Auto
          THEN D -1
          THEN (Assert accelerate(k;f) ∈ ℕ+ ⟶ ℤ BY
                      ProveWfLemma)
          THEN PromoteHyp (-1) 3
          THEN MemTypeCD
          THEN Auto) }

1
.....set predicate..... 
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. accelerate(k;f) ∈ ℕ+ ⟶ ℤ
4. k-regular-seq(f)
⊢ regular-seq(accelerate(k;f))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[f:\{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  k-regular-seq(f)\}  ].    (accelerate(k;f)  \mmember{}  \mBbbR{})


By

---

Latex:
TACTIC:(Auto
                THEN  D  -1
                THEN  (Assert  accelerate(k;f)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}  BY
                                        ProveWfLemma)
                THEN  PromoteHyp  (-1)  3
                THEN  MemTypeCD
                THEN  Auto)

---

Home Index