Step * 1 1 1 of Lemma m-regularize_wf_finite


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