---

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