---

Step * of Lemma enum-fin-seq-true

∀m:ℕ. ((λx.tt) = enum-fin-seq(m)[0] ∈ (ℕ ⟶ 𝔹))
BY
{ (InductionOnNat THEN RepUR ``enum-fin-seq`` 0 THEN Auto) }

1
1. m : ℤ
2. 0 < m
3. (λx.tt) = enum-fin-seq(m - 1)[0] ∈ (ℕ ⟶ 𝔹)
⊢ (λx.tt)
= primrec(m;[λx.tt];λi,r. (map(λs,x. if x=i  then tt  else (s x);r) @ map(λs,x. if x=i  then ff  else (s x);r)))[0]
∈ (ℕ ⟶ 𝔹)

---

Latex:

---

Latex:
\mforall{}m:\mBbbN{}.  ((\mlambda{}x.tt)  =  enum-fin-seq(m)[0])


By

---

Latex:
(InductionOnNat  THEN  RepUR  ``enum-fin-seq``  0  THEN  Auto)

---

Home Index