---

Step * 2 of Lemma mFOL-proveable-evidence


1. [s] : mFOL-sequent()
2. pf : proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i
3. \\%2 : correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf)@i
4. ∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s))
⊢ mFOL-sequent-evidence(s)
BY
{ ((Assert correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) BY
          (Unhide THEN Auto))
   THEN Assert ⌈(fst(fst(pf))) = s ∈ mFOL-sequent()⌉⋅
   THEN Try ((InstHyp [⌈fst(fst(pf))⌉] (-3)⋅ THEN Complete (Auto)))
   THEN DProofTree 2
   THEN RecUnfold `correct_proof` (-1)
   THEN Reduce (-1)
   THEN D -1
   THEN Reduce 0
   THEN Hypothesis) }

---

Latex:



1.  [s]  :  mFOL-sequent()
2.  pf  :  proof-tree(mFOL-sequent();mFOLRule();\mlambda{}sr.mFOLeffect(sr))@i
3.  \mbackslash{}\mbackslash{}\%2  :  correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)@i
4.  \mforall{}s:mFOL-sequent()
          (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  {}\mRightarrow{}  mFOL-sequent-evidence(s))
\mvdash{}  mFOL-sequent-evidence(s)


By

((Assert  correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  BY
                (Unhide  THEN  Auto))
  THEN  Assert  \mkleeneopen{}(fst(fst(pf)))  =  s\mkleeneclose{}\mcdot{}
  THEN  Try  ((InstHyp  [\mkleeneopen{}fst(fst(pf))\mkleeneclose{}]  (-3)\mcdot{}  THEN  Complete  (Auto)))
  THEN  DProofTree  2
  THEN  RecUnfold  `correct\_proof`  (-1)
  THEN  Reduce  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Hypothesis)

---

Home Index