---

Step * 1 12 1 1 2 1 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. d : Dom
22. Dom,S,a[y := d] |= mFOL-abstract(B)
23. Dom,S,a |= mFOL-abstract(concl) = Dom,S,a[z := d] |= mFOL-abstract(concl) ∈ ℙ
⊢ Dom,S,a |= mFOL-abstract(concl)
BY
{ (Assert tuple-type(map(λh.Dom,S,a[z := d] |= mFOL-abstract(h);hyps)) BY
         (NthHypEq (-10)
          THEN EqCD
          THEN Auto
          THEN (MoveToConcl 8
                THEN All Thin
                THEN ListInd 1
                THEN Reduce 0
                THEN Auto
                THEN (RWO "l_all_cons" (-1) THENA Auto)
                THEN EqCD
                THEN Auto
                THEN BLemma `mFOL-abstract-functionality`
                THEN Auto
                THEN RepUR ``update-assignment`` 0
                THEN AutoSplit
                THEN D (-6)
                THEN Auto)⋅)) }

1
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. d : Dom
22. Dom,S,a[y := d] |= mFOL-abstract(B)
23. Dom,S,a |= mFOL-abstract(concl) = Dom,S,a[z := d] |= mFOL-abstract(concl) ∈ ℙ
24. tuple-type(map(λh.Dom,S,a[z := d] |= mFOL-abstract(h);hyps))
⊢ Dom,S,a |= mFOL-abstract(concl)

---

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.  d  :  Dom
22.  Dom,S,a[y  :=  d]  |=  mFOL-abstract(B)
23.  Dom,S,a  |=  mFOL-abstract(concl)  =  Dom,S,a[z  :=  d]  |=  mFOL-abstract(concl)
\mvdash{}  Dom,S,a  |=  mFOL-abstract(concl)


By

(Assert  tuple-type(map(\mlambda{}h.Dom,S,a[z  :=  d]  |=  mFOL-abstract(h);hyps))  BY
              (NthHypEq  (-10)
                THEN  EqCD
                THEN  Auto
                THEN  (MoveToConcl  8
                            THEN  All  Thin
                            THEN  ListInd  1
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  (RWO  "l\_all\_cons"  (-1)  THENA  Auto)
                            THEN  EqCD
                            THEN  Auto
                            THEN  BLemma  `mFOL-abstract-functionality`
                            THEN  Auto
                            THEN  RepUR  ``update-assignment``  0
                            THEN  AutoSplit
                            THEN  D  (-6)
                            THEN  Auto)\mcdot{}))

---

Home Index