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