---

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


1. hyps : mFOL() List@i
2. var : ℤ@i
3. (∀h∈hyps.¬(var ∈ mFOL-freevars(h)))
4. body : mFOL()@i
5. x : ℤ@i
6. mFOL-sequent-evidence(<hyps, body[var/x]>)@i'
7. ¬(var ∈ mFOL-freevars(∀x;body)))@i
⊢ mFOL-sequent-evidence(<hyps, ∀x;body)>)
BY
{ ((D 0 THEN Auto)
   THEN Unfold `mFOL-sequent-abstract` 0
   THEN RepUR ``FOSatWith`` 0
   THEN RW (AddrC [2] (UnfoldC `mFOL-abstract`)) 0
   THEN Reduce 0
   THEN Fold `mFOL-abstract` 0
   THEN RepUR ``FOQuantifier`` 0
   THEN Fold `FOSatWith` 0
   THEN Auto
   THEN RenameVar `z' 2
   THEN (InstLemma `mFOL-subst-abstract` [⌈Dom⌉;⌈S⌉;⌈a[z := v]⌉;⌈body⌉;⌈z⌉;⌈x⌉]⋅ THENA Auto)
   THEN Subst ⌈a[z := v] z ~ v⌉ (-1)⋅
   THEN Try (Complete ((RepUR ``update-assignment`` 0 THEN AutoSplit ⋅ THEN Auto)))) }

1
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) ∈ ℙ
⊢ Dom,S,a[x := v] |= mFOL-abstract(body)

---

Latex:



1.  hyps  :  mFOL()  List@i
2.  var  :  \mBbbZ{}@i
3.  (\mforall{}h\mmember{}hyps.\mneg{}(var  \mmember{}  mFOL-freevars(h)))
4.  body  :  mFOL()@i
5.  x  :  \mBbbZ{}@i
6.  mFOL-sequent-evidence(<hyps,  body[var/x]>)@i'
7.  \mneg{}(var  \mmember{}  mFOL-freevars(\mforall{}x;body)))@i
\mvdash{}  mFOL-sequent-evidence(<hyps,  \mforall{}x;body)>)


By

((D  0  THEN  Auto)
  THEN  Unfold  `mFOL-sequent-abstract`  0
  THEN  RepUR  ``FOSatWith``  0
  THEN  RW  (AddrC  [2]  (UnfoldC  `mFOL-abstract`))  0
  THEN  Reduce  0
  THEN  Fold  `mFOL-abstract`  0
  THEN  RepUR  ``FOQuantifier``  0
  THEN  Fold  `FOSatWith`  0
  THEN  Auto
  THEN  RenameVar  `z'  2
  THEN  (InstLemma  `mFOL-subst-abstract`  [\mkleeneopen{}Dom\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}a[z  :=  v]\mkleeneclose{};\mkleeneopen{}body\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Subst  \mkleeneopen{}a[z  :=  v]  z  \msim{}  v\mkleeneclose{}  (-1)\mcdot{}
  THEN  Try  (Complete  ((RepUR  ``update-assignment``  0  THEN  AutoSplit  \mcdot{}  THEN  Auto))))

---

Home Index