---

Step * 2 1 1 1 of Lemma mFOL-abstract-rename


1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. knd : Atom
6. left : mFOL()
7. right : mFOL()
8. ¬(x ∈ mFOL-boundvars(mFOconnect(knd;left;right)))
9. a1 : FOAssignment(mFOL-freevars(mFOL-rename(mFOconnect(knd;left;right);y;x)),Dom)
10. a2 : FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom)
11. a2 = a1[y := a1 x] ∈ FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom)
12. ¬(x ∈ mFOL-boundvars(left))
13. ¬(x ∈ mFOL-boundvars(right))
14. ∀a1:FOAssignment(mFOL-freevars(mFOL-rename(right;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(right),Dom).
      ((a2 = if y ∈b mFOL-freevars(right) then a1[y := a1 x] else a1 fi  ∈ FOAssignment(mFOL-freevars(right),Dom))
      ⇒ (Dom,S,a2 |= mFOL-abstract(right) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(right;y;x)) ∈ ℙ))
15. ∀a1:FOAssignment(mFOL-freevars(mFOL-rename(left;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(left),Dom).
      ((a2 = if y ∈b mFOL-freevars(left) then a1[y := a1 x] else a1 fi  ∈ FOAssignment(mFOL-freevars(left),Dom))
      ⇒ (Dom,S,a2 |= mFOL-abstract(left) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(left;y;x)) ∈ ℙ))
16. (y ∈ mFOL-freevars(mFOconnect(knd;left;right)))
17. (y ∈ mFOL-freevars(left)) ∨ (y ∈ mFOL-freevars(right))
⊢ Dom,S,a2 |= mFOL-abstract(mFOconnect(knd;left;right))
= Dom,S,a1 |= mFOL-abstract(mFOL-rename(mFOconnect(knd;left;right);y;x))
∈ ℙ
BY
{ (RepUR ``mFOL-rename mFOL-abstract`` 0
   THEN Folds ``mFOL-rename mFOL-abstract`` 0
   THEN RepUR ``FOConnective FOSatWith let`` 0
   THEN Fold `FOSatWith` 0
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))
   THEN Auto
   THEN (BackThruSomeHyp ORELSE ((EqCD THEN Try (Trivial)) THEN BackThruSomeHyp))
   THEN Try ((RepUR ``mFOL-rename`` 0 THEN Fold `mFOL-rename` 0))
   THEN Try ((FOLFreevarsContained THEN Auto))
   THEN AutoSplit
   THEN Try ((SubsumeEq THEN Auto THEN FOLFreevarsContained THEN Auto))
   THEN Unfold `FOAssignment` 0
   THEN (FunExt THENA Auto)
   THEN D -1
   THEN (Assert (x1 ∈ mFOL-freevars(mFOconnect(knd;left;right))) BY
               (RepUR ``mFOL-freevars`` 0
                THEN Fold `mFOL-freevars` 0
                THEN (RWO "val-union-l-union" 0 THEN Auto)
                THEN BLemma `member-union`
                THEN Auto))
   THEN ((Unfold `FOAssignment` 12 THEN ApFunToHypEquands `Z' ⌜Z x1⌝ ⌜Dom⌝ 12⋅) THENA Auto)
   THEN RepUR ``update-assignment`` -1
   THEN SplitOnHypITE -1 
   THEN Auto
   THEN HypSubst' (-1) (-4)
   THEN Auto) }

---

Latex:

---

Latex:

1.  Dom  :  Type
2.  S  :  FOStruct(Dom)
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  knd  :  Atom
6.  left  :  mFOL()
7.  right  :  mFOL()
8.  \mneg{}(x  \mmember{}  mFOL-boundvars(mFOconnect(knd;left;right)))
9.  a1  :  FOAssignment(mFOL-freevars(mFOL-rename(mFOconnect(knd;left;right);y;x)),Dom)
10.  a2  :  FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom)
11.  a2  =  a1[y  :=  a1  x]
12.  \mneg{}(x  \mmember{}  mFOL-boundvars(left))
13.  \mneg{}(x  \mmember{}  mFOL-boundvars(right))
14.  \mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(right;y;x)),Dom).
        \mforall{}a2:FOAssignment(mFOL-freevars(right),Dom).
            ((a2  =  if  y  \mmember{}\msubb{}  mFOL-freevars(right)  then  a1[y  :=  a1  x]  else  a1  fi  )
            {}\mRightarrow{}  (Dom,S,a2  |=  mFOL-abstract(right)  =  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(right;y;x))))
15.  \mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(left;y;x)),Dom).
        \mforall{}a2:FOAssignment(mFOL-freevars(left),Dom).
            ((a2  =  if  y  \mmember{}\msubb{}  mFOL-freevars(left)  then  a1[y  :=  a1  x]  else  a1  fi  )
            {}\mRightarrow{}  (Dom,S,a2  |=  mFOL-abstract(left)  =  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(left;y;x))))
16.  (y  \mmember{}  mFOL-freevars(mFOconnect(knd;left;right)))
17.  (y  \mmember{}  mFOL-freevars(left))  \mvee{}  (y  \mmember{}  mFOL-freevars(right))
\mvdash{}  Dom,S,a2  |=  mFOL-abstract(mFOconnect(knd;left;right))
=  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(mFOconnect(knd;left;right);y;x))


By

---

Latex:
(RepUR  ``mFOL-rename  mFOL-abstract``  0
  THEN  Folds  ``mFOL-rename  mFOL-abstract``  0
  THEN  RepUR  ``FOConnective  FOSatWith  let``  0
  THEN  Fold  `FOSatWith`  0
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
  THEN  Auto
  THEN  (BackThruSomeHyp  ORELSE  ((EqCD  THEN  Try  (Trivial))  THEN  BackThruSomeHyp))
  THEN  Try  ((RepUR  ``mFOL-rename``  0  THEN  Fold  `mFOL-rename`  0))
  THEN  Try  ((FOLFreevarsContained  THEN  Auto))
  THEN  AutoSplit
  THEN  Try  ((SubsumeEq  THEN  Auto  THEN  FOLFreevarsContained  THEN  Auto))
  THEN  Unfold  `FOAssignment`  0
  THEN  (FunExt  THENA  Auto)
  THEN  D  -1
  THEN  (Assert  (x1  \mmember{}  mFOL-freevars(mFOconnect(knd;left;right)))  BY
                          (RepUR  ``mFOL-freevars``  0
                            THEN  Fold  `mFOL-freevars`  0
                            THEN  (RWO  "val-union-l-union"  0  THEN  Auto)
                            THEN  BLemma  `member-union`
                            THEN  Auto))
  THEN  ((Unfold  `FOAssignment`  12  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x1\mkleeneclose{}  \mkleeneopen{}Dom\mkleeneclose{}  12\mcdot{})  THENA  Auto)
  THEN  RepUR  ``update-assignment``  -1
  THEN  SplitOnHypITE  -1 
  THEN  Auto
  THEN  HypSubst'  (-1)  (-4)
  THEN  Auto)

---

Home Index