Step * 2 of Lemma mFOL-abstract-rename


1. Dom Type
2. FOStruct(Dom)
3. : ℤ
4. : ℤ
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 |= mFOL-abstract(left) Dom,S,a1 |= mFOL-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 |= mFOL-abstract(right) Dom,S,a1 |= mFOL-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 |= mFOL-abstract(mFOconnect(knd;left;right))
Dom,S,a1 |= mFOL-abstract(mFOL-rename(mFOconnect(knd;left;right);y;x))
∈ ℙ
BY
((Assert (x ∈ mFOL-boundvars(left))) ∧ (x ∈ mFOL-boundvars(right))) BY
          OnMaybeHyp 10 (\h. (RepUR ``mFOL-boundvars`` h
                              THEN Fold `mFOL-boundvars` h
                              THEN 0
                              THEN ParallelOp h
                              THEN BLemma `member-union`
                              THEN Auto)))
   THEN ExRepD
   THEN RepeatFor (ThinTrivial)) }

1
1. Dom Type
2. FOStruct(Dom)
3. : ℤ
4. : ℤ
5. knd Atom
6. left mFOL()
7. right mFOL()
8. ¬(x ∈ mFOL-boundvars(mFOconnect(knd;left;right)))
9. a1 FOAssignment(mFOL-freevars(mFOL-rename(mFOconnect(knd;left;right);y;x)),Dom)
10. a2 FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom)
11. a2
FOAssigment-rename(a1;mFOconnect(knd;left;right);x;y)
∈ FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom)
12. ¬(x ∈ mFOL-boundvars(left))
13. ¬(x ∈ mFOL-boundvars(right))
14. ∀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 |= mFOL-abstract(right) Dom,S,a1 |= mFOL-abstract(mFOL-rename(right;y;x)) ∈ ℙ))
15. ∀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 |= mFOL-abstract(left) Dom,S,a1 |= mFOL-abstract(mFOL-rename(left;y;x)) ∈ ℙ))
⊢ Dom,S,a2 |= mFOL-abstract(mFOconnect(knd;left;right))
Dom,S,a1 |= mFOL-abstract(mFOL-rename(mFOconnect(knd;left;right);y;x))
∈ ℙ


Latex:


Latex:

1.  Dom  :  Type
2.  S  :  FOStruct(Dom)
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  knd  :  Atom
6.  left  :  mFOL()
7.  right  :  mFOL()
8.  (\mneg{}(x  \mmember{}  mFOL-boundvars(left)))
{}\mRightarrow{}  (\mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(left;y;x)),Dom).
        \mforall{}a2:FOAssignment(mFOL-freevars(left),Dom).
            ((a2  =  FOAssigment-rename(a1;left;x;y))
            {}\mRightarrow{}  (Dom,S,a2  |=  mFOL-abstract(left)  =  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(left;y;x)))))
9.  (\mneg{}(x  \mmember{}  mFOL-boundvars(right)))
{}\mRightarrow{}  (\mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(right;y;x)),Dom).
        \mforall{}a2:FOAssignment(mFOL-freevars(right),Dom).
            ((a2  =  FOAssigment-rename(a1;right;x;y))
            {}\mRightarrow{}  (Dom,S,a2  |=  mFOL-abstract(right)  =  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(right;y;x)))))
10.  \mneg{}(x  \mmember{}  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)
\mvdash{}  Dom,S,a2  |=  mFOL-abstract(mFOconnect(knd;left;right))
=  Dom,S,a1  |=  mFOL-abstract(mFOL-rename(mFOconnect(knd;left;right);y;x))


By


Latex:
((Assert  (\mneg{}(x  \mmember{}  mFOL-boundvars(left)))  \mwedge{}  (\mneg{}(x  \mmember{}  mFOL-boundvars(right)))  BY
                OnMaybeHyp  10  (\mbackslash{}h.  (RepUR  ``mFOL-boundvars``  h
                                                        THEN  Fold  `mFOL-boundvars`  h
                                                        THEN  D  0
                                                        THEN  ParallelOp  h
                                                        THEN  BLemma  `member-union`
                                                        THEN  Auto)))
  THEN  ExRepD
  THEN  RepeatFor  2  (ThinTrivial))




Home Index