---

Step * 1 of Lemma mFOL-abstract-rename


1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. name : Atom
6. vars : ℤ List
7. ¬(x ∈ mFOL-boundvars(name(vars)))
8. a1 : FOAssignment(mFOL-freevars(mFOL-rename(name(vars);y;x)),Dom)
9. a2 : FOAssignment(mFOL-freevars(name(vars)),Dom)
10. a2 = FOAssigment-rename(a1;name(vars);x;y) ∈ FOAssignment(mFOL-freevars(name(vars)),Dom)
⊢ Dom,S,a2 |= mFOL-abstract(name(vars)) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(name(vars);y;x)) ∈ ℙ
BY
{ (All (Unfold `FOAssigment-rename`)
   THEN RepUR ``mFOL-rename mFOL-abstract`` 0
   THEN RepUR ``AbstractFOAtomic FOSatWith`` 0
   THEN EqCD
   THEN Auto
   THEN (RWO  "map-map" 0 THENA Auto)
   THEN (Assert vars ∈ {z:ℤ| (z ∈ vars)}  List BY
               Auto)
   THEN EqCD
   THEN Auto
   THEN FunExt
   THEN Reduce 0
   THEN Auto
   THEN AutoSplit) }

1
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. name : Atom
6. vars : ℤ List
7. ¬(x ∈ mFOL-boundvars(name(vars)))
8. a1 : FOAssignment(mFOL-freevars(mFOL-rename(name(vars);y;x)),Dom)
9. a2 : FOAssignment(mFOL-freevars(name(vars)),Dom)
10. a2 = if y ∈b mFOL-freevars(name(vars)) then a1[y := a1 x] else a1 fi  ∈ FOAssignment(mFOL-freevars(name(vars)),Dom)
11. vars ∈ {z:ℤ| (z ∈ vars)}  List
12. x1 : {z:ℤ| (z ∈ vars)} 
13. x1 = y ∈ ℤ
⊢ (a2 x1) = (a1 x) ∈ Dom

2
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. name : Atom
6. vars : ℤ List
7. ¬(x ∈ mFOL-boundvars(name(vars)))
8. a1 : FOAssignment(mFOL-freevars(mFOL-rename(name(vars);y;x)),Dom)
9. a2 : FOAssignment(mFOL-freevars(name(vars)),Dom)
10. a2 = if y ∈b mFOL-freevars(name(vars)) then a1[y := a1 x] else a1 fi  ∈ FOAssignment(mFOL-freevars(name(vars)),Dom)
11. vars ∈ {z:ℤ| (z ∈ vars)}  List
12. x1 : {z:ℤ| (z ∈ vars)} 
13. x1 ≠ y
⊢ (a2 x1) = (a1 x1) ∈ Dom

---

Latex:

---

Latex:

1.  Dom  :  Type
2.  S  :  FOStruct(Dom)
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  name  :  Atom
6.  vars  :  \mBbbZ{}  List
7.  \mneg{}(x  \mmember{}  mFOL-boundvars(name(vars)))
8.  a1  :  FOAssignment(mFOL-freevars(mFOL-rename(name(vars);y;x)),Dom)
9.  a2  :  FOAssignment(mFOL-freevars(name(vars)),Dom)
10.  a2  =  FOAssigment-rename(a1;name(vars);x;y)
\mvdash{}  Dom,S,a2  |=  mFOL-abstract(name(vars))  =  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(name(vars);y;x))


By

---

Latex:
(All  (Unfold  `FOAssigment-rename`)
  THEN  RepUR  ``mFOL-rename  mFOL-abstract``  0
  THEN  RepUR  ``AbstractFOAtomic  FOSatWith``  0
  THEN  EqCD
  THEN  Auto
  THEN  (RWO    "map-map"  0  THENA  Auto)
  THEN  (Assert  vars  \mmember{}  \{z:\mBbbZ{}|  (z  \mmember{}  vars)\}    List  BY
                          Auto)
  THEN  EqCD
  THEN  Auto
  THEN  FunExt
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index