---

Step * of Lemma FOL-proveable-evidence

No Annotations
∀[s:mFOL-sequent()]. (FOL-proveable(s) ⇒ FOL-sequent-evidence{i:l}(s))
BY
{ (Auto
   THEN D -1
   THEN Assert ⌜∀s:mFOL-sequent()
                  (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;pf) ⇒ FOL-sequent-evidence{i:l}(s))⌝⋅) }

1
.....assertion..... 
1. [s] : mFOL-sequent()
2. pf : proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
3. [%2] : correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;pf)
⊢ ∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;pf) ⇒ FOL-sequent-evidence{i:l}(s))

2
1. [s] : mFOL-sequent()
2. pf : proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
3. [%2] : correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;pf)
4. ∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;pf) ⇒ FOL-sequent-evidence{i:l}(s))
⊢ FOL-sequent-evidence{i:l}(s)

---

Latex:

---

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


By

---

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

---

Home Index