---

Step * 1 1 of Lemma mFOL-proveable-evidence

.....antecedent..... 
∀s:mFOL-sequent(). ∀r:FOLRule().
  ∀s@0:mFOL-sequent()
    (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s@0;proof-abort(s;r)) ⇒ mFOL-sequent-evidence(s@0)) 
  supposing ↑isr((λsr.mFOLeffect(sr)) <s, r>)
BY
{ ((Reduce 0 THEN Auto)
   THEN RecUnfold `correct_proof` (-1)
   THEN Repeat (MoveToConcl (-1)⋅)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RepUR ``proof-abort make-proof-tree`` 0
   THEN (GenConclTerm ⌜mFOLeffect(<s, r>)⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
\mforall{}s:mFOL-sequent().  \mforall{}r:FOLRule().
    \mforall{}s@0:mFOL-sequent()
        (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s@0;proof-abort(s;r))
        {}\mRightarrow{}  mFOL-sequent-evidence(s@0)) 
    supposing  \muparrow{}isr((\mlambda{}sr.mFOLeffect(sr))  <s,  r>)


By

---

Latex:
((Reduce  0  THEN  Auto)
  THEN  RecUnfold  `correct\_proof`  (-1)
  THEN  Repeat  (MoveToConcl  (-1)\mcdot{})
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepUR  ``proof-abort  make-proof-tree``  0
  THEN  (GenConclTerm  \mkleeneopen{}mFOLeffect(<s,  r>)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index