---

Step * 3 2 1 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 : ℤ
19. x1 ≠ z
20. (x1 ∈ mFOL-freevars(body))
21. (y ∈ mFOL-freevars(body))
22. x1 = y ∈ ℤ
⊢ (a2 x1) = (a1 x) ∈ Dom
BY
{ ((Assert (x1 ∈ filter(λx.(¬b(x =z z));mFOL-freevars(body))) BY
          (BLemma `member_filter` THEN Reduce 0 THEN Auto))
   THEN OnMaybeHyp 16 (\h. ((SplitOnHypITE h  THENA Auto)
                            THEN Try ((D -1 THEN BLemma `member_filter` THEN Reduce 0 THEN Auto))
                            THEN Unfold `FOAssignment` h
                            THEN (ApFunToHypEquands `Z' ⌜Z x1⌝ ⌜Dom⌝ h⋅ THENA Auto)
                            THEN RepUR ``update-assignment`` -1
                            THEN SplitOnHypITE -1 
                            THEN Auto))
   ) }

---

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  :  \mBbbZ{}
19.  x1  \mneq{}  z
20.  (x1  \mmember{}  mFOL-freevars(body))
21.  (y  \mmember{}  mFOL-freevars(body))
22.  x1  =  y
\mvdash{}  (a2  x1)  =  (a1  x)


By

---

Latex:
((Assert  (x1  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(body)))  BY
                (BLemma  `member\_filter`  THEN  Reduce  0  THEN  Auto))
  THEN  OnMaybeHyp  16  (\mbackslash{}h.  ((SplitOnHypITE  h    THENA  Auto)
                                                    THEN  Try  ((D  -1  THEN  BLemma  `member\_filter`  THEN  Reduce  0  THEN  Auto))
                                                    THEN  Unfold  `FOAssignment`  h
                                                    THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x1\mkleeneclose{}  \mkleeneopen{}Dom\mkleeneclose{}  h\mcdot{}  THENA  Auto)
                                                    THEN  RepUR  ``update-assignment``  -1
                                                    THEN  SplitOnHypITE  -1 
                                                    THEN  Auto))
  )

---

Home Index