---

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


1. [opr] : Type
2. f : opr
3. v : varname()
4. bts : bound-term(opr) List
⊢ ∀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)))))
BY
{ ((Intro THEN RW (AddrC [1] (UnfoldC `free-vars-aux`)) 0)
   THEN Reduce 0
   THEN (RWO "member-l-union-list" 0 THENA Auto)
   THEN (RWO "member-map" 0 THENA Auto)
   THEN (Reduce 0 THEN Auto)
   THEN ExRepD) }

1
1. [opr] : Type
2. f : opr
3. v : varname()
4. bts : bound-term(opr) List
5. bnds : varname() List
6. l : varname() List
7. y : bound-term(opr)
8. (y ∈ bts)
9. l = let vs,a = y in free-vars-aux(rev(vs) + bnds;a) ∈ (varname() List)
10. (v ∈ l)
⊢ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (v ∈ free-vars-aux(rev(fst(bt)) + bnds;snd(bt))))

2
1. [opr] : Type
2. f : opr
3. v : varname()
4. bts : bound-term(opr) List
5. bnds : varname() List
6. bt : bound-term(opr)
7. (bt ∈ bts)
8. (v ∈ free-vars-aux(rev(fst(bt)) + bnds;snd(bt)))
⊢ ∃l:varname() List
   ((∃y:bound-term(opr). ((y ∈ bts) ∧ (l = let vs,a = y in free-vars-aux(rev(vs) + bnds;a) ∈ (varname() List))))
   ∧ (v ∈ l))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  f  :  opr
3.  v  :  varname()
4.  bts  :  bound-term(opr)  List
\mvdash{}  \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)))))


By

---

Latex:
((Intro  THEN  RW  (AddrC  [1]  (UnfoldC  `free-vars-aux`))  0)
  THEN  Reduce  0
  THEN  (RWO  "member-l-union-list"  0  THENA  Auto)
  THEN  (RWO  "member-map"  0  THENA  Auto)
  THEN  (Reduce  0  THEN  Auto)
  THEN  ExRepD)

---

Home Index