---

Step * 1 3 1 1 1 1 1 1 2 1 2 1 1 2 1 of Lemma FOL-proveable-evidence

.....subterm..... T:t
2:n
1. z : ℤ
2. body : mFOL()
3. x : ℤ
4. Dom : Type
5. S : FOStruct+{i:l}(Dom)
6. v : Dom
7. u : mFOL()
8. v1 : mFOL() List
9. ∀a:FOAssignment(mFOL-sequent-freevars(<v1, ∀x;body)>),Dom)
     ((∀h∈v1.¬(z ∈ mFOL-freevars(h)))
     ⇒ (tuple-type(FOL-hyps-meaning(Dom;S;a[z := v];v1)) = tuple-type(FOL-hyps-meaning(Dom;S;a;v1)) ∈ ℙ))
10. a : FOAssignment(mFOL-sequent-freevars(<[u / v1], ∀x;body)>),Dom)
11. (∀h∈[u / v1].¬(z ∈ mFOL-freevars(h)))
12. Dom,S,a[z := v] +|= FOL-abstract(u) = Dom,S,a +|= FOL-abstract(u) ∈ ℙ
⊢ tuple-type(FOL-hyps-meaning(Dom;S;a[z := v];v1)) = tuple-type(FOL-hyps-meaning(Dom;S;a;v1)) ∈ Type
BY
{ (BHyp -4 THEN Auto) }

1
1. z : ℤ
2. body : mFOL()
3. x : ℤ
4. Dom : Type
5. S : FOStruct+{i:l}(Dom)
6. v : Dom
7. u : mFOL()
8. v1 : mFOL() List
9. ∀a:FOAssignment(mFOL-sequent-freevars(<v1, ∀x;body)>),Dom)
     ((∀h∈v1.¬(z ∈ mFOL-freevars(h)))
     ⇒ (tuple-type(FOL-hyps-meaning(Dom;S;a[z := v];v1)) = tuple-type(FOL-hyps-meaning(Dom;S;a;v1)) ∈ ℙ))
10. a : FOAssignment(mFOL-sequent-freevars(<[u / v1], ∀x;body)>),Dom)
11. (∀h∈[u / v1].¬(z ∈ mFOL-freevars(h)))
12. Dom,S,a[z := v] +|= FOL-abstract(u) = Dom,S,a +|= FOL-abstract(u) ∈ ℙ
13. a = a ∈ FOAssignment(mFOL-sequent-freevars(<[u / v1], ∀x;body)>),Dom)
14. h : mFOL()
15. (h ∈ v1)
⊢ mFOL-freevars(h) ⊆ mFOL-sequent-freevars(<[u / v1], ∀x;body)>)

2
1. z : ℤ
2. body : mFOL()
3. x : ℤ
4. Dom : Type
5. S : FOStruct+{i:l}(Dom)
6. v : Dom
7. u : mFOL()
8. v1 : mFOL() List
9. ∀a:FOAssignment(mFOL-sequent-freevars(<v1, ∀x;body)>),Dom)
     ((∀h∈v1.¬(z ∈ mFOL-freevars(h)))
     ⇒ (tuple-type(FOL-hyps-meaning(Dom;S;a[z := v];v1)) = tuple-type(FOL-hyps-meaning(Dom;S;a;v1)) ∈ ℙ))
10. a : FOAssignment(mFOL-sequent-freevars(<[u / v1], ∀x;body)>),Dom)
11. (∀h∈[u / v1].¬(z ∈ mFOL-freevars(h)))
12. Dom,S,a[z := v] +|= FOL-abstract(u) = Dom,S,a +|= FOL-abstract(u) ∈ ℙ
⊢ (∀h∈v1.¬(z ∈ mFOL-freevars(h)))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  z  :  \mBbbZ{}
2.  body  :  mFOL()
3.  x  :  \mBbbZ{}
4.  Dom  :  Type
5.  S  :  FOStruct+\{i:l\}(Dom)
6.  v  :  Dom
7.  u  :  mFOL()
8.  v1  :  mFOL()  List
9.  \mforall{}a:FOAssignment(mFOL-sequent-freevars(<v1,  \mforall{}x;body)>),Dom)
          ((\mforall{}h\mmember{}v1.\mneg{}(z  \mmember{}  mFOL-freevars(h)))
          {}\mRightarrow{}  (tuple-type(FOL-hyps-meaning(Dom;S;a[z  :=  v];v1))
                =  tuple-type(FOL-hyps-meaning(Dom;S;a;v1))))
10.  a  :  FOAssignment(mFOL-sequent-freevars(<[u  /  v1],  \mforall{}x;body)>),Dom)
11.  (\mforall{}h\mmember{}[u  /  v1].\mneg{}(z  \mmember{}  mFOL-freevars(h)))
12.  Dom,S,a[z  :=  v]  +|=  FOL-abstract(u)  =  Dom,S,a  +|=  FOL-abstract(u)
\mvdash{}  tuple-type(FOL-hyps-meaning(Dom;S;a[z  :=  v];v1))  =  tuple-type(FOL-hyps-meaning(Dom;S;a;v1))


By

---

Latex:
(BHyp  -4  THEN  Auto)

---

Home Index