Step
*
of Lemma
AbstractFOAtomic_wf
∀[n:Atom]. ∀[L:ℤ List]. (AbstractFOAtomic(n;L) ∈ AbstractFOFormula)
BY
{ (Unfold `AbstractFOFormula` 0 THEN ProveWfLemma) }
Latex:
\mforall{}[n:Atom]. \mforall{}[L:\mBbbZ{} List]. (AbstractFOAtomic(n;L) \mmember{} AbstractFOFormula)
By
(Unfold `AbstractFOFormula` 0 THEN ProveWfLemma)
Home
Index