---

Step * of Lemma FOQuantifier_wf

∀[vs:ℤ List]. ∀[isall:𝔹].
  (FOQuantifier(isall) ∈ z:ℤ ⟶ AbstractFOFormula(vs) ⟶ AbstractFOFormula(filter(λx.(¬b(x =z z));vs)))
BY
{ (Auto THEN Unfolds ``AbstractFOFormula`` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[vs:\mBbbZ{}  List].  \mforall{}[isall:\mBbbB{}].
    (FOQuantifier(isall)  \mmember{}  z:\mBbbZ{}
      {}\mrightarrow{}  AbstractFOFormula(vs)
      {}\mrightarrow{}  AbstractFOFormula(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));vs)))


By

---

Latex:
(Auto  THEN  Unfolds  ``AbstractFOFormula``  0  THEN  ProveWfLemma)

---

Home Index