---

Step * 1 1 of Lemma mFOL-sequent-evidence-trivial


1. hyps : mFOL() List@i
2. i : ℤ@i
3. 0 ≤ i
4. i < ||hyps||
5. Dom : Type
6. S : FOStruct(Dom)
7. a : FOAssignment(mFOL-sequent-freevars(<hyps, hyps[i]>),Dom)@i
8. x : tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))@i
⊢ x.i ∈ Dom,S,a |= mFOL-abstract(hyps[i])
BY
{ DoSubsume⋅ }

1
1. hyps : mFOL() List@i
2. i : ℤ@i
3. 0 ≤ i
4. i < ||hyps||
5. Dom : Type
6. S : FOStruct(Dom)
7. a : FOAssignment(mFOL-sequent-freevars(<hyps, hyps[i]>),Dom)@i
8. x : tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))@i
⊢ x.i ∈ mFOL-hyps-meaning(Dom;S;a;hyps)[i]

2
1. hyps : mFOL() List@i
2. i : ℤ@i
3. 0 ≤ i
4. i < ||hyps||
5. Dom : Type
6. S : FOStruct(Dom)
7. a : FOAssignment(mFOL-sequent-freevars(<hyps, hyps[i]>),Dom)@i
8. x : tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))@i
9. x.i = x.i ∈ mFOL-hyps-meaning(Dom;S;a;hyps)[i]
⊢ mFOL-hyps-meaning(Dom;S;a;hyps)[i] ⊆r Dom,S,a |= mFOL-abstract(hyps[i])

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List@i
2.  i  :  \mBbbZ{}@i
3.  0  \mleq{}  i
4.  i  <  ||hyps||
5.  Dom  :  Type
6.  S  :  FOStruct(Dom)
7.  a  :  FOAssignment(mFOL-sequent-freevars(<hyps,  hyps[i]>),Dom)@i
8.  x  :  tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))@i
\mvdash{}  x.i  \mmember{}  Dom,S,a  |=  mFOL-abstract(hyps[i])


By

---

Latex:
DoSubsume\mcdot{}

---

Home Index