---

Step * of Lemma mFOL-abstract-rename

∀[Dom:Type]. ∀[S:FOStruct(Dom)].
  ∀x,y:ℤ. ∀fmla:mFOL().
    ((¬(x ∈ mFOL-boundvars(fmla)))
    ⇒ (∀a1,a2:FOAssignment(Dom).
          ((a2 = a1[y := a1 x] ∈ FOAssignment(Dom))
          ⇒ (Dom,S,a2 |= mFOL-abstract(fmla) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(fmla;y;x)) ∈ ℙ))))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (BLemmaUp `mFOL-induction` THEN At ⌈𝕌'⌉Auto⋅ THEN Auto)
   THEN (Try ((RepUR ``mFOL-rename`` 0⋅ THEN Try (Fold `mFOL-rename` 0)))
         THEN Try ((RepUR ``mFOL-abstract`` 0⋅ THEN Try (Fold `mFOL-abstract` 0)))
         THEN RepUR ``FOSatWith FOConnective FOQuantifier AbstractFOAtomic let`` 0
         THEN Try (Fold `FOSatWith` 0)
         THEN Try ((EqCD
                    THEN Auto
                    THEN (HypSubst (-1) 0 THEN Auto)
                    THEN Unfold `update-assignment` 0
                    THEN All Thin
                    THEN ListInd (-2)
                    THEN Reduce 0
                    THEN Auto
                    THEN AutoSplit)⋅)
         THEN Try (((Assert (¬(x ∈ mFOL-boundvars(left))) ∧ (¬(x ∈ mFOL-boundvars(right))) BY
                           (Auto
                            THEN OnMaybeHyp 9 (\h. (ParallelOp h
                                                    THEN RepUR ``mFOL-boundvars`` 0
                                                    THEN Fold `mFOL-boundvars` 0
                                                    THEN BLemma `member-union`
                                                    THEN Auto))
                            ))⋅
                    THEN Repeat (AutoSplit⋅)
                    THEN EqCD
                    THEN Auto))⋅
         THEN (RenameVar `z' 6
               THEN (Assert (¬(x = z ∈ ℤ)) ∧ (¬(x ∈ mFOL-boundvars(body))) BY
                           (Auto
                            THEN OnMaybeHyp 9 (\h. (ParallelOp h
                                                    THEN RepUR ``mFOL-boundvars`` 0
                                                    THEN Fold `mFOL-boundvars` 0
                                                    THEN BLemma `member-insert`
                                                    THEN Auto))
                            ))
               THEN (RepeatFor 2 (AutoSplit)
                     THEN Try ((HypSubst' (-1) 0
                                THEN RepeatFor 2 ((EqCD THEN Auto))
                                THEN (SubstFor ⌈a2⌉ 0⋅ THENA Auto)
                                THEN (RepUR ``update-assignment FOAssignment`` 0 THEN EqCD THEN Auto THEN AutoSplit)⋅)⋅)
                     THEN (EqCD THEN Auto)
                     THEN BackThruSomeHyp
                     THEN Auto
                     THEN ((SubstFor ⌈a2⌉ 0⋅ THENA (Auto THEN Fold `FOAssignment` 0 THEN Auto))
                           THEN RepUR ``update-assignment FOAssignment`` 0
                           THEN EqCD
                           THEN Auto
                           THEN RepeatFor 3 (AutoSplit))⋅))⋅)⋅) }

---

Latex:


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


By

(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (BLemmaUp  `mFOL-induction`  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}Auto\mcdot{}  THEN  Auto)
  THEN  (Try  ((RepUR  ``mFOL-rename``  0\mcdot{}  THEN  Try  (Fold  `mFOL-rename`  0)))
              THEN  Try  ((RepUR  ``mFOL-abstract``  0\mcdot{}  THEN  Try  (Fold  `mFOL-abstract`  0)))
              THEN  RepUR  ``FOSatWith  FOConnective  FOQuantifier  AbstractFOAtomic  let``  0
              THEN  Try  (Fold  `FOSatWith`  0)
              THEN  Try  ((EqCD
                                    THEN  Auto
                                    THEN  (HypSubst  (-1)  0  THEN  Auto)
                                    THEN  Unfold  `update-assignment`  0
                                    THEN  All  Thin
                                    THEN  ListInd  (-2)
                                    THEN  Reduce  0
                                    THEN  Auto
                                    THEN  AutoSplit)\mcdot{})
              THEN  Try  (((Assert  (\mneg{}(x  \mmember{}  mFOL-boundvars(left)))  \mwedge{}  (\mneg{}(x  \mmember{}  mFOL-boundvars(right)))  BY
                                                  (Auto
                                                    THEN  OnMaybeHyp  9  (\mbackslash{}h.  (ParallelOp  h
                                                                                                    THEN  RepUR  ``mFOL-boundvars``  0
                                                                                                    THEN  Fold  `mFOL-boundvars`  0
                                                                                                    THEN  BLemma  `member-union`
                                                                                                    THEN  Auto))
                                                    ))\mcdot{}
                                    THEN  Repeat  (AutoSplit\mcdot{})
                                    THEN  EqCD
                                    THEN  Auto))\mcdot{}
              THEN  (RenameVar  `z'  6
                          THEN  (Assert  (\mneg{}(x  =  z))  \mwedge{}  (\mneg{}(x  \mmember{}  mFOL-boundvars(body)))  BY
                                                  (Auto
                                                    THEN  OnMaybeHyp  9  (\mbackslash{}h.  (ParallelOp  h
                                                                                                    THEN  RepUR  ``mFOL-boundvars``  0
                                                                                                    THEN  Fold  `mFOL-boundvars`  0
                                                                                                    THEN  BLemma  `member-insert`
                                                                                                    THEN  Auto))
                                                    ))
                          THEN  (RepeatFor  2  (AutoSplit)
                                      THEN  Try  ((HypSubst'  (-1)  0
                                                            THEN  RepeatFor  2  ((EqCD  THEN  Auto))
                                                            THEN  (SubstFor  \mkleeneopen{}a2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                                                            THEN  (RepUR  ``update-assignment  FOAssignment``  0
                                                                        THEN  EqCD
                                                                        THEN  Auto
                                                                        THEN  AutoSplit)\mcdot{})\mcdot{})
                                      THEN  (EqCD  THEN  Auto)
                                      THEN  BackThruSomeHyp
                                      THEN  Auto
                                      THEN  ((SubstFor  \mkleeneopen{}a2\mkleeneclose{}  0\mcdot{}  THENA  (Auto  THEN  Fold  `FOAssignment`  0  THEN  Auto))
                                                  THEN  RepUR  ``update-assignment  FOAssignment``  0
                                                  THEN  EqCD
                                                  THEN  Auto
                                                  THEN  RepeatFor  3  (AutoSplit))\mcdot{}))\mcdot{})\mcdot{})

---

Home Index