---

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


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)
BY
{ (Thin 5
   THEN D 1
   THEN RenameVar `hyps' 1
   THEN RenameVar `concl' 2
   THEN RenameVar `rule' 3
   THEN RenameVar `subgoals' 4
   THEN RenameVar `subproofs' 6
   THEN (Assert ⌜∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])⌝⋅
         THENA (ParallelLast THEN (D -4 With ⌜i⌝  THENA Auto) THEN BHyp -1 THEN Auto)
         )
   THEN ThinVar `subproofs') }

1
1. hyps : mFOL() List
2. concl : mFOL()
3. rule : FOLRule()
4. subgoals : mFOL-sequent() List
5. mFOLeffect(<<hyps, concl>, rule>) = (inl subgoals) ∈ (mFOL-sequent() List?)
6. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
⊢ mFOL-sequent-evidence(<hyps, concl>)

---

Latex:

---

Latex:

1.  s  :  mFOL-sequent()
2.  r  :  FOLRule()
3.  x  :  mFOL-sequent()  List
4.  mFOLeffect(<s,  r>)  =  (inl  x)
5.  True
6.  L  :  proof-tree(mFOL-sequent();FOLRule();\mlambda{}sr.mFOLeffect(sr))  List
7.  ||L||  =  ||x||
8.  (\mforall{}pf\mmember{}L.\mforall{}s:mFOL-sequent()
                        (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  {}\mRightarrow{}  mFOL-sequent-evidence(s)))
9.  \mforall{}i:\mBbbN{}||x||.  correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);x[i];L[i])
\mvdash{}  mFOL-sequent-evidence(s)


By

---

Latex:
(Thin  5
  THEN  D  1
  THEN  RenameVar  `hyps'  1
  THEN  RenameVar  `concl'  2
  THEN  RenameVar  `rule'  3
  THEN  RenameVar  `subgoals'  4
  THEN  RenameVar  `subproofs'  6
  THEN  (Assert  \mkleeneopen{}\mforall{}i:\mBbbN{}||subgoals||.  mFOL-sequent-evidence(subgoals[i])\mkleeneclose{}\mcdot{}
              THENA  (ParallelLast  THEN  (D  -4  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)  THEN  BHyp  -1  THEN  Auto)
              )
  THEN  ThinVar  `subproofs')

---

Home Index