---

Step * 1 4 1 of Lemma FOL-proveable-evidence


1. hyps : mFOL() List
2. z : ℤ
3. body : mFOL()
4. x : ℤ
5. FOL-sequent-evidence{i:l}(<hyps, body[z/x]>)
6. (z ∈ mFOL-sequent-freevars(<hyps, ∃x;body)>))
7. [Dom] : Type
8. [S] : FOStruct+{i:l}(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, ∃x;body)>),Dom)
10. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
⊢ (∃v:Dom. Dom,S,a[x := v] +|= FOL-abstract(body)) ⋃ (S "false" [])
BY
{ ((Assert filter(λx@0.(¬b(x@0 =z x));mFOL-freevars(body)) ⊆ mFOL-sequent-freevars(<hyps, ∃x;body)>) BY
          (Unfold `l_contains` 0
           THEN (RWO "l_all_iff" 0 THENA Auto)
           THEN (RWO "member-mFOL-sequent-freevars" 0 THENA Auto)
           THEN Reduce 0
           THEN Auto))
   THEN (UnionOrLeft THENA Auto)
   ) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  filter(\mlambda{}x@0.(\mneg{}\msubb{}(x@0  =\msubz{}  x));mFOL-freevars(body))  \msubseteq{}  mFOL-sequent-freevars(<hyps,  \mexists{}x;body)>)  B\000CY
                (Unfold  `l\_contains`  0
                  THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
                  THEN  (RWO  "member-mFOL-sequent-freevars"  0  THENA  Auto)
                  THEN  Reduce  0
                  THEN  Auto))
  THEN  (UnionOrLeft  THENA  Auto)
  )

---

Home Index