---

Step * 1 of Lemma mFOL-proveable-evidence

.....assertion..... 
1. [s] : mFOL-sequent()
2. pf : proof-tree(mFOL-sequent();FOLRule();λsr.mFOLeffect(sr))
3. [%2] : correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf)
⊢ ∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s))
BY
{ (All Thin
   THEN MoveToConcl (-1)
   THEN InstLemmaUp `proof-tree-induction-ext` [⌜mFOL-sequent()⌝;⌜FOLRule()⌝;⌜λsr.mFOLeffect(sr)⌝;
   ⌜λ2pf.∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s))⌝]⋅
   THEN Try (Complete (Auto))) }

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

2
.....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>)

---

Latex:

---

Latex:
.....assertion..... 
1.  [s]  :  mFOL-sequent()
2.  pf  :  proof-tree(mFOL-sequent();FOLRule();\mlambda{}sr.mFOLeffect(sr))
3.  [\%2]  :  correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)
\mvdash{}  \mforall{}s:mFOL-sequent()
        (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  {}\mRightarrow{}  mFOL-sequent-evidence(s))


By

---

Latex:
(All  Thin
  THEN  MoveToConcl  (-1)
  THEN  InstLemmaUp  `proof-tree-induction-ext`  [\mkleeneopen{}mFOL-sequent()\mkleeneclose{};\mkleeneopen{}FOLRule()\mkleeneclose{};\mkleeneopen{}\mlambda{}sr.mFOLeffect(sr)\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}pf.\mforall{}s:mFOL-sequent()
                  (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  {}\mRightarrow{}  mFOL-sequent-evidence(s))\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index