---

Step * 3 2 1 3 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. ¬(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
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 (RWO "member_filter" (-1) THEN Auto)
                            THEN Unfold `FOAssignment` h
                            THEN ApFunToHypEquands `Z' ⌜Z x1⌝ ⌜Dom⌝ h⋅
                            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{}(y  \mmember{}  mFOL-freevars(body))
11.  \mneg{}(x  \mmember{}  mFOL-boundvars(\mexists{}z;body)))
12.  a1  :  FOAssignment(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(mFOL-rename(body;y;x))),Dom)
13.  a2  :  FOAssignment(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(body)),Dom)
14.  a2  =  if  y  \mmember{}\msubb{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(body))  then  a1[y  :=  a1  x]  else  a1  fi 
15.  \mneg{}(x  =  z)
16.  \mneg{}(x  \mmember{}  mFOL-boundvars(body))
17.  \mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(body;y;x)),Dom).
        \mforall{}a2:FOAssignment(mFOL-freevars(body),Dom).
            ((a2  =  a1)
            {}\mRightarrow{}  (Dom,S,a2  |=  mFOL-abstract(body)  =  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(body;y;x))))
18.  v  :  Dom
19.  x1  :  \mBbbZ{}
20.  x1  \mneq{}  z
21.  (x1  \mmember{}  mFOL-freevars(body))
\mvdash{}  (a2  x1)  =  (a1  x1)


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  (RWO  "member\_filter"  (-1)  THEN  Auto)
                                                    THEN  Unfold  `FOAssignment`  h
                                                    THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x1\mkleeneclose{}  \mkleeneopen{}Dom\mkleeneclose{}  h\mcdot{}
                                                    THEN  Auto))
  )

---

Home Index