---

Step * 1 of Lemma FOL-sequent-evidence_and


1. hyps : mFOL() List@i
2. [x] : mFOL()
3. [y] : mFOL()
4. FOL-sequent-evidence{i:l}(<hyps, x>)@i'
5. FOL-sequent-evidence{i:l}(<hyps, y>)@i'
6. [Dom] : Type
7. [S] : FOStruct+{i:l}(Dom)
8. a : FOAssignment(mFOL-sequent-freevars(<hyps, x ∧ y>),Dom)@i
9. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))@i
10. Dom,S,a +|= FOL-abstract(y)
11. Dom,S,a +|= FOL-abstract(x)
⊢ (Dom,S,a +|= FOL-abstract(x) ∧ Dom,S,a +|= FOL-abstract(y)) ⋃ (S "false" [])
BY
{ (Assert a ∈ FOAssignment(mFOL-freevars(x ∧ y),Dom) BY
         ((DoSubsume THEN Auto) THEN SubtypeReasoning1 THEN Auto)) }

1
1. hyps : mFOL() List@i
2. [x] : mFOL()
3. [y] : mFOL()
4. FOL-sequent-evidence{i:l}(<hyps, x>)@i'
5. FOL-sequent-evidence{i:l}(<hyps, y>)@i'
6. [Dom] : Type
7. [S] : FOStruct+{i:l}(Dom)
8. a : FOAssignment(mFOL-sequent-freevars(<hyps, x ∧ y>),Dom)@i
9. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))@i
10. Dom,S,a +|= FOL-abstract(y)
11. Dom,S,a +|= FOL-abstract(x)
12. a ∈ FOAssignment(mFOL-freevars(x ∧ y),Dom)
⊢ (Dom,S,a +|= FOL-abstract(x) ∧ Dom,S,a +|= FOL-abstract(y)) ⋃ (S "false" [])

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List@i
2.  [x]  :  mFOL()
3.  [y]  :  mFOL()
4.  FOL-sequent-evidence\{i:l\}(<hyps,  x>)@i'
5.  FOL-sequent-evidence\{i:l\}(<hyps,  y>)@i'
6.  [Dom]  :  Type
7.  [S]  :  FOStruct+\{i:l\}(Dom)
8.  a  :  FOAssignment(mFOL-sequent-freevars(<hyps,  x  \mwedge{}  y>),Dom)@i
9.  tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))@i
10.  Dom,S,a  +|=  FOL-abstract(y)
11.  Dom,S,a  +|=  FOL-abstract(x)
\mvdash{}  (Dom,S,a  +|=  FOL-abstract(x)  \mwedge{}  Dom,S,a  +|=  FOL-abstract(y))  \mcup{}  (S  "false"  [])


By

---

Latex:
(Assert  a  \mmember{}  FOAssignment(mFOL-freevars(x  \mwedge{}  y),Dom)  BY
              ((DoSubsume  THEN  Auto)  THEN  SubtypeReasoning1  THEN  Auto))

---

Home Index