---

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


1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. hypnum : ℕ@i
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>)
⊢ 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:



1.  hyps  :  mFOL()  List@i
2.  concl  :  mFOL()@i
3.  hypnum  :  \mBbbN{}@i
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
                                                  >)
\mvdash{}  mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum])  /  hyps],  hyps[hypnum]>)


By

((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