---

Step * 1 12 1 1 1 2 of Lemma mFOL-proveable-evidence


1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. hypnum : ℕ@i
5. z : ℤ@i
6. ¬(z ∈ mFOL-freevars(concl))
7. hypnum < ||hyps||
8. (∀h∈hyps.¬(z ∈ mFOL-freevars(h)))
9. ↑mFOquant?(hyps[hypnum])
10. mFOquant-isall(hyps[hypnum]) = ff
11. [Dom] : Type
12. [S] : FOStruct(Dom)
13. a : FOAssignment(Dom)@i
14. tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps))@i
15. B : mFOL()@i
16. mFOquant-body(hyps[hypnum]) = B ∈ mFOL()@i
17. y : ℤ@i
18. mFOquant-var(hyps[hypnum]) = y ∈ ℤ@i
19. mFOL-sequent-evidence(<[B[z/y] / hyps], concl>)@i'
20. hyps[hypnum] = ∃y;B) ∈ mFOL()@i
21. Dom,S,a |= mFOL-abstract(∃y;B))
⊢ ∃d:Dom. Dom,S,a[y := d] |= mFOL-abstract(B)
BY
{ (RepUR ``mFOL-abstract`` (-1)
   THEN Fold `mFOL-abstract` (-1)
   THEN RepUR ``FOSatWith FOQuantifier`` -1
   THEN Fold `FOSatWith` (-1)
   THEN Auto) }

---

Latex:



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


By

(RepUR  ``mFOL-abstract``  (-1)
  THEN  Fold  `mFOL-abstract`  (-1)
  THEN  RepUR  ``FOSatWith  FOQuantifier``  -1
  THEN  Fold  `FOSatWith`  (-1)
  THEN  Auto)

---

Home Index