---

Step * 1 3 1 2 2 1 of Lemma FOL-sequent-evidence-false-hyp


1. hyps : mFOL() List
2. concl : mFOL()
3. i : ℕ||hyps||
4. ↑mFOatomic?(hyps[i])
5. mFOatomic-name(hyps[i]) = "false" ∈ Atom
6. mFOatomic-vars(hyps[i]) = [] ∈ (ℤ List)
7. Dom : Type
8. S : FOStruct+{i:l}(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
10. x : tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
11. x.i = x.i ∈ FOL-hyps-meaning(Dom;S;a;hyps)[i]
12. hyps[i] = false ∈ mFOL()
13. z : mFOL()
14. z = false ∈ mFOL()
15. a = a ∈ FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
⊢ mFOL-freevars(z) ⊆ mFOL-sequent-freevars(<hyps, concl>)
BY
{ Subst' mFOL-freevars(z) ~ [] 0 }

1
.....equality..... 
1. hyps : mFOL() List
2. concl : mFOL()
3. i : ℕ||hyps||
4. ↑mFOatomic?(hyps[i])
5. mFOatomic-name(hyps[i]) = "false" ∈ Atom
6. mFOatomic-vars(hyps[i]) = [] ∈ (ℤ List)
7. Dom : Type
8. S : FOStruct+{i:l}(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
10. x : tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
11. x.i = x.i ∈ FOL-hyps-meaning(Dom;S;a;hyps)[i]
12. hyps[i] = false ∈ mFOL()
13. z : mFOL()
14. z = false ∈ mFOL()
15. a = a ∈ FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
⊢ mFOL-freevars(z) ~ []

2
1. hyps : mFOL() List
2. concl : mFOL()
3. i : ℕ||hyps||
4. ↑mFOatomic?(hyps[i])
5. mFOatomic-name(hyps[i]) = "false" ∈ Atom
6. mFOatomic-vars(hyps[i]) = [] ∈ (ℤ List)
7. Dom : Type
8. S : FOStruct+{i:l}(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
10. x : tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
11. x.i = x.i ∈ FOL-hyps-meaning(Dom;S;a;hyps)[i]
12. hyps[i] = false ∈ mFOL()
13. z : mFOL()
14. z = false ∈ mFOL()
15. a = a ∈ FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
⊢ [] ⊆ mFOL-sequent-freevars(<hyps, concl>)

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  i  :  \mBbbN{}||hyps||
4.  \muparrow{}mFOatomic?(hyps[i])
5.  mFOatomic-name(hyps[i])  =  "false"
6.  mFOatomic-vars(hyps[i])  =  []
7.  Dom  :  Type
8.  S  :  FOStruct+\{i:l\}(Dom)
9.  a  :  FOAssignment(mFOL-sequent-freevars(<hyps,  concl>),Dom)
10.  x  :  tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
11.  x.i  =  x.i
12.  hyps[i]  =  false
13.  z  :  mFOL()
14.  z  =  false
15.  a  =  a
\mvdash{}  mFOL-freevars(z)  \msubseteq{}  mFOL-sequent-freevars(<hyps,  concl>)


By

---

Latex:
Subst'  mFOL-freevars(z)  \msim{}  []  0

---

Home Index