---

Step * 1 2 of Lemma mFOL-proveable-evidence

.....antecedent..... 
∀s:mFOL-sequent(). ∀r:FOLRule().
  ∀L:proof-tree(mFOL-sequent();FOLRule();λsr.mFOLeffect(sr)) List
    (∀pf∈L.∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s)))
    ⇒ (∀s@0:mFOL-sequent()
          (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s@0;make-proof-tree(s;r;L)) ⇒ mFOL-sequent-evidence(s@0))) 
    supposing ||L|| = ||outl((λsr.mFOLeffect(sr)) <s, r>)|| ∈ ℤ 
  supposing ↑isl((λsr.mFOLeffect(sr)) <s, r>)
BY
{ (Reduce 0 THEN At ⌜𝕌'⌝ Auto⋅) }

1
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)

---

Latex:

---

Latex:
.....antecedent..... 
\mforall{}s:mFOL-sequent().  \mforall{}r:FOLRule().
    \mforall{}L:proof-tree(mFOL-sequent();FOLRule();\mlambda{}sr.mFOLeffect(sr))  List
        (\mforall{}pf\mmember{}L.\mforall{}s:mFOL-sequent()
                          (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  {}\mRightarrow{}  mFOL-sequent-evidence(s)))
        {}\mRightarrow{}  (\mforall{}s@0:mFOL-sequent()
                    (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s@0;make-proof-tree(s;r;L))
                    {}\mRightarrow{}  mFOL-sequent-evidence(s@0))) 
        supposing  ||L||  =  ||outl((\mlambda{}sr.mFOLeffect(sr))  <s,  r>)|| 
    supposing  \muparrow{}isl((\mlambda{}sr.mFOLeffect(sr))  <s,  r>)


By

---

Latex:
(Reduce  0  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  Auto\mcdot{})

---

Home Index