---

Step * 7 of Lemma member-free-vars-aux


1. opr : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀v:varname(). ∀bnds:varname() List.
           ((v ∈ free-vars-aux(bnds;snd(bt))) ⇐⇒ (v ∈ free-vars-aux([];snd(bt))) ∧ (¬(v ∈ bnds)))))
4. f : opr
5. v : varname()
6. bnds : varname() List
7. (v ∈ free-vars-aux(bnds;mkterm(f;bts)))
⊢ ¬(v ∈ bnds)
BY
{ (FLemma `member-free-vars-aux-not-bound` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  bts  :  bound-term(opr)  List
3.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)
          {}\mRightarrow{}  (\mforall{}v:varname().  \mforall{}bnds:varname()  List.
                      ((v  \mmember{}  free-vars-aux(bnds;snd(bt)))  \mLeftarrow{}{}\mRightarrow{}  (v  \mmember{}  free-vars-aux([];snd(bt)))  \mwedge{}  (\mneg{}(v  \mmember{}  bnds)))))
4.  f  :  opr
5.  v  :  varname()
6.  bnds  :  varname()  List
7.  (v  \mmember{}  free-vars-aux(bnds;mkterm(f;bts)))
\mvdash{}  \mneg{}(v  \mmember{}  bnds)


By

---

Latex:
(FLemma  `member-free-vars-aux-not-bound`  [-1]  THEN  Auto)

---

Home Index