---

Step * 1 4 1 1 1 2 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-freevars(∃x;body))) ∨ (∃h∈hyps. (z ∈ mFOL-freevars(h)))
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)>)
12. mFOL-freevars(body[z/x]) ⊆ mFOL-sequent-freevars(<hyps, ∃x;body)>)
⊢ Dom,S,a[x := a z] +|= FOL-abstract(body)
BY
{ ((InstLemma `FOL-subst-abstract` [⌜Dom⌝;⌜S⌝;⌜body⌝;⌜z⌝;⌜x⌝;⌜a⌝]⋅ THENA Auto)
   THEN ((Assert Dom,S,a +|= FOL-sequent-abstract(<hyps, body[z/x]>) BY
                ((With ⌜Dom⌝ (D 5)⋅ THENA Auto) THEN BackThruSomeHyp))
         THEN RepUR ``FOL-sequent-abstract FOSatWith+`` (-1)
         THEN Fold `FOSatWith+` (-1)
         THEN D (-1)
         THEN Auto)⋅
   ) }

---

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-freevars(\mexists{}x;body)))  \mvee{}  (\mexists{}h\mmember{}hyps.  (z  \mmember{}  mFOL-freevars(h)))
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))
11.  filter(\mlambda{}x@0.(\mneg{}\msubb{}(x@0  =\msubz{}  x));mFOL-freevars(body))  \msubseteq{}  mFOL-sequent-freevars(<hyps,  \mexists{}x;body)>)
12.  mFOL-freevars(body[z/x])  \msubseteq{}  mFOL-sequent-freevars(<hyps,  \mexists{}x;body)>)
\mvdash{}  Dom,S,a[x  :=  a  z]  +|=  FOL-abstract(body)


By

---

Latex:
((InstLemma  `FOL-subst-abstract`  [\mkleeneopen{}Dom\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}body\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((Assert  Dom,S,a  +|=  FOL-sequent-abstract(<hyps,  body[z/x]>)  BY
                            ((With  \mkleeneopen{}Dom\mkleeneclose{}  (D  5)\mcdot{}  THENA  Auto)  THEN  BackThruSomeHyp))
              THEN  RepUR  ``FOL-sequent-abstract  FOSatWith+``  (-1)
              THEN  Fold  `FOSatWith+`  (-1)
              THEN  D  (-1)
              THEN  Auto)\mcdot{}
  )

---

Home Index