---

Step * of Lemma num-digits_wf

∀[k:ℕ]. (num-digits(k) ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} )
BY
{ (Auto THEN MoveToConcl (-1) THEN CompleteInductionOnNat THEN RecUnfold `num-digits` 0 THEN AutoSplit) }

1
1. k : ℕ
2. ∀k:ℕk. (num-digits(k) ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} )
3. k < 10
⊢ 1 ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} 

2
1. k : ℕ
2. ¬k < 10
3. ∀k:ℕk. (num-digits(k) ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} )
⊢ eval k' = k ÷ 10 in
  1 + num-digits(k') ∈ {n:ℕ+| ((10^n - 1 ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} 

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  (num-digits(k)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  ((10\^{}n  -  1  \mleq{}  k)  \mvee{}  (k  =  0))  \mwedge{}  k  <  10\^{}n\}  )


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  CompleteInductionOnNat
  THEN  RecUnfold  `num-digits`  0
  THEN  AutoSplit)

---

Home Index