Step
*
of Lemma
enum-fin-seq-max_wf
∀[M:(ℕ ⟶ 𝔹) ⟶ ℕ]. ∀[m:ℕ]. (enum-fin-seq-max(M;m) ∈ ℕ)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``enum-fin-seq-max`` 0 THEN MemTypeCD THEN Auto) }
1
.....set predicate.....
1. M : (ℕ ⟶ 𝔹) ⟶ ℕ
2. m : ℕ
⊢ 0 ≤ imax-list(map(λs.(M s);enum-fin-seq(m)))
Latex:
Latex:
\mforall{}[M:(\mBbbN{} {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} \mBbbN{}]. \mforall{}[m:\mBbbN{}]. (enum-fin-seq-max(M;m) \mmember{} \mBbbN{})
By
Latex:
((UnivCD THENA Auto) THEN RepUR ``enum-fin-seq-max`` 0 THEN MemTypeCD THEN Auto)
Home
Index