---

Step * 1 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. (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
BY
{ (Reduce -1 THEN (Assert m-not-reg(d;s;0) = ff BY (Computation THEN Auto)) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Reduce  -1  THEN  (Assert  m-not-reg(d;s;0)  =  ff  BY  (Computation  THEN  Auto))  THEN  Auto)

---

Home Index