Step
*
1
1
2
of Lemma
enum-fin-seq-true
1. m : ℤ
2. m ≠ 0
3. 0 < m
4. (λx.tt) = enum-fin-seq(m - 1)[0] ∈ (ℕ ⟶ 𝔹)
⊢ (λx.tt)
= map(λs,x. if x=m - 1 then tt else (s x);primrec(m - 1;[λ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]
∈ (ℕ ⟶ 𝔹)
BY
{ Fold `enum-fin-seq` 0 }
1
1. m : ℤ
2. m ≠ 0
3. 0 < m
4. (λx.tt) = enum-fin-seq(m - 1)[0] ∈ (ℕ ⟶ 𝔹)
⊢ (λx.tt) = map(λs,x. if x=m - 1 then tt else (s x);enum-fin-seq(m - 1))[0] ∈ (ℕ ⟶ 𝔹)
Latex:
Latex:
1. m : \mBbbZ{}
2. m \mneq{} 0
3. 0 < m
4. (\mlambda{}x.tt) = enum-fin-seq(m - 1)[0]
\mvdash{} (\mlambda{}x.tt)
= map(\mlambda{}s,x. if x=m - 1 then tt else (s x);primrec(m - 1;[\mlambda{}x.tt];\mlambda{}i,r. (map(\mlambda{}s,x. if x=i
then tt
else (s x);r)
@ map(\mlambda{}s,x. if x=i
then ff
else (s x);r))))[0\000C]
By
Latex:
Fold `enum-fin-seq` 0
Home
Index