---

Step * 2 of Lemma mFOL-abstract-functionality


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)) ∈ ℙ
BY
{ (RepUR ``mFOL-abstract`` 0
   THEN Fold `mFOL-abstract` 0
   THEN RepUR ``FOSatWith FOConnective let`` 0
   THEN Fold `FOSatWith` 0
   THEN Repeat (AutoSplit)
   THEN EqCD
   THEN Auto
   THEN (BackThruSomeHyp
         THEN OnMaybeHyp 10 (\h. (ParallelOp h
                                  THEN ParallelLast
                                  THEN RepUR ``mFOL-freevars`` 0
                                  THEN Fold `mFOL-freevars` 0
                                  THEN (RWO "val-union-l-union" 0 THENM RWW "member-union" 0)
                                  THEN Auto))
         )⋅)⋅ }

---

Latex:



1.  Dom  :  Type
2.  S  :  FOStruct(Dom)
3.  knd  :  Atom@i'
4.  left  :  mFOL()@i'
5.  right  :  mFOL()@i'
6.  \mforall{}a1,a2:FOAssignment(Dom).
          ((\mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(left))  {}\mRightarrow{}  ((a1  z)  =  (a2  z))))
          {}\mRightarrow{}  (Dom,S,a1  |=  mFOL-abstract(left)  =  Dom,S,a2  |=  mFOL-abstract(left)))@i'
7.  \mforall{}a1,a2:FOAssignment(Dom).
          ((\mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(right))  {}\mRightarrow{}  ((a1  z)  =  (a2  z))))
          {}\mRightarrow{}  (Dom,S,a1  |=  mFOL-abstract(right)  =  Dom,S,a2  |=  mFOL-abstract(right)))@i'
8.  a1  :  FOAssignment(Dom)@i'
9.  a2  :  FOAssignment(Dom)@i'
10.  \mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(mFOconnect(knd;left;right)))  {}\mRightarrow{}  ((a1  z)  =  (a2  z)))@i'
\mvdash{}  Dom,S,a1  |=  mFOL-abstract(mFOconnect(knd;left;right))
=  Dom,S,a2  |=  mFOL-abstract(mFOconnect(knd;left;right))


By

(RepUR  ``mFOL-abstract``  0
  THEN  Fold  `mFOL-abstract`  0
  THEN  RepUR  ``FOSatWith  FOConnective  let``  0
  THEN  Fold  `FOSatWith`  0
  THEN  Repeat  (AutoSplit)
  THEN  EqCD
  THEN  Auto
  THEN  (BackThruSomeHyp
              THEN  OnMaybeHyp  10  (\mbackslash{}h.  (ParallelOp  h
                                                                THEN  ParallelLast
                                                                THEN  RepUR  ``mFOL-freevars``  0
                                                                THEN  Fold  `mFOL-freevars`  0
                                                                THEN  (RWO  "val-union-l-union"  0  THENM  RWW  "member-union"  0)
                                                                THEN  Auto))
              )\mcdot{})\mcdot{}

---

Home Index