---

Step * of Lemma bool-size_wf

∀[k:ℕ]. ∀[f:ℕk ⟶ 𝔹].  (𝔹size(k;f) ∈ ℕk + 1)
BY
{ xxx(xxxInductionOnNatxxx
      THEN Unfold `bool-size` 0
      THEN (RWO "primrec-unroll" 0 THENA Auto)
      THEN Reduce 0
      THEN Try (xxxFold `bool-size` 0xxx))xxx }

1
1. k : ℤ
⊢ ∀[f:ℕ0 ⟶ 𝔹]. (0 ∈ ℕ1)

2
1. k : ℤ
2. 0 < k
3. ∀[f:ℕk - 1 ⟶ 𝔹]. (𝔹size(k - 1;f) ∈ ℕ(k - 1) + 1)
⊢ ∀[f:ℕk ⟶ 𝔹]. (if (k =z 0) then 0 else if f (k - 1) then 1 else 0 fi  + 𝔹size(k - 1;f) fi  ∈ ℕk + 1)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[f:\mBbbN{}k  {}\mrightarrow{}  \mBbbB{}].    (\mBbbB{}size(k;f)  \mmember{}  \mBbbN{}k  +  1)


By

---

Latex:
xxx(xxxInductionOnNatxxx
        THEN  Unfold  `bool-size`  0
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  Reduce  0
        THEN  Try  (xxxFold  `bool-size`  0xxx))xxx

---

Home Index