---

Step * 6 1 of Lemma member-free-vars-aux


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 ∈ l-union-list(VarDeq;map(λbt.let vs,a = bt 
                                    in free-vars-aux(rev(vs) + bnds;a);bts)))
⊢ (v ∈ l-union-list(VarDeq;map(λbt.let vs,a = bt 
                                   in free-vars-aux(rev(vs) + [];a);bts)))
BY
{ ((RWO "member-l-union-list" (-1) THENA Auto)
   THEN (RWO "member-l-union-list" 0 THENA Auto)
   THEN (RWO "member-map" (-1) THENA Auto)
   THEN (RWO "member-map" 0 THENA Auto)
   THEN Reduce -1
   THEN Reduce 0
   THEN ExRepD) }

1
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. l : varname() List
8. y : bound-term(opr)
9. (y ∈ bts)
10. l = let vs,a = y in free-vars-aux(rev(vs) + bnds;a) ∈ (varname() List)
11. (v ∈ l)
⊢ ∃l:varname() List
   ((∃y:bound-term(opr). ((y ∈ bts) ∧ (l = let vs,a = y in free-vars-aux(rev(vs) + [];a) ∈ (varname() List))))
   ∧ (v ∈ l))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  bts  :  bound-term(opr)  List
3.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)
          {}\mRightarrow{}  (\mforall{}v:varname().  \mforall{}bnds:varname()  List.
                      ((v  \mmember{}  free-vars-aux(bnds;snd(bt)))  \mLeftarrow{}{}\mRightarrow{}  (v  \mmember{}  free-vars-aux([];snd(bt)))  \mwedge{}  (\mneg{}(v  \mmember{}  bnds)))))
4.  f  :  opr
5.  v  :  varname()
6.  bnds  :  varname()  List
7.  (v  \mmember{}  l-union-list(VarDeq;map(\mlambda{}bt.let  vs,a  =  bt 
                                                                        in  free-vars-aux(rev(vs)  +  bnds;a);bts)))
\mvdash{}  (v  \mmember{}  l-union-list(VarDeq;map(\mlambda{}bt.let  vs,a  =  bt 
                                                                      in  free-vars-aux(rev(vs)  +  [];a);bts)))


By

---

Latex:
((RWO  "member-l-union-list"  (-1)  THENA  Auto)
  THEN  (RWO  "member-l-union-list"  0  THENA  Auto)
  THEN  (RWO  "member-map"  (-1)  THENA  Auto)
  THEN  (RWO  "member-map"  0  THENA  Auto)
  THEN  Reduce  -1
  THEN  Reduce  0
  THEN  ExRepD)

---

Home Index