---

Step * 8 1 1 1 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. l : varname() List
8. y1 : varname() List
9. y2 : term(opr)
10. (<y1, y2> ∈ bts)
11. l = free-vars-aux(rev(y1) + [];y2) ∈ (varname() List)
12. (v ∈ l)
13. ¬(v ∈ bnds)
14. ∃y@0:bound-term(opr)
     ((y@0 ∈ bts)
     ∧ (free-vars-aux(rev(y1) + bnds;y2) = let vs,a = y@0 in free-vars-aux(rev(vs) + bnds;a) ∈ (varname() List)))
15. ∀v:varname(). ∀bnds:varname() List.  ((v ∈ free-vars-aux(bnds;y2)) ⇐⇒ (v ∈ free-vars-aux([];y2)) ∧ (¬(v ∈ bnds)))
16. (v ∈ free-vars-aux([];y2))
⊢ ¬(v ∈ y1)
BY
{ ((Assert (v ∈ free-vars-aux(rev(y1) + [];y2)) BY Auto) THEN FLemma `member-free-vars-aux-not-bound` [-1] THEN Auto) }

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. y1 : varname() List
9. y2 : term(opr)
10. (<y1, y2> ∈ bts)
11. l = free-vars-aux(rev(y1) + [];y2) ∈ (varname() List)
12. (v ∈ l)
13. ¬(v ∈ bnds)
14. ∃y@0:bound-term(opr)
     ((y@0 ∈ bts)
     ∧ (free-vars-aux(rev(y1) + bnds;y2) = let vs,a = y@0 in free-vars-aux(rev(vs) + bnds;a) ∈ (varname() List)))
15. ∀v:varname(). ∀bnds:varname() List.  ((v ∈ free-vars-aux(bnds;y2)) ⇐⇒ (v ∈ free-vars-aux([];y2)) ∧ (¬(v ∈ bnds)))
16. (v ∈ free-vars-aux([];y2))
17. (v ∈ free-vars-aux(rev(y1) + [];y2))
18. ¬(v ∈ rev(y1) + [])
⊢ ¬(v ∈ y1)

---

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.  l  :  varname()  List
8.  y1  :  varname()  List
9.  y2  :  term(opr)
10.  (<y1,  y2>  \mmember{}  bts)
11.  l  =  free-vars-aux(rev(y1)  +  [];y2)
12.  (v  \mmember{}  l)
13.  \mneg{}(v  \mmember{}  bnds)
14.  \mexists{}y@0:bound-term(opr)
          ((y@0  \mmember{}  bts)
          \mwedge{}  (free-vars-aux(rev(y1)  +  bnds;y2)  =  let  vs,a  =  y@0  in  free-vars-aux(rev(vs)  +  bnds;a)))
15.  \mforall{}v:varname().  \mforall{}bnds:varname()  List.
            ((v  \mmember{}  free-vars-aux(bnds;y2))  \mLeftarrow{}{}\mRightarrow{}  (v  \mmember{}  free-vars-aux([];y2))  \mwedge{}  (\mneg{}(v  \mmember{}  bnds)))
16.  (v  \mmember{}  free-vars-aux([];y2))
\mvdash{}  \mneg{}(v  \mmember{}  y1)


By

---

Latex:
((Assert  (v  \mmember{}  free-vars-aux(rev(y1)  +  [];y2))  BY
                Auto)
  THEN  FLemma  `member-free-vars-aux-not-bound`  [-1]
  THEN  Auto)

---

Home Index