---

Step * 1 2 1 of Lemma mFOL-proveable-evidence


1. s : mFOL-sequent()
2. r : FOLRule()
3. ↑isl(mFOLeffect(<s, r>))
4. L : proof-tree(mFOL-sequent();FOLRule();λsr.mFOLeffect(sr)) List
5. ||L|| = ||outl(mFOLeffect(<s, r>))|| ∈ ℤ
6. (∀pf∈L.∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s)))
7. s@0 : mFOL-sequent()
8. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s@0;make-proof-tree(s;r;L))
⊢ mFOL-sequent-evidence(s@0)
BY
{ (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 At ⌜𝕌'⌝ Auto⋅)
   THEN (RevHypSubst' (-2) 0 THENA Auto)
   THEN RepeatFor 2 (Thin (-2))) }

1
1. s : mFOL-sequent()
2. r : FOLRule()
3. x : mFOL-sequent() List
4. mFOLeffect(<s, r>) = (inl x) ∈ (mFOL-sequent() List?)
5. True
6. L : proof-tree(mFOL-sequent();FOLRule();λsr.mFOLeffect(sr)) List
7. ||L|| = ||x|| ∈ ℤ
8. (∀pf∈L.∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s)))
9. ∀i:ℕ||x||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);x[i];L[i])
⊢ mFOL-sequent-evidence(s)

---

Latex:

---

Latex:

1.  s  :  mFOL-sequent()
2.  r  :  FOLRule()
3.  \muparrow{}isl(mFOLeffect(<s,  r>))
4.  L  :  proof-tree(mFOL-sequent();FOLRule();\mlambda{}sr.mFOLeffect(sr))  List
5.  ||L||  =  ||outl(mFOLeffect(<s,  r>))||
6.  (\mforall{}pf\mmember{}L.\mforall{}s:mFOL-sequent()
                        (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  {}\mRightarrow{}  mFOL-sequent-evidence(s)))
7.  s@0  :  mFOL-sequent()
8.  correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s@0;make-proof-tree(s;r;L))
\mvdash{}  mFOL-sequent-evidence(s@0)


By

---

Latex:
(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  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  Auto\mcdot{})
  THEN  (RevHypSubst'  (-2)  0  THENA  Auto)
  THEN  RepeatFor  2  (Thin  (-2)))

---

Home Index