---

Step * 1 6 1 of Lemma FOL-proveable-evidence


1. hyps : mFOL() List
2. concl : mFOL()
3. left : 𝔹
4. ¬↑left
5. ↑mFOconnect?(concl)
6. mFOconnect-knd(concl) = "or" ∈ Atom
7. FOL-sequent-evidence{i:l}(<hyps, mFOconnect-right(concl)>)
8. [Dom] : Type
9. [S] : FOStruct+{i:l}(Dom)
10. a : FOAssignment(mFOL-freevars(mFOconnect-left(concl) ∨ mFOconnect-right(concl)),Dom)
11. Dom,S,a +|= FOL-abstract(mFOconnect-right(concl))
⊢ (Dom,S,a +|= FOL-abstract(mFOconnect-left(concl)) ∨ Dom,S,a +|= FOL-abstract(mFOconnect-right(concl))) ⋃ (S "false" 
                                                                                                            [])
BY
{ (UnionOrLeft THEN Auto) }

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  left  :  \mBbbB{}
4.  \mneg{}\muparrow{}left
5.  \muparrow{}mFOconnect?(concl)
6.  mFOconnect-knd(concl)  =  "or"
7.  FOL-sequent-evidence\{i:l\}(<hyps,  mFOconnect-right(concl)>)
8.  [Dom]  :  Type
9.  [S]  :  FOStruct+\{i:l\}(Dom)
10.  a  :  FOAssignment(mFOL-freevars(mFOconnect-left(concl)  \mvee{}  mFOconnect-right(concl)),Dom)
11.  Dom,S,a  +|=  FOL-abstract(mFOconnect-right(concl))
\mvdash{}  (Dom,S,a  +|=  FOL-abstract(mFOconnect-left(concl))
\mvee{}  Dom,S,a  +|=  FOL-abstract(mFOconnect-right(concl)))  \mcup{}  (S  "false"  [])


By

---

Latex:
(UnionOrLeft  THEN  Auto)

---

Home Index