---

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


1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. var : ℤ@i
4. ↑mFOquant?(concl)
5. mFOquant-isall(concl) = ff
6. 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 (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 ThinVar `concl')⋅ }

1
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)>)

---

Latex:



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


By

((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  (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  ThinVar  `concl')\mcdot{}

---

Home Index