---

Step * 1 1 1 2 1 of Lemma CCC-finite


1. k : ℕ
2. ∀m:ℕ3. CCC(ℕm)
⊢ CCC(ℕ2^k)
BY
{ NatInd 1 }

1
.....basecase..... 
1. ∀m:ℕ3. CCC(ℕm)
⊢ CCC(ℕ2^0)

2
.....upcase..... 
1. ∀m:ℕ3. CCC(ℕm)
2. k : ℤ
3. [%4] : 0 < k
4. CCC(ℕ2^(k - 1))
⊢ CCC(ℕ2^k)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  \mforall{}m:\mBbbN{}3.  CCC(\mBbbN{}m)
\mvdash{}  CCC(\mBbbN{}2\^{}k)


By

---

Latex:
NatInd  1

---

Home Index