---

Step * 1 of Lemma FOL-abstract_wf


1. sz : ℕ
2. ∀sz:ℕsz. ∀fmla:mFOL().  FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla)) supposing mFOL_size(fmla) ≤ sz
3. name : Atom
4. f2 : ℤ List
5. 0 ≤ sz
⊢ FOL-abstract(name(f2)) ∈ AbstractFOFormula+(mFOL-freevars(name(f2)))
BY
{ (RepUR ``FOL-abstract mFOL-freevars`` 0 THEN DoSubsume THEN Auto) }

1
1. sz : ℕ
2. ∀sz:ℕsz. ∀fmla:mFOL().  FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla)) supposing mFOL_size(fmla) ≤ sz
3. name : Atom
4. f2 : ℤ List
5. 0 ≤ sz
6. AbstractFOAtomic+(name;f2) = AbstractFOAtomic+(name;f2) ∈ AbstractFOFormula+(f2)
⊢ AbstractFOFormula+(f2) ⊆r AbstractFOFormula+(remove-repeats(IntDeq;f2))

---

Latex:

---

Latex:

1.  sz  :  \mBbbN{}
2.  \mforall{}sz:\mBbbN{}sz.  \mforall{}fmla:mFOL().
          FOL-abstract(fmla)  \mmember{}  AbstractFOFormula+(mFOL-freevars(fmla))  supposing  mFOL\_size(fmla)  \mleq{}  sz
3.  name  :  Atom
4.  f2  :  \mBbbZ{}  List
5.  0  \mleq{}  sz
\mvdash{}  FOL-abstract(name(f2))  \mmember{}  AbstractFOFormula+(mFOL-freevars(name(f2)))


By

---

Latex:
(RepUR  ``FOL-abstract  mFOL-freevars``  0  THEN  DoSubsume  THEN  Auto)

---

Home Index