Step
*
2
of Lemma
mFOL-abstract-rename
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
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 D 0
THEN ParallelOp h
THEN BLemma `member-union`
THEN Auto)))
THEN ExRepD
THEN RepeatFor 2 (ThinTrivial)) }
1
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
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