---

Step * 2 of Lemma num-digits_wf


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} 
BY
{ (CallByValueReduce 0 THENA Auto) }

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

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  \mneg{}k  <  10
3.  \mforall{}k:\mBbbN{}k.  (num-digits(k)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  ((10\^{}n  -  1  \mleq{}  k)  \mvee{}  (k  =  0))  \mwedge{}  k  <  10\^{}n\}  )
\mvdash{}  eval  k'  =  k  \mdiv{}  10  in
    1  +  num-digits(k')  \mmember{}  \{n:\mBbbN{}\msupplus{}|  ((10\^{}n  -  1  \mleq{}  k)  \mvee{}  (k  =  0))  \mwedge{}  k  <  10\^{}n\} 


By

---

Latex:
(CallByValueReduce  0  THENA  Auto)

---

Home Index