---

Step * of Lemma mFOL-proveable-evidence

No Annotations
∀[s:mFOL-sequent()]. (mFOL-proveable(s) ⇒ mFOL-sequent-evidence(s))
BY
{ TACTIC:(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();FOLRule();λsr.mFOLeffect(sr))
3. [%2] : correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf)
⊢ ∀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();FOLRule();λsr.mFOLeffect(sr))
3. [%2] : correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf)
4. ∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s))
⊢ mFOL-sequent-evidence(s)

---

Latex:

---

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


By

---

Latex:
TACTIC:(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