Step
*
of Lemma
coded-seq_wf
∀x:ℕ. (coded-seq(x) ∈ k:ℕ × (ℕk ⟶ ℕ))
BY
{ xxxProveWfLemmaxxx }
Latex:
Latex:
\mforall{}x:\mBbbN{}.  (coded-seq(x)  \mmember{}  k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}))
By
Latex:
xxxProveWfLemmaxxx
Home
Index