Step
*
1
11
1
2
2
2
1
1
of Lemma
FOL-proveable-evidence
.....antecedent.....
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. var : ℤ
6. hypnum < ||hyps||
7. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. ∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
∀a:FOAssignment(mFOL-sequent-freevars(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps]
, concl
>),Dom)
Dom,S,a +|= FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
11. hyps[hypnum] = ∀mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum])) ∈ mFOL()
12. mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum]) ⊆ mFOL-sequent-freevars(<hyps
, mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]
>)
14. ¬(mFOquant-var(hyps[hypnum]) ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
= FOL-abstract(mFOquant-body(hyps[hypnum]))
∈ AbstractFOFormula+(mFOL-freevars(mFOquant-body(hyps[hypnum])))
16. [Dom] : Type
17. [S] : FOStruct+{i:l}(Dom)
18. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
19. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
⊢ tuple-type(FOL-hyps-meaning(Dom;S;a;[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps]))
BY
{ Assert ⌜Dom,S,a +|= FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])⌝⋅ }
1
.....assertion.....
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. var : ℤ
6. hypnum < ||hyps||
7. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. ∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
∀a:FOAssignment(mFOL-sequent-freevars(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps]
, concl
>),Dom)
Dom,S,a +|= FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
11. hyps[hypnum] = ∀mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum])) ∈ mFOL()
12. mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum]) ⊆ mFOL-sequent-freevars(<hyps
, mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]
>)
14. ¬(mFOquant-var(hyps[hypnum]) ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
= FOL-abstract(mFOquant-body(hyps[hypnum]))
∈ AbstractFOFormula+(mFOL-freevars(mFOquant-body(hyps[hypnum])))
16. [Dom] : Type
17. [S] : FOStruct+{i:l}(Dom)
18. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
19. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
⊢ Dom,S,a +|= FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
2
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. var : ℤ
6. hypnum < ||hyps||
7. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. ∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
∀a:FOAssignment(mFOL-sequent-freevars(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps]
, concl
>),Dom)
Dom,S,a +|= FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
11. hyps[hypnum] = ∀mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum])) ∈ mFOL()
12. mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum]) ⊆ mFOL-sequent-freevars(<hyps
, mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]
>)
14. ¬(mFOquant-var(hyps[hypnum]) ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
= FOL-abstract(mFOquant-body(hyps[hypnum]))
∈ AbstractFOFormula+(mFOL-freevars(mFOquant-body(hyps[hypnum])))
16. [Dom] : Type
17. [S] : FOStruct+{i:l}(Dom)
18. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
19. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
20. Dom,S,a +|= FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
⊢ tuple-type(FOL-hyps-meaning(Dom;S;a;[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps]))
Latex:
Latex:
.....antecedent.....
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : \mBbbN{}
5. var : \mBbbZ{}
6. hypnum < ||hyps||
7. (var \mmember{} mFOL-sequent-freevars(<hyps, concl>))
8. \muparrow{}mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. \mforall{}[Dom:Type]. \mforall{}[S:FOStruct+\{i:l\}(Dom)].
\mforall{}a:FOAssignment(mFOL-sequent-freevars(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(...)] /
hyps]
, concl
>),Dom)
Dom,S,a +|= FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(...)] /
hyps]
, concl
>)
11. hyps[hypnum] = \mforall{}mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum]))
12. mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
\msubseteq{} mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum])
\msubseteq{} mFOL-sequent-freevars(<hyps, mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]>)
14. \mneg{}(mFOquant-var(hyps[hypnum]) \mmember{} mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
= FOL-abstract(mFOquant-body(hyps[hypnum]))
16. [Dom] : Type
17. [S] : FOStruct+\{i:l\}(Dom)
18. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
19. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
\mvdash{} tuple-type(FOL-hyps-meaning(Dom;S;a;[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[...])] /
hyps]))
By
Latex:
Assert \mkleeneopen{}Dom,S,a +|= FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])\mkleeneclose{}\mcdot{}
Home
Index