---

Step * 2 of Lemma bool-size_wf


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)
BY
{ (ParallelLast THEN xxx(Auto' THEN SplitOnConclITE THEN Auto')xxx) }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}[f:\mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbB{}].  (\mBbbB{}size(k  -  1;f)  \mmember{}  \mBbbN{}(k  -  1)  +  1)
\mvdash{}  \mforall{}[f:\mBbbN{}k  {}\mrightarrow{}  \mBbbB{}]
        (if  (k  =\msubz{}  0)  then  0  else  if  f  (k  -  1)  then  1  else  0  fi    +  \mBbbB{}size(k  -  1;f)  fi    \mmember{}  \mBbbN{}k  +  1)


By

---

Latex:
(ParallelLast  THEN  xxx(Auto'  THEN  SplitOnConclITE  THEN  Auto')xxx)

---

Home Index