---

Step * of Lemma mFOL-abstract-functionality

∀[fmla:mFOL()]. ∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a1,a2:FOAssignment(Dom)].
  Dom,S,a1 |= mFOL-abstract(fmla) = Dom,S,a2 |= mFOL-abstract(fmla) ∈ ℙ 
  supposing ∀z:ℤ. ((z ∈ mFOL-freevars(fmla)) ⇒ ((a1 z) = (a2 z) ∈ Dom))
BY
{ (Auto
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN MoveToConcl 1
   THEN BLemmaUp `mFOL-induction`
   THEN At ⌈𝕌'⌉ Auto⋅
   THEN Auto) }

1
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)) ∈ ℙ

2
1. Dom : Type
2. S : FOStruct(Dom)
3. knd : Atom@i'
4. left : mFOL()@i'
5. right : mFOL()@i'
6. ∀a1,a2:FOAssignment(Dom).
     ((∀z:ℤ. ((z ∈ mFOL-freevars(left)) ⇒ ((a1 z) = (a2 z) ∈ Dom)))
     ⇒ (Dom,S,a1 |= mFOL-abstract(left) = Dom,S,a2 |= mFOL-abstract(left) ∈ ℙ))@i'
7. ∀a1,a2:FOAssignment(Dom).
     ((∀z:ℤ. ((z ∈ mFOL-freevars(right)) ⇒ ((a1 z) = (a2 z) ∈ Dom)))
     ⇒ (Dom,S,a1 |= mFOL-abstract(right) = Dom,S,a2 |= mFOL-abstract(right) ∈ ℙ))@i'
8. a1 : FOAssignment(Dom)@i'
9. a2 : FOAssignment(Dom)@i'
10. ∀z:ℤ. ((z ∈ mFOL-freevars(mFOconnect(knd;left;right))) ⇒ ((a1 z) = (a2 z) ∈ Dom))@i'
⊢ Dom,S,a1 |= mFOL-abstract(mFOconnect(knd;left;right)) = Dom,S,a2 |= mFOL-abstract(mFOconnect(knd;left;right)) ∈ ℙ

3
1. Dom : Type
2. S : FOStruct(Dom)
3. isall : 𝔹@i'
4. var : ℤ@i'
5. body : mFOL()@i'
6. ∀a1,a2:FOAssignment(Dom).
     ((∀z:ℤ. ((z ∈ mFOL-freevars(body)) ⇒ ((a1 z) = (a2 z) ∈ Dom)))
     ⇒ (Dom,S,a1 |= mFOL-abstract(body) = Dom,S,a2 |= mFOL-abstract(body) ∈ ℙ))@i'
7. a1 : FOAssignment(Dom)@i'
8. a2 : FOAssignment(Dom)@i'
9. ∀z:ℤ. ((z ∈ mFOL-freevars(mFOquant(isall;var;body))) ⇒ ((a1 z) = (a2 z) ∈ Dom))@i'
⊢ Dom,S,a1 |= mFOL-abstract(mFOquant(isall;var;body)) = Dom,S,a2 |= mFOL-abstract(mFOquant(isall;var;body)) ∈ ℙ

---

Latex:


\mforall{}[fmla:mFOL()].  \mforall{}[Dom:Type].  \mforall{}[S:FOStruct(Dom)].  \mforall{}[a1,a2:FOAssignment(Dom)].
    Dom,S,a1  |=  mFOL-abstract(fmla)  =  Dom,S,a2  |=  mFOL-abstract(fmla) 
    supposing  \mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(fmla))  {}\mRightarrow{}  ((a1  z)  =  (a2  z)))


By

(Auto
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  MoveToConcl  1
  THEN  BLemmaUp  `mFOL-induction`
  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  Auto\mcdot{}
  THEN  Auto)

---

Home Index