---

Step * of Lemma member-free-vars-aux-not-bound

No Annotations
∀[opr:Type]. ∀t:term(opr). ∀bnds:varname() List. ∀v:varname().  ((v ∈ free-vars-aux(bnds;t)) ⇒ (¬(v ∈ bnds)))
BY
{ (Intro THEN BLemma `term-induction` THEN Auto) }

1
1. opr : Type
2. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. bnds : varname() List
4. v@0 : varname()
5. (v@0 ∈ free-vars-aux(bnds;varterm(v)))
⊢ ¬(v@0 ∈ bnds)

2
1. opr : Type
2. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. bnds : varname() List
4. v@0 : varname()
⊢ free-vars-aux(bnds;varterm(v)) ∈ varname() List

3
1. opr : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr)
     ((bt ∈ bts) ⇒ (∀bnds:varname() List. ∀v:varname().  ((v ∈ free-vars-aux(bnds;snd(bt))) ⇒ (¬(v ∈ bnds)))))
4. f : opr
5. bnds : varname() List
6. v : varname()
7. (v ∈ free-vars-aux(bnds;mkterm(f;bts)))
⊢ ¬(v ∈ bnds)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}t:term(opr).  \mforall{}bnds:varname()  List.  \mforall{}v:varname().    ((v  \mmember{}  free-vars-aux(bnds;t))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  bnds)))


By

---

Latex:
(Intro  THEN  BLemma  `term-induction`  THEN  Auto)

---

Home Index