---

Step * 1 of Lemma m-regularize-of-regular


1. X : Type
2. d : metric(X)
3. s : ℕ ⟶ X
4. m-k-regular(d;2;s)
5. ∀n:ℕ. m-not-reg(d;s;n) = ff
6. x : ℕ
⊢ (m-regularize(d;s) x) = (s x) ∈ X
BY
{ (RepUR ``m-regularize`` 0
   THEN (InstLemma `first-m-not-reg-property` [⌜X⌝;⌜d⌝;⌜x + 1⌝;⌜s⌝]⋅ THENA Auto)
   THEN Subst' first-m-not-reg(d;s;x + 1) = 0 ∈ ℤ 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  s  :  \mBbbN{}  {}\mrightarrow{}  X
4.  m-k-regular(d;2;s)
5.  \mforall{}n:\mBbbN{}.  m-not-reg(d;s;n)  =  ff
6.  x  :  \mBbbN{}
\mvdash{}  (m-regularize(d;s)  x)  =  (s  x)


By

---

Latex:
(RepUR  ``m-regularize``  0
  THEN  (InstLemma  `first-m-not-reg-property`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x  +  1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Subst'  first-m-not-reg(d;s;x  +  1)  =  0  0
  THEN  Auto)

---

Home Index