---

Step * 1 12 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. ∃d:Dom. Dom,S,a[y := d] |= mFOL-abstract(B)
⊢ Dom,S,a |= mFOL-abstract(concl)
BY
{ (D (-1)
   THEN (InstLemma `mFOL-abstract-functionality` [⌈concl⌉;⌈Dom⌉;⌈S⌉;⌈a⌉;⌈a[z := d]⌉]⋅
         THENA (Auto
                THEN RepUR ``update-assignment`` 0
                THEN AutoSplit
                THEN OnMaybeHyp 8 (\h. (D h THEN Complete (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) ∈ ℙ
⊢ 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.  \mexists{}d:Dom.  Dom,S,a[y  :=  d]  |=  mFOL-abstract(B)
\mvdash{}  Dom,S,a  |=  mFOL-abstract(concl)


By

(D  (-1)
  THEN  (InstLemma  `mFOL-abstract-functionality`  [\mkleeneopen{}concl\mkleeneclose{};\mkleeneopen{}Dom\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a[z  :=  d]\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  RepUR  ``update-assignment``  0
                            THEN  AutoSplit
                            THEN  OnMaybeHyp  8  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto))))
              )
  )

---

Home Index