---

Step * 3 1 of Lemma member-free-vars-aux-not-bound


1. opr : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr)
     ((bt ∈ bts) ⇒ (∀bnds:varname() List. ∀v:varname().  ((v ∈ free-vars-aux(bnds;snd(bt))) ⇒ (¬(v ∈ bnds)))))
4. f : opr
5. bnds : varname() List
6. v : varname()
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)
⊢ ¬(v ∈ bnds)
BY
{ ((DVar `y' THEN All Reduce)
   THEN InstHyp [⌜<y1, y2>⌝;⌜rev(y1) + bnds⌝;⌜v⌝] 3⋅
   THEN Auto
   THEN ParallelLast
   THEN RWO "member-rev-append" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  bts  :  bound-term(opr)  List
3.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)
          {}\mRightarrow{}  (\mforall{}bnds:varname()  List.  \mforall{}v:varname().    ((v  \mmember{}  free-vars-aux(bnds;snd(bt)))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  bnds)))))
4.  f  :  opr
5.  bnds  :  varname()  List
6.  v  :  varname()
7.  l  :  varname()  List
8.  y  :  bound-term(opr)
9.  (y  \mmember{}  bts)
10.  l  =  let  vs,a  =  y  in  free-vars-aux(rev(vs)  +  bnds;a)
11.  (v  \mmember{}  l)
\mvdash{}  \mneg{}(v  \mmember{}  bnds)


By

---

Latex:
((DVar  `y'  THEN  All  Reduce)
  THEN  InstHyp  [\mkleeneopen{}<y1,  y2>\mkleeneclose{};\mkleeneopen{}rev(y1)  +  bnds\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]  3\mcdot{}
  THEN  Auto
  THEN  ParallelLast
  THEN  RWO  "member-rev-append"  0
  THEN  Auto)

---

Home Index