---

Step * 1 1 of Lemma free-vars_functionality


1. opr : Type
2. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. varterm(v) ∈ term(opr)
4. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. bnds1 : varname() List
6. bnds2 : varname() List
7. alpha-aux(opr;bnds1;bnds2;varterm(v);varterm(v1))
⊢ free-vars-aux(bnds1;varterm(v)) = free-vars-aux(bnds2;varterm(v1)) ∈ (varname() List)
BY
{ (Unfold `alpha-aux` -1 THEN Reduce -1 THEN Auto THEN Unfold `free-vars-aux` 0 THEN Reduce 0) }

1
1. opr : Type
2. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. varterm(v) ∈ term(opr)
4. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. bnds1 : varname() List
6. bnds2 : varname() List
7. ↑same-binding(bnds1;bnds2;v;v1)
⊢ if v ∈b bnds1 then [] else [v] fi  = if v1 ∈b bnds2 then [] else [v1] fi  ∈ (varname() List)

---

Latex:

---

Latex:

1.  opr  :  Type
2.  v  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
3.  varterm(v)  \mmember{}  term(opr)
4.  v1  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
5.  bnds1  :  varname()  List
6.  bnds2  :  varname()  List
7.  alpha-aux(opr;bnds1;bnds2;varterm(v);varterm(v1))
\mvdash{}  free-vars-aux(bnds1;varterm(v))  =  free-vars-aux(bnds2;varterm(v1))


By

---

Latex:
(Unfold  `alpha-aux`  -1  THEN  Reduce  -1  THEN  Auto  THEN  Unfold  `free-vars-aux`  0  THEN  Reduce  0)

---

Home Index