---

Step * of Lemma AbstractFOAtomic+_wf

∀[n:Atom]. ∀[L:ℤ List].  (AbstractFOAtomic+(n;L) ∈ AbstractFOFormula+(L))
BY
{ (Auto THEN Unfold `AbstractFOFormula+` 0 THEN (Assert L ∈ {z:ℤ| (z ∈ L)}  List BY Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n:Atom].  \mforall{}[L:\mBbbZ{}  List].    (AbstractFOAtomic+(n;L)  \mmember{}  AbstractFOFormula+(L))


By

---

Latex:
(Auto
  THEN  Unfold  `AbstractFOFormula+`  0
  THEN  (Assert  L  \mmember{}  \{z:\mBbbZ{}|  (z  \mmember{}  L)\}    List  BY
                          Auto)
  THEN  ProveWfLemma)

---

Home Index