---

Step * 2 of Lemma FOL-proveable-evidence


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)
BY
{ ((Assert correct_proof(mFOL-sequent();λsr.FOLeffect(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:

---

Latex:

1.  [s]  :  mFOL-sequent()
2.  pf  :  proof-tree(mFOL-sequent();FOLRule();\mlambda{}sr.FOLeffect(sr))
3.  [\%2]  :  correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(sr);s;pf)
4.  \mforall{}s:mFOL-sequent()
          (correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(sr);s;pf)  {}\mRightarrow{}  FOL-sequent-evidence\{i:l\}(s))
\mvdash{}  FOL-sequent-evidence\{i:l\}(s)


By

---

Latex:
((Assert  correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(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