---

Step * 1 11 1 1 of Lemma FOL-proveable-evidence

.....assertion..... 
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. var : ℤ
6. hypnum < ||hyps||
7. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. FOL-sequent-evidence{i:l}(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
11. hyps[hypnum] = ∀mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum])) ∈ mFOL()
⊢ mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
BY
{ (Unfold `l_contains` 0
   THEN (RWO  "l_all_iff" 0 THENA Auto)
   THEN RWO "freevars-FOL-subst" 0
   THEN Auto
   THEN D -1
   THEN Auto) }

1
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. var : ℤ
6. hypnum < ||hyps||
7. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. FOL-sequent-evidence{i:l}(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
11. hyps[hypnum] = ∀mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum])) ∈ mFOL()
12. a : ℤ
13. ¬(a = mFOquant-var(hyps[hypnum]) ∈ ℤ)
14. (a ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
⊢ (a ∈ mFOL-sequent-freevars(<hyps, concl>))

---

Latex:

---

Latex:
.....assertion..... 
1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  subgoals  :  mFOL-sequent()  List
4.  hypnum  :  \mBbbN{}
5.  var  :  \mBbbZ{}
6.  hypnum  <  ||hyps||
7.  (var  \mmember{}  mFOL-sequent-freevars(<hyps,  concl>))
8.  \muparrow{}mFOquant?(hyps[hypnum])
9.  mFOquant-isall(hyps[hypnum])  =  tt
10.  FOL-sequent-evidence\{i:l\}(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]  /  hyps]
                                                            ,  concl
                                                            >)
11.  hyps[hypnum]  =  \mforall{}mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum]))
\mvdash{}  mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
    \msubseteq{}  mFOL-sequent-freevars(<hyps,  concl>)


By

---

Latex:
(Unfold  `l\_contains`  0
  THEN  (RWO    "l\_all\_iff"  0  THENA  Auto)
  THEN  RWO  "freevars-FOL-subst"  0
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index