---

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


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

1
1. v : mFOL()
⊢ (↑mFOatomic?(v))
⇒ (mFOatomic-name(v) = "false" ∈ Atom)
⇒ (mFOatomic-vars(v) = [] ∈ (ℤ List))
⇒ (v = false ∈ mFOL())

---

Latex:

---

Latex:

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


By

---

Latex:
All  Thin

---

Home Index