---

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


1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. isall : 𝔹
6. ¬↑isall
7. z : ℤ
8. z ≠ y
9. body : mFOL()
10. ¬(x ∈ mFOL-boundvars(∃z;body)))
11. a1 : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(mFOL-rename(body;y;x))),Dom)
12. a2 : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(body)),Dom)
13. a2
= if y ∈b filter(λx.(¬b(x =z z));mFOL-freevars(body)) then a1[y := a1 x] else a1 fi 
∈ FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(body)),Dom)
14. ¬(x = z ∈ ℤ)
15. ¬(x ∈ mFOL-boundvars(body))
16. ∀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 |= mFOL-abstract(body) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ))
17. v : Dom
18. x1 : {z:ℤ| (z ∈ mFOL-freevars(body))} 
⊢ (a2[z := v] x1) = (if y ∈b mFOL-freevars(body) then a1[z := v][y := a1[z := v] x] else a1[z := v] fi  x1) ∈ Dom
BY
{ (D -1 THEN AutoSplit THEN RepUR ``update-assignment`` 0 THEN Repeat (AutoSplit)) }

1
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. isall : 𝔹
6. ¬↑isall
7. z : ℤ
8. z ≠ y
9. body : mFOL()
10. ¬(x ∈ mFOL-boundvars(∃z;body)))
11. a1 : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(mFOL-rename(body;y;x))),Dom)
12. a2 : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(body)),Dom)
13. a2
= if y ∈b filter(λx.(¬b(x =z z));mFOL-freevars(body)) then a1[y := a1 x] else a1 fi 
∈ FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(body)),Dom)
14. ¬(x = z ∈ ℤ)
15. ¬(x ∈ mFOL-boundvars(body))
16. ∀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 |= mFOL-abstract(body) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ))
17. v : Dom
18. x1 : ℤ
19. x1 ≠ z
20. (x1 ∈ mFOL-freevars(body))
21. (y ∈ mFOL-freevars(body))
22. x1 = y ∈ ℤ
⊢ (a2 x1) = (a1 x) ∈ Dom

2
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. isall : 𝔹
6. ¬↑isall
7. z : ℤ
8. z ≠ y
9. body : mFOL()
10. ¬(x ∈ mFOL-boundvars(∃z;body)))
11. a1 : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(mFOL-rename(body;y;x))),Dom)
12. a2 : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(body)),Dom)
13. a2
= if y ∈b filter(λx.(¬b(x =z z));mFOL-freevars(body)) then a1[y := a1 x] else a1 fi 
∈ FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(body)),Dom)
14. ¬(x = z ∈ ℤ)
15. ¬(x ∈ mFOL-boundvars(body))
16. ∀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 |= mFOL-abstract(body) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ))
17. v : Dom
18. x1 : ℤ
19. x1 ≠ y
20. x1 ≠ z
21. (x1 ∈ mFOL-freevars(body))
22. (y ∈ mFOL-freevars(body))
⊢ (a2 x1) = (a1 x1) ∈ Dom

3
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. isall : 𝔹
6. ¬↑isall
7. z : ℤ
8. z ≠ y
9. body : mFOL()
10. ¬(y ∈ mFOL-freevars(body))
11. ¬(x ∈ mFOL-boundvars(∃z;body)))
12. a1 : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(mFOL-rename(body;y;x))),Dom)
13. a2 : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(body)),Dom)
14. a2
= if y ∈b filter(λx.(¬b(x =z z));mFOL-freevars(body)) then a1[y := a1 x] else a1 fi 
∈ FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(body)),Dom)
15. ¬(x = z ∈ ℤ)
16. ¬(x ∈ mFOL-boundvars(body))
17. ∀a1:FOAssignment(mFOL-freevars(mFOL-rename(body;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(body),Dom).
      ((a2 = a1 ∈ FOAssignment(mFOL-freevars(body),Dom))
      ⇒ (Dom,S,a2 |= mFOL-abstract(body) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ))
18. v : Dom
19. x1 : ℤ
20. x1 ≠ z
21. (x1 ∈ mFOL-freevars(body))
⊢ (a2 x1) = (a1 x1) ∈ Dom

---

Latex:

---

Latex:

1.  Dom  :  Type
2.  S  :  FOStruct(Dom)
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  isall  :  \mBbbB{}
6.  \mneg{}\muparrow{}isall
7.  z  :  \mBbbZ{}
8.  z  \mneq{}  y
9.  body  :  mFOL()
10.  \mneg{}(x  \mmember{}  mFOL-boundvars(\mexists{}z;body)))
11.  a1  :  FOAssignment(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(mFOL-rename(body;y;x))),Dom)
12.  a2  :  FOAssignment(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(body)),Dom)
13.  a2  =  if  y  \mmember{}\msubb{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(body))  then  a1[y  :=  a1  x]  else  a1  fi 
14.  \mneg{}(x  =  z)
15.  \mneg{}(x  \mmember{}  mFOL-boundvars(body))
16.  \mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(body;y;x)),Dom).
        \mforall{}a2:FOAssignment(mFOL-freevars(body),Dom).
            ((a2  =  if  y  \mmember{}\msubb{}  mFOL-freevars(body)  then  a1[y  :=  a1  x]  else  a1  fi  )
            {}\mRightarrow{}  (Dom,S,a2  |=  mFOL-abstract(body)  =  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(body;y;x))))
17.  v  :  Dom
18.  x1  :  \{z:\mBbbZ{}|  (z  \mmember{}  mFOL-freevars(body))\} 
\mvdash{}  (a2[z  :=  v]  x1)
=  (if  y  \mmember{}\msubb{}  mFOL-freevars(body)  then  a1[z  :=  v][y  :=  a1[z  :=  v]  x]  else  a1[z  :=  v]  fi    x1)


By

---

Latex:
(D  -1  THEN  AutoSplit  THEN  RepUR  ``update-assignment``  0  THEN  Repeat  (AutoSplit))

---

Home Index