---

Step * 1 2 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 = 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
BY
{ (RepUR ``FOAssignment update-assignment`` (-4)
   THEN RepUR ``mFOL-freevars`` -4
   THEN (ApFunToHypEquands `Z' ⌜Z x1⌝ ⌜Dom⌝ (-4)⋅ THENA (DVar `x1' THEN Auto))
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN Reduce (-2)
   THEN Auto) }

---

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  =  if  y  \mmember{}\msubb{}  mFOL-freevars(name(vars))  then  a1[y  :=  a1  x]  else  a1  fi 
11.  vars  \mmember{}  \{z:\mBbbZ{}|  (z  \mmember{}  vars)\}    List
12.  x1  :  \{z:\mBbbZ{}|  (z  \mmember{}  vars)\} 
13.  x1  \mneq{}  y
\mvdash{}  (a2  x1)  =  (a1  x1)


By

---

Latex:
(RepUR  ``FOAssignment  update-assignment``  (-4)
  THEN  RepUR  ``mFOL-freevars``  -4
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x1\mkleeneclose{}  \mkleeneopen{}Dom\mkleeneclose{}  (-4)\mcdot{}  THENA  (DVar  `x1'  THEN  Auto))
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  Reduce  (-2)
  THEN  Auto)

---

Home Index