Step * of Lemma code-seq1_wf

[k:ℕ]. ∀[s:ℕk ⟶ ℕ].  (code-seq1(k;s) ∈ ℕ)
BY
xxxProveWfLemmaxxx }


Latex:


Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}].    (code-seq1(k;s)  \mmember{}  \mBbbN{})


By


Latex:
xxxProveWfLemmaxxx




Home Index