---

Step * of Lemma mFOL-proveable-evidence

∀[s:mFOL-sequent()]. (mFOL-proveable(s) ⇒ mFOL-sequent-evidence(s))
BY
{ (Auto
   THEN D -1
   THEN Assert ⌈∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s))⌉
   ⋅) }

1
.....assertion..... 
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
⊢ ∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s))

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

---

Latex:


\mforall{}[s:mFOL-sequent()].  (mFOL-proveable(s)  {}\mRightarrow{}  mFOL-sequent-evidence(s))


By

(Auto
  THEN  D  -1
  THEN  Assert  \mkleeneopen{}\mforall{}s:mFOL-sequent()
                                (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  {}\mRightarrow{}  mFOL-sequent-evidence(s))\mkleeneclose{}
  \mcdot{})

---

Home Index