---

Step * 1 of Lemma mFOL-abstract-functionality


1. Dom : Type
2. S : FOStruct(Dom)
3. name : Atom@i'
4. vars : ℤ List@i'
5. a1 : FOAssignment(Dom)@i'
6. a2 : FOAssignment(Dom)@i'
7. ∀z:ℤ. ((z ∈ mFOL-freevars(name(vars))) ⇒ ((a1 z) = (a2 z) ∈ Dom))@i'
⊢ Dom,S,a1 |= mFOL-abstract(name(vars)) = Dom,S,a2 |= mFOL-abstract(name(vars)) ∈ ℙ
BY
{ (RepUR ``mFOL-abstract FOSatWith AbstractFOAtomic`` 0 THEN EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
1. Dom : Type
2. S : FOStruct(Dom)
3. name : Atom@i'
4. vars : ℤ List@i'
5. a1 : FOAssignment(Dom)@i'
6. a2 : FOAssignment(Dom)@i'
7. ∀z:ℤ. ((z ∈ mFOL-freevars(name(vars))) ⇒ ((a1 z) = (a2 z) ∈ Dom))@i'
⊢ map(a1;vars) = map(a2;vars) ∈ (Dom List)

---

Latex:



1.  Dom  :  Type
2.  S  :  FOStruct(Dom)
3.  name  :  Atom@i'
4.  vars  :  \mBbbZ{}  List@i'
5.  a1  :  FOAssignment(Dom)@i'
6.  a2  :  FOAssignment(Dom)@i'
7.  \mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(name(vars)))  {}\mRightarrow{}  ((a1  z)  =  (a2  z)))@i'
\mvdash{}  Dom,S,a1  |=  mFOL-abstract(name(vars))  =  Dom,S,a2  |=  mFOL-abstract(name(vars))


By

(RepUR  ``mFOL-abstract  FOSatWith  AbstractFOAtomic``  0  THEN  EqCD  THEN  Auto)

---

Home Index