---

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

.....truecase..... 
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)))
⊢ Dom,S,a2 |= mFOL-abstract(mFOconnect(knd;left;right))
= Dom,S,a1 |= mFOL-abstract(mFOL-rename(mFOconnect(knd;left;right);y;x))
∈ ℙ
BY
{ (DupHyp (-1)
   THEN RepUR ``mFOL-freevars`` -1
   THEN Fold `mFOL-freevars` (-1)
   THEN (RWO "val-union-l-union" (-1) THENA Auto)
   THEN ((RWO "member-union" (-1) THENA Auto) ORELSE Auto)) }

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

---

Latex:

---

Latex:
.....truecase..... 
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)))
\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:
(DupHyp  (-1)
  THEN  RepUR  ``mFOL-freevars``  -1
  THEN  Fold  `mFOL-freevars`  (-1)
  THEN  (RWO  "val-union-l-union"  (-1)  THENA  Auto)
  THEN  ((RWO  "member-union"  (-1)  THENA  Auto)  ORELSE  Auto))

---

Home Index