---

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


1. hyps : mFOL() List@i
2. z : ℤ@i
3. body : mFOL()@i
4. x : ℤ@i
5. mFOL-sequent-evidence(<hyps, body[z/x]>)@i'
6. [Dom] : Type
7. [S] : FOStruct(Dom)
8. a : FOAssignment(Dom)@i
9. tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps))@i
10. Dom,S,a |= mFOL-abstract(body[z/x]) = Dom,S,a[x := a z] |= mFOL-abstract(body) ∈ ℙ
⊢ Dom,S,a[x := a z] |= mFOL-abstract(body)
BY
{ ((Assert Dom,S,a |= mFOL-sequent-abstract(<hyps, body[z/x]>) BY
          ((With ⌈Dom⌉ (D 5)⋅ THENA Auto) THEN BackThruSomeHyp))
   THEN RepUR ``mFOL-sequent-abstract FOSatWith`` (-1)
   THEN Fold `FOSatWith` (-1)
   THEN D (-1)
   THEN Auto)⋅ }

---

Latex:



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


By

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

---

Home Index