---

Step * of Lemma regularize-regular

No Annotations
∀k:ℕ+. ∀x:{f:ℕ+ ⟶ ℤ| k-regular-seq(f)} .  (regularize(k;x) = x ∈ (ℕ+ ⟶ ℤ))
BY
{ ((Auto THEN D -1)
   THEN (Ext THENA Auto)
   THEN RenameVar `n' (-1)
   THEN InstLemma `regular-upto-regularize` [⌜x⌝;⌜k⌝;⌜n⌝]⋅
   THEN Auto
   THEN (Unfold `regular-int-seq` 3 THEN Reduce 3)
   THEN RWO "assert-regular-upto" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}x:\{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  k-regular-seq(f)\}  .    (regularize(k;x)  =  x)


By

---

Latex:
((Auto  THEN  D  -1)
  THEN  (Ext  THENA  Auto)
  THEN  RenameVar  `n'  (-1)
  THEN  InstLemma  `regular-upto-regularize`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (Unfold  `regular-int-seq`  3  THEN  Reduce  3)
  THEN  RWO  "assert-regular-upto"  0
  THEN  Auto)

---

Home Index