---

Step * 2 1 of Lemma member-free-vars-mkterm


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 ∈ rev(fst(bt)) + [])
10. (v ∈ free-vars-aux([];snd(bt)))
⊢ ¬(v ∈ fst(bt))
BY
{ (ParallelOp -2 THEN GenListD 0 THEN Auto) }

---

Latex:

---

Latex:

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)))
9.  \mneg{}(v  \mmember{}  rev(fst(bt))  +  [])
10.  (v  \mmember{}  free-vars-aux([];snd(bt)))
\mvdash{}  \mneg{}(v  \mmember{}  fst(bt))


By

---

Latex:
(ParallelOp  -2  THEN  GenListD  0  THEN  Auto)

---

Home Index