---

Step * 3 of Lemma member-free-vars-mkterm

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

1
1. [opr] : Type
2. f : opr
3. v : varname()
4. bts : bound-term(opr) List
5. ∀bnds:varname() List
     ((v ∈ free-vars-aux(bnds;mkterm(f;bts)))
     ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (v ∈ free-vars-aux(rev(fst(bt)) + bnds;snd(bt)))))
6. bt : bound-term(opr)
7. (bt ∈ bts)
8. (v ∈ free-vars-aux([];snd(bt)))
9. ¬(v ∈ fst(bt))
10. (v ∈ free-vars-aux([];snd(bt)))
⊢ ¬(v ∈ rev(fst(bt)) + [])

---

Latex:

---

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


By

---

Latex:
(RWO  "member-free-vars-aux"  0  THEN  Auto)

---

Home Index