---

Step * 1 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
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))))
BY
{ (D 0 With ⌜y⌝  THEN Auto THEN DVar `y' THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

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  \mmember{}  bts)
9.  l  =  let  vs,a  =  y  in  free-vars-aux(rev(vs)  +  bnds;a)
10.  (v  \mmember{}  l)
\mvdash{}  \mexists{}bt:bound-term(opr).  ((bt  \mmember{}  bts)  \mwedge{}  (v  \mmember{}  free-vars-aux(rev(fst(bt))  +  bnds;snd(bt))))


By

---

Latex:
(D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto  THEN  DVar  `y'  THEN  All  Reduce  THEN  Auto)

---

Home Index