---

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


1. hyps : mFOL() List
2. concl : mFOL()
3. hypnum : ℕ
4. hypnum < ||hyps||
5. ↑mFOconnect?(hyps[hypnum])
6. mFOconnect-knd(hyps[hypnum]) = "and" ∈ Atom
7. mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>)
8. hyps[hypnum] = mFOconnect-left(hyps[hypnum]) ∧ mFOconnect-right(hyps[hypnum]) ∈ mFOL()
9. mFOL-freevars(mFOconnect-left(hyps[hypnum])) ⊆ mFOL-freevars(hyps[hypnum])
⊢ mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum]) / hyps], hyps[hypnum]>)
BY
{ ((InstLemma `mFOL-sequent-evidence-trivial` [⌜[mFOconnect-right(hyps[hypnum]) / hyps]⌝;⌜hypnum + 1⌝]⋅ THENA Auto')
   THEN (RWO "select-cons" (-1) THENA Auto)
   THEN SplitOnHypITE -1 
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  hypnum  :  \mBbbN{}
4.  hypnum  <  ||hyps||
5.  \muparrow{}mFOconnect?(hyps[hypnum])
6.  mFOconnect-knd(hyps[hypnum])  =  "and"
7.  mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]);  [mFOconnect-right(hyps[hypnum])  /  hyps]]
                                                  ,  concl
                                                  >)
8.  hyps[hypnum]  =  mFOconnect-left(hyps[hypnum])  \mwedge{}  mFOconnect-right(hyps[hypnum])
9.  mFOL-freevars(mFOconnect-left(hyps[hypnum]))  \msubseteq{}  mFOL-freevars(hyps[hypnum])
\mvdash{}  mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum])  /  hyps],  hyps[hypnum]>)


By

---

Latex:
((InstLemma  `mFOL-sequent-evidence-trivial`  [\mkleeneopen{}[mFOconnect-right(hyps[hypnum])  /  hyps]\mkleeneclose{};\mkleeneopen{}hypnum  +  1\mkleeneclose{}]
    \mcdot{}
    THENA  Auto'
    )
  THEN  (RWO  "select-cons"  (-1)  THENA  Auto)
  THEN  SplitOnHypITE  -1 
  THEN  Auto)\mcdot{}

---

Home Index