---

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


1. hyps : mFOL() List@i
2. z : ℤ@i
3. (∀h∈hyps.¬(z ∈ mFOL-freevars(h)))
4. body : mFOL()@i
5. x : ℤ@i
6. mFOL-sequent-evidence(<hyps, body[z/x]>)@i'
7. ¬(z ∈ mFOL-freevars(∀x;body)))@i
8. Dom : Type
9. S : FOStruct(Dom)
10. a : FOAssignment(Dom)@i
11. tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps))@i
12. v : Dom@i
13. Dom,S,a[z := v] |= mFOL-abstract(body[z/x]) = Dom,S,a[z := v][x := v] |= mFOL-abstract(body) ∈ ℙ
14. z@0 : ℤ@i
15. (z@0 ∈ mFOL-freevars(body))@i
⊢ (a[z := v][x := v] z@0) = (a[x := v] z@0) ∈ Dom
BY
{ (RepUR ``update-assignment`` 0
   THEN RepeatFor 2 (AutoSplit
                     ⋅)
   THEN Auto
   THEN D 7
   THEN RepUR ``mFOL-freevars`` 0
   THEN Fold `mFOL-freevars` 0
   THEN RWO  "member_filter" 0
   THEN Auto
   THEN Reduce 0
   THEN RW assert_pushdownC 0
   THEN Auto)⋅ }

---

Latex:



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


By

(RepUR  ``update-assignment``  0
  THEN  RepeatFor  2  (AutoSplit
                                      \mcdot{})
  THEN  Auto
  THEN  D  7
  THEN  RepUR  ``mFOL-freevars``  0
  THEN  Fold  `mFOL-freevars`  0
  THEN  RWO    "member\_filter"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)\mcdot{}

---

Home Index