---

Step * 1 4 of Lemma FOL-proveable-evidence


1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. var : ℤ
8. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
9. ↑mFOquant?(concl)
10. mFOquant-isall(concl) = ff
11. [<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>] = subgoals ∈ (mFOL-sequent() List)
12. FOL-sequent-evidence{i:l}(<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)
BY
{ (ThinVar `subgoals'
   THEN ((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 `FOL-sequent-abstract` 0
         THEN RepUR ``FOSatWith+`` 0
         THEN RW (AddrC [2] (UnfoldC `FOL-abstract`)) 0
         THEN Reduce 0
         THEN Fold `FOL-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. FOL-sequent-evidence{i:l}(<hyps, body[z/x]>)
6. (z ∈ mFOL-sequent-freevars(<hyps, ∃x;body)>))
7. [Dom] : Type
8. [S] : FOStruct+{i:l}(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, ∃x;body)>),Dom)
10. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
⊢ (∃v:Dom. Dom,S,a[x := v] +|= FOL-abstract(body)) ⋃ (S "false" [])

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  subgoals  :  mFOL-sequent()  List
4.  subproofs  :  \mBbbN{}||subgoals||  {}\mrightarrow{}  proof-tree(mFOL-sequent();FOLRule();\mlambda{}sr.FOLeffect(sr))
5.  \mforall{}b:\mBbbN{}||subgoals||.  \mforall{}s:mFOL-sequent().
          (correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(sr);s;subproofs  b)  {}\mRightarrow{}  FOL-sequent-evidence\{i:l\}(s))
6.  \mforall{}i:\mBbbN{}||subgoals||.  correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(sr);subgoals[i];subproofs  i)
7.  var  :  \mBbbZ{}
8.  (var  \mmember{}  mFOL-sequent-freevars(<hyps,  concl>))
9.  \muparrow{}mFOquant?(concl)
10.  mFOquant-isall(concl)  =  ff
11.  [<hyps,  mFOquant-body(concl)[var/mFOquant-var(concl)]>]  =  subgoals
12.  FOL-sequent-evidence\{i:l\}(<hyps,  mFOquant-body(concl)[var/mFOquant-var(concl)]>)
\mvdash{}  FOL-sequent-evidence\{i:l\}(<hyps,  concl>)


By

---

Latex:
(ThinVar  `subgoals'
  THEN  ((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  `FOL-sequent-abstract`  0
              THEN  RepUR  ``FOSatWith+``  0
              THEN  RW  (AddrC  [2]  (UnfoldC  `FOL-abstract`))  0
              THEN  Reduce  0
              THEN  Fold  `FOL-abstract`  0
              THEN  RepUR  ``FOQuantifier+``  0
              THEN  Auto
              THEN  ThinVar  `concl'
              THEN  RenameVar  `z'  2)\mcdot{}
  )

---

Home Index