---

Step * of Lemma member-free-vars-aux

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

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

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

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

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

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

6
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 ∈ free-vars-aux([];mkterm(f;bts)))

7
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)

8
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([];mkterm(f;bts)))
8. ¬(v ∈ bnds)
⊢ (v ∈ free-vars-aux(bnds;mkterm(f;bts)))

---

Latex:

---

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


By

---

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

---

Home Index