---

Step * 3 of Lemma mFOL-abstract-functionality


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)) ∈ ℙ
BY
{ (RepUR ``mFOL-abstract`` 0
   THEN Fold `mFOL-abstract` 0
   THEN RepUR ``FOSatWith FOQuantifier let`` 0
   THEN Fold `FOSatWith` 0
   THEN AutoSplit
   THEN EqCD
   THEN Auto
   THEN BackThruSomeHyp
   THEN (Auto
         THEN RepUR ``update-assignment`` 0
         THEN AutoSplit
         THEN BackThruSomeHyp
         THEN RepUR ``mFOL-freevars`` 0⋅
         THEN Fold `mFOL-freevars` 0
         THEN BLemma `member_filter`
         THEN Auto
         THEN Reduce 0
         THEN RW assert_pushdownC 0
         THEN Auto)⋅)⋅ }

---

Latex:



1.  Dom  :  Type
2.  S  :  FOStruct(Dom)
3.  isall  :  \mBbbB{}@i'
4.  var  :  \mBbbZ{}@i'
5.  body  :  mFOL()@i'
6.  \mforall{}a1,a2:FOAssignment(Dom).
          ((\mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(body))  {}\mRightarrow{}  ((a1  z)  =  (a2  z))))
          {}\mRightarrow{}  (Dom,S,a1  |=  mFOL-abstract(body)  =  Dom,S,a2  |=  mFOL-abstract(body)))@i'
7.  a1  :  FOAssignment(Dom)@i'
8.  a2  :  FOAssignment(Dom)@i'
9.  \mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(mFOquant(isall;var;body)))  {}\mRightarrow{}  ((a1  z)  =  (a2  z)))@i'
\mvdash{}  Dom,S,a1  |=  mFOL-abstract(mFOquant(isall;var;body))
=  Dom,S,a2  |=  mFOL-abstract(mFOquant(isall;var;body))


By

(RepUR  ``mFOL-abstract``  0
  THEN  Fold  `mFOL-abstract`  0
  THEN  RepUR  ``FOSatWith  FOQuantifier  let``  0
  THEN  Fold  `FOSatWith`  0
  THEN  AutoSplit
  THEN  EqCD
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  (Auto
              THEN  RepUR  ``update-assignment``  0
              THEN  AutoSplit
              THEN  BackThruSomeHyp
              THEN  RepUR  ``mFOL-freevars``  0\mcdot{}
              THEN  Fold  `mFOL-freevars`  0
              THEN  BLemma  `member\_filter`
              THEN  Auto
              THEN  Reduce  0
              THEN  RW  assert\_pushdownC  0
              THEN  Auto)\mcdot{})\mcdot{}

---

Home Index