Step
*
3
of Lemma
mFOL-abstract-rename
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. isall : 𝔹
6. var : ℤ
7. body : mFOL()
8. (¬(x ∈ mFOL-boundvars(body)))
⇒ (∀a1:FOAssignment(mFOL-freevars(mFOL-rename(body;y;x)),Dom). ∀a2:FOAssignment(mFOL-freevars(body),Dom).
((a2 = FOAssigment-rename(a1;body;x;y) ∈ FOAssignment(mFOL-freevars(body),Dom))
⇒ (Dom,S,a2 |= mFOL-abstract(body) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ)))
9. ¬(x ∈ mFOL-boundvars(mFOquant(isall;var;body)))
10. a1 : FOAssignment(mFOL-freevars(mFOL-rename(mFOquant(isall;var;body);y;x)),Dom)
11. a2 : FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom)
12. a2 = FOAssigment-rename(a1;mFOquant(isall;var;body);x;y) ∈ FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom)
⊢ Dom,S,a2 |= mFOL-abstract(mFOquant(isall;var;body))
= Dom,S,a1 |= mFOL-abstract(mFOL-rename(mFOquant(isall;var;body);y;x))
∈ ℙ
BY
{ ((RenameVar `z' 6 THEN All (Unfold `FOAssigment-rename`))
THEN ((Assert (¬(x = z ∈ ℤ)) ∧ (¬(x ∈ mFOL-boundvars(body))) BY
(Auto
THEN OnMaybeHyp 10 (\h. (ParallelOp h
THEN RepUR ``mFOL-boundvars`` 0
THEN Fold `mFOL-boundvars` 0
THEN BLemma `member-insert`
THEN Auto))
))
THEN D -1
)
THEN RepeatFor 2 (ThinTrivial)
THEN (RepUR ``mFOL-rename`` 0⋅ THEN Fold `mFOL-rename` 0)
THEN (RepUR ``mFOL-abstract`` 0⋅ THEN Fold `mFOL-abstract` 0)
THEN RepUR ``FOSatWith FOQuantifier`` 0
THEN Fold `FOSatWith` 0
THEN (BoolCase ⌜isall⌝⋅ THENA Auto)
THEN (BoolCase ⌜(z =z y)⌝⋅ THENA Auto)
THEN Try ((HypSubst' (-1) 0
THEN RepeatFor 3 ((EqCD THEN Auto))
THEN Unfold `FOAssignment` 0
THEN FunExt
THEN Reduce 0
THEN Auto
THEN D -1
THEN (Assert (x1 ∈ mFOL-freevars(mFOquant(isall;z;body))) BY
(HypSubst' (-4) 0 THEN RepUR ``mFOL-freevars`` 0 THEN Fold `mFOL-freevars` 0 THEN Auto))
THEN (RWO "member_filter" (-2) THENA Auto)
THEN D -2
THEN Reduce (-2)
THEN OnMaybeHyp 14 (\h. (Unfold `FOAssignment` h
THEN (ApFunToHypEquands `Z' ⌜Z x1⌝ ⌜Dom⌝ h⋅ THENA Complete (Auto))
THEN SplitOnHypITE -1
THEN Auto
THEN RepUR ``update-assignment`` -2
THEN SplitOnHypITE -2
THEN Auto))))
THEN (EqCD THENA Auto)
THEN Try ((Fold `member` 0 THEN Auto))) }
1
.....subterm..... T:t
2:n
1. Dom : Type
2. S : FOStruct(Dom)
3. x : ℤ
4. y : ℤ
5. isall : 𝔹
6. z : ℤ
7. z ≠ y
8. body : mFOL()
9. ¬(x ∈ mFOL-boundvars(mFOquant(isall;z;body)))
10. a1 : FOAssignment(mFOL-freevars(mFOL-rename(mFOquant(isall;z;body);y;x)),Dom)
11. a2 : FOAssignment(mFOL-freevars(mFOquant(isall;z;body)),Dom)
12. a2
= if y ∈b mFOL-freevars(mFOquant(isall;z;body)) then a1[y := a1 x] else a1 fi
∈ FOAssignment(mFOL-freevars(mFOquant(isall;z;body)),Dom)
13. ¬(x = z ∈ ℤ)
14. ¬(x ∈ mFOL-boundvars(body))
15. ∀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)) ∈ ℙ))
16. ↑isall
17. v : Dom
⊢ Dom,S,a2[z := v] |= mFOL-abstract(body) = Dom,S,a1[z := v] |= mFOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ
2
.....subterm..... T:t
2:n
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(mFOL-freevars(mFOL-rename(∃z;body);y;x)),Dom)
12. a2 : FOAssignment(mFOL-freevars(∃z;body)),Dom)
13. a2 = if y ∈b mFOL-freevars(∃z;body)) then a1[y := a1 x] else a1 fi ∈ FOAssignment(mFOL-freevars(∃z;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
⊢ Dom,S,a2[z := v] |= mFOL-abstract(body) = Dom,S,a1[z := v] |= mFOL-abstract(mFOL-rename(body;y;x)) ∈ ℙ
Latex:
Latex:
1. Dom : Type
2. S : FOStruct(Dom)
3. x : \mBbbZ{}
4. y : \mBbbZ{}
5. isall : \mBbbB{}
6. var : \mBbbZ{}
7. body : mFOL()
8. (\mneg{}(x \mmember{} mFOL-boundvars(body)))
{}\mRightarrow{} (\mforall{}a1:FOAssignment(mFOL-freevars(mFOL-rename(body;y;x)),Dom).
\mforall{}a2:FOAssignment(mFOL-freevars(body),Dom).
((a2 = FOAssigment-rename(a1;body;x;y))
{}\mRightarrow{} (Dom,S,a2 |= mFOL-abstract(body) = Dom,S,a1 |= mFOL-abstract(mFOL-rename(body;y;x)))))
9. \mneg{}(x \mmember{} mFOL-boundvars(mFOquant(isall;var;body)))
10. a1 : FOAssignment(mFOL-freevars(mFOL-rename(mFOquant(isall;var;body);y;x)),Dom)
11. a2 : FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom)
12. a2 = FOAssigment-rename(a1;mFOquant(isall;var;body);x;y)
\mvdash{} Dom,S,a2 |= mFOL-abstract(mFOquant(isall;var;body))
= Dom,S,a1 |= mFOL-abstract(mFOL-rename(mFOquant(isall;var;body);y;x))
By
Latex:
((RenameVar `z' 6 THEN All (Unfold `FOAssigment-rename`))
THEN ((Assert (\mneg{}(x = z)) \mwedge{} (\mneg{}(x \mmember{} mFOL-boundvars(body))) BY
(Auto
THEN OnMaybeHyp 10 (\mbackslash{}h. (ParallelOp h
THEN RepUR ``mFOL-boundvars`` 0
THEN Fold `mFOL-boundvars` 0
THEN BLemma `member-insert`
THEN Auto))
))
THEN D -1
)
THEN RepeatFor 2 (ThinTrivial)
THEN (RepUR ``mFOL-rename`` 0\mcdot{} THEN Fold `mFOL-rename` 0)
THEN (RepUR ``mFOL-abstract`` 0\mcdot{} THEN Fold `mFOL-abstract` 0)
THEN RepUR ``FOSatWith FOQuantifier`` 0
THEN Fold `FOSatWith` 0
THEN (BoolCase \mkleeneopen{}isall\mkleeneclose{}\mcdot{} THENA Auto)
THEN (BoolCase \mkleeneopen{}(z =\msubz{} y)\mkleeneclose{}\mcdot{} THENA Auto)
THEN Try ((HypSubst' (-1) 0
THEN RepeatFor 3 ((EqCD THEN Auto))
THEN Unfold `FOAssignment` 0
THEN FunExt
THEN Reduce 0
THEN Auto
THEN D -1
THEN (Assert (x1 \mmember{} mFOL-freevars(mFOquant(isall;z;body))) BY
(HypSubst' (-4) 0
THEN RepUR ``mFOL-freevars`` 0
THEN Fold `mFOL-freevars` 0
THEN Auto))
THEN (RWO "member\_filter" (-2) THENA Auto)
THEN D -2
THEN Reduce (-2)
THEN OnMaybeHyp 14 (\mbackslash{}h. (Unfold `FOAssignment` h
THEN (ApFunToHypEquands `Z' \mkleeneopen{}Z x1\mkleeneclose{} \mkleeneopen{}Dom\mkleeneclose{} h\mcdot{}
THENA Complete (Auto)
)
THEN SplitOnHypITE -1
THEN Auto
THEN RepUR ``update-assignment`` -2
THEN SplitOnHypITE -2
THEN Auto))))
THEN (EqCD THENA Auto)
THEN Try ((Fold `member` 0 THEN Auto)))
Home
Index