---

Step * of Lemma mFOL-abstract_wf

∀[fmla:mFOL()]. (mFOL-abstract(fmla) ∈ AbstractFOFormula(mFOL-freevars(fmla)))
BY
{ xxx((D 0 THENA Auto) THEN SimpleDatatypeInduction 1⋅)xxx }

1
1. sz : ℕ
2. ∀sz:ℕsz. ∀fmla:mFOL().  mFOL-abstract(fmla) ∈ AbstractFOFormula(mFOL-freevars(fmla)) supposing mFOL_size(fmla) ≤ sz
3. name : Atom
4. f2 : ℤ List
5. 0 ≤ sz
⊢ mFOL-abstract(name(f2)) ∈ AbstractFOFormula(mFOL-freevars(name(f2)))

2
1. knd : Atom
2. left : mFOL()
3. f3 : mFOL()
4. mFOL-abstract(f3) ∈ AbstractFOFormula(mFOL-freevars(f3))
5. mFOL-abstract(left) ∈ AbstractFOFormula(mFOL-freevars(left))
⊢ mFOL-abstract(mFOconnect(knd;left;f3)) ∈ AbstractFOFormula(mFOL-freevars(mFOconnect(knd;left;f3)))

3
1. isall : 𝔹
2. var : ℤ
3. f3 : mFOL()
4. mFOL-abstract(f3) ∈ AbstractFOFormula(mFOL-freevars(f3))
⊢ mFOL-abstract(mFOquant(isall;var;f3)) ∈ AbstractFOFormula(mFOL-freevars(mFOquant(isall;var;f3)))

---

Latex:

---

Latex:
\mforall{}[fmla:mFOL()].  (mFOL-abstract(fmla)  \mmember{}  AbstractFOFormula(mFOL-freevars(fmla)))


By

---

Latex:
xxx((D  0  THENA  Auto)  THEN  SimpleDatatypeInduction  1\mcdot{})xxx

---

Home Index