---

Step * 1 4 1 1 of Lemma mFOL-proveable-evidence


1. hyps : mFOL() List@i
2. var : ℤ@i
3. body : mFOL()@i
4. x : ℤ@i
5. mFOL-sequent-evidence(<hyps, body[var/x]>)@i'
⊢ mFOL-sequent-evidence(<hyps, ∃x;body)>)
BY
{ ((D 0 THEN Auto)
   THEN Unfold `mFOL-sequent-abstract` 0
   THEN RepUR ``FOSatWith`` 0
   THEN RW (AddrC [2] (UnfoldC `mFOL-abstract`)) 0
   THEN Reduce 0
   THEN Fold `mFOL-abstract` 0
   THEN RepUR ``FOQuantifier`` 0
   THEN Fold `FOSatWith` 0
   THEN Auto
   THEN RenameVar `z' 2
   THEN With ⌈a z⌉ (D 0)⋅
   THEN Auto
   THEN (InstLemma `mFOL-subst-abstract` [⌈Dom⌉;⌈S⌉;⌈a⌉;⌈body⌉;⌈z⌉;⌈x⌉]⋅ THENA Auto)⋅) }

1
1. hyps : mFOL() List@i
2. z : ℤ@i
3. body : mFOL()@i
4. x : ℤ@i
5. mFOL-sequent-evidence(<hyps, body[z/x]>)@i'
6. [Dom] : Type
7. [S] : FOStruct(Dom)
8. a : FOAssignment(Dom)@i
9. tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps))@i
10. Dom,S,a |= mFOL-abstract(body[z/x]) = Dom,S,a[x := a z] |= mFOL-abstract(body) ∈ ℙ
⊢ Dom,S,a[x := a z] |= mFOL-abstract(body)

---

Latex:



1.  hyps  :  mFOL()  List@i
2.  var  :  \mBbbZ{}@i
3.  body  :  mFOL()@i
4.  x  :  \mBbbZ{}@i
5.  mFOL-sequent-evidence(<hyps,  body[var/x]>)@i'
\mvdash{}  mFOL-sequent-evidence(<hyps,  \mexists{}x;body)>)


By

((D  0  THEN  Auto)
  THEN  Unfold  `mFOL-sequent-abstract`  0
  THEN  RepUR  ``FOSatWith``  0
  THEN  RW  (AddrC  [2]  (UnfoldC  `mFOL-abstract`))  0
  THEN  Reduce  0
  THEN  Fold  `mFOL-abstract`  0
  THEN  RepUR  ``FOQuantifier``  0
  THEN  Fold  `FOSatWith`  0
  THEN  Auto
  THEN  RenameVar  `z'  2
  THEN  With  \mkleeneopen{}a  z\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `mFOL-subst-abstract`  [\mkleeneopen{}Dom\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}body\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{})

---

Home Index