Step
*
of Lemma
enum-fin-seq-max2_wf
∀[M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ?)]. ∀[m:ℕ]. (enum-fin-seq-max2(M;m) ∈ ℕ)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``enum-fin-seq-max2`` 0 THEN MemTypeCD THEN Auto) }
1
.....set predicate.....
1. M : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ?)
2. m : ℕ
⊢ 0 ≤ imax-list(map(λs.case M m s of inl(k) => k + 1 | inr(x) => 0;enum-fin-seq(m)))
Latex:
Latex:
\mforall{}[M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} (\mBbbN{}?)]. \mforall{}[m:\mBbbN{}]. (enum-fin-seq-max2(M;m) \mmember{} \mBbbN{})
By
Latex:
((UnivCD THENA Auto) THEN RepUR ``enum-fin-seq-max2`` 0 THEN MemTypeCD THEN Auto)
Home
Index