---

Step * 1 12 1 1 of Lemma FOL-proveable-evidence


1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. z : ℤ
6. ¬(z ∈ mFOL-sequent-freevars(<hyps, concl>))
7. hypnum < ||hyps||
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = ff
10. [Dom] : Type
11. [S] : FOStruct+{i:l}(Dom)
12. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
13. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
14. B : mFOL()
15. mFOquant-body(hyps[hypnum]) = B ∈ mFOL()
16. y : ℤ
17. mFOquant-var(hyps[hypnum]) = y ∈ ℤ
18. FOL-sequent-evidence{i:l}(<[B[z/y] / hyps], concl>)
19. hyps[hypnum] = ∃y;B) ∈ mFOL()
⊢ Dom,S,a +|= FOL-abstract(concl)
BY
{ Assert ⌜Dom,S,a +|= FOL-abstract(∃y;B))⌝⋅ }

1
.....assertion..... 
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. z : ℤ
6. ¬(z ∈ mFOL-sequent-freevars(<hyps, concl>))
7. hypnum < ||hyps||
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = ff
10. [Dom] : Type
11. [S] : FOStruct+{i:l}(Dom)
12. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
13. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
14. B : mFOL()
15. mFOquant-body(hyps[hypnum]) = B ∈ mFOL()
16. y : ℤ
17. mFOquant-var(hyps[hypnum]) = y ∈ ℤ
18. FOL-sequent-evidence{i:l}(<[B[z/y] / hyps], concl>)
19. hyps[hypnum] = ∃y;B) ∈ mFOL()
⊢ Dom,S,a +|= FOL-abstract(∃y;B))

2
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. z : ℤ
6. ¬(z ∈ mFOL-sequent-freevars(<hyps, concl>))
7. hypnum < ||hyps||
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = ff
10. [Dom] : Type
11. [S] : FOStruct+{i:l}(Dom)
12. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
13. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
14. B : mFOL()
15. mFOquant-body(hyps[hypnum]) = B ∈ mFOL()
16. y : ℤ
17. mFOquant-var(hyps[hypnum]) = y ∈ ℤ
18. FOL-sequent-evidence{i:l}(<[B[z/y] / hyps], concl>)
19. hyps[hypnum] = ∃y;B) ∈ mFOL()
20. Dom,S,a +|= FOL-abstract(∃y;B))
⊢ Dom,S,a +|= FOL-abstract(concl)

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  subgoals  :  mFOL-sequent()  List
4.  hypnum  :  \mBbbN{}
5.  z  :  \mBbbZ{}
6.  \mneg{}(z  \mmember{}  mFOL-sequent-freevars(<hyps,  concl>))
7.  hypnum  <  ||hyps||
8.  \muparrow{}mFOquant?(hyps[hypnum])
9.  mFOquant-isall(hyps[hypnum])  =  ff
10.  [Dom]  :  Type
11.  [S]  :  FOStruct+\{i:l\}(Dom)
12.  a  :  FOAssignment(mFOL-sequent-freevars(<hyps,  concl>),Dom)
13.  tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
14.  B  :  mFOL()
15.  mFOquant-body(hyps[hypnum])  =  B
16.  y  :  \mBbbZ{}
17.  mFOquant-var(hyps[hypnum])  =  y
18.  FOL-sequent-evidence\{i:l\}(<[B[z/y]  /  hyps],  concl>)
19.  hyps[hypnum]  =  \mexists{}y;B)
\mvdash{}  Dom,S,a  +|=  FOL-abstract(concl)


By

---

Latex:
Assert  \mkleeneopen{}Dom,S,a  +|=  FOL-abstract(\mexists{}y;B))\mkleeneclose{}\mcdot{}

---

Home Index