---

Step * 1 1 of Lemma m-regularize_wf_finite


1. X : Type
2. d : metric(X)
3. b : ℕ
4. s : ℕb ⟶ X
5. n : ℕb
6. 0 < first-m-not-reg(d;s;n + 1)
7. first-m-not-reg(d;s;n + 1) = 0 ∈ ℤ ⇐⇒ ∀n:ℕn + 1. m-not-reg(d;s;n) = ff
8. let i = first-m-not-reg(d;s;n + 1) - 1 in
       (∀n:ℕi. m-not-reg(d;s;n) = ff) ∧ m-not-reg(d;s;i) = tt
⊢ first-m-not-reg(d;s;n + 1) - 2 ∈ ℕb
BY
{ ((MoveToConcl (-1) THEN MoveToConcl (-2))
   THEN (GenConclTerm ⌜first-m-not-reg(d;s;n + 1)⌝⋅ THENA Auto)
   THEN RepUR ``let`` 0
   THEN CaseNat 1 `v'
   THEN Auto) }

1
1. X : Type
2. d : metric(X)
3. b : ℕ
4. s : ℕb ⟶ X
5. n : ℕb
6. (first-m-not-reg(d;s;n + 1) = 0 ∈ ℤ) ⇒ (∀n:ℕn + 1. m-not-reg(d;s;n) = ff)
7. (first-m-not-reg(d;s;n + 1) = 0 ∈ ℤ) ⇐ ∀n:ℕn + 1. m-not-reg(d;s;n) = ff
8. v : ℕ(n + 1) + 1
9. first-m-not-reg(d;s;n + 1) = v ∈ ℕ(n + 1) + 1
10. v = 1 ∈ ℤ
11. 0 < 1
12. ∀n:ℕ1 - 1. m-not-reg(d;s;n) = ff
13. m-not-reg(d;s;1 - 1) = tt
⊢ 1 - 2 ∈ ℕb

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  b  :  \mBbbN{}
4.  s  :  \mBbbN{}b  {}\mrightarrow{}  X
5.  n  :  \mBbbN{}b
6.  0  <  first-m-not-reg(d;s;n  +  1)
7.  first-m-not-reg(d;s;n  +  1)  =  0  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}n  +  1.  m-not-reg(d;s;n)  =  ff
8.  let  i  =  first-m-not-reg(d;s;n  +  1)  -  1  in
              (\mforall{}n:\mBbbN{}i.  m-not-reg(d;s;n)  =  ff)  \mwedge{}  m-not-reg(d;s;i)  =  tt
\mvdash{}  first-m-not-reg(d;s;n  +  1)  -  2  \mmember{}  \mBbbN{}b


By

---

Latex:
((MoveToConcl  (-1)  THEN  MoveToConcl  (-2))
  THEN  (GenConclTerm  \mkleeneopen{}first-m-not-reg(d;s;n  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``let``  0
  THEN  CaseNat  1  `v'
  THEN  Auto)

---

Home Index