---

Step * 1 2 1 1 1 4 1 1 of Lemma mFOL-proveable-evidence


1. hyps : mFOL() List
2. z : ℤ
3. body : mFOL()
4. x : ℤ
5. mFOL-sequent-evidence(<hyps, body[z/x]>)
6. (z ∈ mFOL-sequent-freevars(<hyps, ∃x;body)>))
7. [Dom] : Type
8. [S] : FOStruct(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, ∃x;body)>),Dom)
10. tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))
⊢ ∃v:Dom. Dom,S,a[x := v] |= mFOL-abstract(body)
BY
{ ((With ⌜a z⌝ (D 0)⋅ THENA Auto) THEN ((RWO "member-mFOL-sequent-freevars" 6 THENM Reduce 6) THENA Auto)) }

1
1. hyps : mFOL() List
2. z : ℤ
3. body : mFOL()
4. x : ℤ
5. mFOL-sequent-evidence(<hyps, body[z/x]>)
6. (z ∈ mFOL-freevars(∃x;body))) ∨ (∃h∈hyps. (z ∈ mFOL-freevars(h)))
7. [Dom] : Type
8. [S] : FOStruct(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, ∃x;body)>),Dom)
10. tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))
⊢ Dom,S,a[x := a z] |= mFOL-abstract(body)

2
1. hyps : mFOL() List
2. z : ℤ
3. body : mFOL()
4. x : ℤ
5. mFOL-sequent-evidence(<hyps, body[z/x]>)
6. (z ∈ mFOL-freevars(∃x;body))) ∨ (∃h∈hyps. (z ∈ mFOL-freevars(h)))
7. Dom : Type
8. S : FOStruct(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, ∃x;body)>),Dom)
10. tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))
11. v : Dom
12. a = a ∈ FOAssignment(mFOL-sequent-freevars(<hyps, ∃x;body)>),Dom)
⊢ filter(λx@0.(¬b(x@0 =z x));mFOL-freevars(body)) ⊆ mFOL-sequent-freevars(<hyps, ∃x;body)>)

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  z  :  \mBbbZ{}
3.  body  :  mFOL()
4.  x  :  \mBbbZ{}
5.  mFOL-sequent-evidence(<hyps,  body[z/x]>)
6.  (z  \mmember{}  mFOL-sequent-freevars(<hyps,  \mexists{}x;body)>))
7.  [Dom]  :  Type
8.  [S]  :  FOStruct(Dom)
9.  a  :  FOAssignment(mFOL-sequent-freevars(<hyps,  \mexists{}x;body)>),Dom)
10.  tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))
\mvdash{}  \mexists{}v:Dom.  Dom,S,a[x  :=  v]  |=  mFOL-abstract(body)


By

---

Latex:
((With  \mkleeneopen{}a  z\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  ((RWO  "member-mFOL-sequent-freevars"  6  THENM  Reduce  6)  THENA  Auto)
  )

---

Home Index