Step
*
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)
⊢ first-m-not-reg(d;s;n + 1) - 2 ∈ ℕb
BY
{ ((InstLemma `first-m-not-reg-property` [⌜X⌝;⌜d⌝;⌜n + 1⌝;⌜s⌝]⋅ THENA Auto) THEN ExRepD THEN ThinTrivial) }
1
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
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)
\mvdash{} first-m-not-reg(d;s;n + 1) - 2 \mmember{} \mBbbN{}b
By
Latex:
((InstLemma `first-m-not-reg-property` [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}n + 1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{} THENA Auto)
THEN ExRepD
THEN ThinTrivial)
Home
Index