---

Step * 3 of Lemma FOL-abstract-rename


1. Dom : Type
2. S : FOStruct+{i:l}(Dom)
3. x : ℤ
4. y : ℤ
5. isall : 𝔹
6. var : ℤ
7. body : mFOL()
8. (¬(x ∈ mFOL-boundvars(body)))
⇒ (∀a1:FOAssignment(mFOL-freevars(mFOL-rename(body;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(body),Dom).
      ((a2 = FOAssigment-rename(a1;body;x;y) ∈ FOAssignment(mFOL-freevars(body),Dom))
      ⇒ (Dom,S,a2 +|= FOL-abstract(body) = Dom,S,a1 +|= FOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ)))
9. ¬(x ∈ mFOL-boundvars(mFOquant(isall;var;body)))
10. a1 : FOAssignment(mFOL-freevars(mFOL-rename(mFOquant(isall;var;body);y;x)),Dom)
11. a2 : FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom)
12. a2 = FOAssigment-rename(a1;mFOquant(isall;var;body);x;y) ∈ FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom)
⊢ Dom,S,a2 +|= FOL-abstract(mFOquant(isall;var;body))
= Dom,S,a1 +|= FOL-abstract(mFOL-rename(mFOquant(isall;var;body);y;x))
∈ ℙ
BY
{ All (Unfold `FOAssigment-rename`) }

1
1. Dom : Type
2. S : FOStruct+{i:l}(Dom)
3. x : ℤ
4. y : ℤ
5. isall : 𝔹
6. var : ℤ
7. body : mFOL()
8. (¬(x ∈ mFOL-boundvars(body)))
⇒ (∀a1:FOAssignment(mFOL-freevars(mFOL-rename(body;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(body),Dom).
      ((a2 = if y ∈b mFOL-freevars(body) then a1[y := a1 x] else a1 fi  ∈ FOAssignment(mFOL-freevars(body),Dom))
      ⇒ (Dom,S,a2 +|= FOL-abstract(body) = Dom,S,a1 +|= FOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ)))
9. ¬(x ∈ mFOL-boundvars(mFOquant(isall;var;body)))
10. a1 : FOAssignment(mFOL-freevars(mFOL-rename(mFOquant(isall;var;body);y;x)),Dom)
11. a2 : FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom)
12. a2
= if y ∈b mFOL-freevars(mFOquant(isall;var;body)) then a1[y := a1 x] else a1 fi 
∈ FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom)
⊢ Dom,S,a2 +|= FOL-abstract(mFOquant(isall;var;body))
= Dom,S,a1 +|= FOL-abstract(mFOL-rename(mFOquant(isall;var;body);y;x))
∈ ℙ

---

Latex:

---

Latex:

1.  Dom  :  Type
2.  S  :  FOStruct+\{i:l\}(Dom)
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  isall  :  \mBbbB{}
6.  var  :  \mBbbZ{}
7.  body  :  mFOL()
8.  (\mneg{}(x  \mmember{}  mFOL-boundvars(body)))
{}\mRightarrow{}  (\mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(body;y;x)),Dom).
        \mforall{}a2:FOAssignment(mFOL-freevars(body),Dom).
            ((a2  =  FOAssigment-rename(a1;body;x;y))
            {}\mRightarrow{}  (Dom,S,a2  +|=  FOL-abstract(body)  =  Dom,S,a1  +|=  FOL-abstract(mFOL-rename(body;y;x)))))
9.  \mneg{}(x  \mmember{}  mFOL-boundvars(mFOquant(isall;var;body)))
10.  a1  :  FOAssignment(mFOL-freevars(mFOL-rename(mFOquant(isall;var;body);y;x)),Dom)
11.  a2  :  FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom)
12.  a2  =  FOAssigment-rename(a1;mFOquant(isall;var;body);x;y)
\mvdash{}  Dom,S,a2  +|=  FOL-abstract(mFOquant(isall;var;body))
=  Dom,S,a1  +|=  FOL-abstract(mFOL-rename(mFOquant(isall;var;body);y;x))


By

---

Latex:
All  (Unfold  `FOAssigment-rename`)

---

Home Index