Step
*
of Lemma
consistent-model-fun_wf
∀[Gamma:mFOL() List]. ∀[x:ℕ]. ∀[L:(ℕ × ℕ) List].  (consistent-model-fun(Gamma;x;L) ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[Gamma:mFOL()  List].  \mforall{}[x:\mBbbN{}].  \mforall{}[L:(\mBbbN{}  \mtimes{}  \mBbbN{})  List].    (consistent-model-fun(Gamma;x;L)  \mmember{}  \mBbbP{})
By
Latex:
ProveWfLemma
Home
Index