---

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


1. hyps : mFOL() List
2. concl : mFOL()
3. var : ℤ
4. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
5. ↑mFOquant?(concl)
6. mFOquant-isall(concl) = ff
7. mFOL-sequent-evidence(<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
BY
{ ((Assert concl = ∃mFOquant-var(concl);mFOquant-body(concl)) ∈ mFOL() BY
          (MoveToConcl 2
           THEN BLemmaUp `mFOL-induction`
           THEN Reduce 0
           THEN Auto
           THEN Try ((Fold `AbstractFOFormula` 0 THEN Auto))
           THEN Unfold `mFOL-sequent` 0
           THEN Auto))⋅
   THEN (MoveToConcl 4 THEN (HypSubst' -1 0 THENA Auto))
   THEN MoveToConcl (-2)
   THEN GenConclAtAddr [1;1;2;3]
   THEN Thin (-1)
   THEN RenameVar `body' (-1)
   THEN GenConclAtAddr [1;1;2;2]
   THEN Thin (-1)
   THEN RenameVar `x' (-1)
   THEN Auto
   THEN (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 Auto
   THEN ThinVar `concl'
   THEN RenameVar `z' 2)⋅ }

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

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  var  :  \mBbbZ{}
4.  (var  \mmember{}  mFOL-sequent-freevars(<hyps,  concl>))
5.  \muparrow{}mFOquant?(concl)
6.  mFOquant-isall(concl)  =  ff
7.  mFOL-sequent-evidence(<hyps,  mFOquant-body(concl)[var/mFOquant-var(concl)]>)
\mvdash{}  mFOL-sequent-evidence(<hyps,  concl>)


By

---

Latex:
((Assert  concl  =  \mexists{}mFOquant-var(concl);mFOquant-body(concl))  BY
                (MoveToConcl  2
                  THEN  BLemmaUp  `mFOL-induction`
                  THEN  Reduce  0
                  THEN  Auto
                  THEN  Try  ((Fold  `AbstractFOFormula`  0  THEN  Auto))
                  THEN  Unfold  `mFOL-sequent`  0
                  THEN  Auto))\mcdot{}
  THEN  (MoveToConcl  4  THEN  (HypSubst'  -1  0  THENA  Auto))
  THEN  MoveToConcl  (-2)
  THEN  GenConclAtAddr  [1;1;2;3]
  THEN  Thin  (-1)
  THEN  RenameVar  `body'  (-1)
  THEN  GenConclAtAddr  [1;1;2;2]
  THEN  Thin  (-1)
  THEN  RenameVar  `x'  (-1)
  THEN  Auto
  THEN  (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  Auto
  THEN  ThinVar  `concl'
  THEN  RenameVar  `z'  2)\mcdot{}

---

Home Index