Step * 1 1 1 of Lemma mFOL-abstract_wf


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
6. AbstractFOAtomic(name;f2) AbstractFOAtomic(name;f2) ∈ AbstractFOFormula(f2)
7. Dom Type
8. FOStruct(Dom)
⊢ f2 ⊆ remove-repeats(IntDeq;f2)
BY
(D THEN Auto) }


Latex:


Latex:

1.  sz  :  \mBbbN{}
2.  \mforall{}sz:\mBbbN{}sz.  \mforall{}fmla:mFOL().
          mFOL-abstract(fmla)  \mmember{}  AbstractFOFormula(mFOL-freevars(fmla))  supposing  mFOL\_size(fmla)  \mleq{}  sz
3.  name  :  Atom
4.  f2  :  \mBbbZ{}  List
5.  0  \mleq{}  sz
6.  AbstractFOAtomic(name;f2)  =  AbstractFOAtomic(name;f2)
7.  Dom  :  Type
8.  S  :  FOStruct(Dom)
\mvdash{}  f2  \msubseteq{}  remove-repeats(IntDeq;f2)


By


Latex:
(D  0  THEN  Auto)




Home Index