---

Step * of Lemma FOL-abstract-rename

∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
  ∀x,y:ℤ. ∀fmla:mFOL().
    ((¬(x ∈ mFOL-boundvars(fmla)))
    ⇒ (∀a1:FOAssignment(mFOL-freevars(mFOL-rename(fmla;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(fmla),Dom).
          ((a2 = FOAssigment-rename(a1;fmla;x;y) ∈ FOAssignment(mFOL-freevars(fmla),Dom))
          ⇒ (Dom,S,a2 +|= FOL-abstract(fmla) = Dom,S,a1 +|= FOL-abstract(mFOL-rename(fmla;y;x)) ∈ ℙ))))
BY
{ (RepeatFor 4 (Intro) THEN BLemmaUp `mFOL-induction` THEN At ⌜𝕌'⌝Auto⋅) }

1
1. Dom : Type
2. S : FOStruct+{i:l}(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 +|= FOL-abstract(name(vars)) = Dom,S,a1 +|= FOL-abstract(mFOL-rename(name(vars);y;x)) ∈ ℙ

2
1. Dom : Type
2. S : FOStruct+{i:l}(Dom)
3. x : ℤ
4. y : ℤ
5. knd : Atom
6. left : mFOL()
7. right : mFOL()
8. (¬(x ∈ mFOL-boundvars(left)))
⇒ (∀a1:FOAssignment(mFOL-freevars(mFOL-rename(left;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(left),Dom).
      ((a2 = FOAssigment-rename(a1;left;x;y) ∈ FOAssignment(mFOL-freevars(left),Dom))
      ⇒ (Dom,S,a2 +|= FOL-abstract(left) = Dom,S,a1 +|= FOL-abstract(mFOL-rename(left;y;x)) ∈ ℙ)))
9. (¬(x ∈ mFOL-boundvars(right)))
⇒ (∀a1:FOAssignment(mFOL-freevars(mFOL-rename(right;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(right),Dom).
      ((a2 = FOAssigment-rename(a1;right;x;y) ∈ FOAssignment(mFOL-freevars(right),Dom))
      ⇒ (Dom,S,a2 +|= FOL-abstract(right) = Dom,S,a1 +|= FOL-abstract(mFOL-rename(right;y;x)) ∈ ℙ)))
10. ¬(x ∈ mFOL-boundvars(mFOconnect(knd;left;right)))
11. a1 : FOAssignment(mFOL-freevars(mFOL-rename(mFOconnect(knd;left;right);y;x)),Dom)
12. a2 : FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom)
13. a2
= FOAssigment-rename(a1;mFOconnect(knd;left;right);x;y)
∈ FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom)
⊢ Dom,S,a2 +|= FOL-abstract(mFOconnect(knd;left;right))
= Dom,S,a1 +|= FOL-abstract(mFOL-rename(mFOconnect(knd;left;right);y;x))
∈ ℙ

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

---

Latex:

---

Latex:
\mforall{}[Dom:Type].  \mforall{}[S:FOStruct+\{i:l\}(Dom)].
    \mforall{}x,y:\mBbbZ{}.  \mforall{}fmla:mFOL().
        ((\mneg{}(x  \mmember{}  mFOL-boundvars(fmla)))
        {}\mRightarrow{}  (\mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(fmla;y;x)),Dom).
                \mforall{}a2:FOAssignment(mFOL-freevars(fmla),Dom).
                    ((a2  =  FOAssigment-rename(a1;fmla;x;y))
                    {}\mRightarrow{}  (Dom,S,a2  +|=  FOL-abstract(fmla)  =  Dom,S,a1  +|=  FOL-abstract(mFOL-rename(fmla;y;x))))))


By

---

Latex:
(RepeatFor  4  (Intro)  THEN  BLemmaUp  `mFOL-induction`  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}Auto\mcdot{})

---

Home Index