---

Step * 1 of Lemma alpha-aux-trans


1. [opr] : Type
2. a : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. varterm(a) ∈ term(opr)
4. b : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. varterm(b) ∈ term(opr)
6. c : {v:varname()| ¬(v = nullvar() ∈ varname())} 
7. varterm(c) ∈ term(opr)
8. us : varname() List
9. vs : varname() List
10. ws : varname() List
11. alpha-aux(opr;us;vs;varterm(a);varterm(b))
12. alpha-aux(opr;vs;ws;varterm(b);varterm(c))
⊢ alpha-aux(opr;us;ws;varterm(a);varterm(c))
BY
{ (All (Unfold `alpha-aux`) THEN All Reduce THEN FLemma `same-binding-trans` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  a  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
3.  varterm(a)  \mmember{}  term(opr)
4.  b  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
5.  varterm(b)  \mmember{}  term(opr)
6.  c  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
7.  varterm(c)  \mmember{}  term(opr)
8.  us  :  varname()  List
9.  vs  :  varname()  List
10.  ws  :  varname()  List
11.  alpha-aux(opr;us;vs;varterm(a);varterm(b))
12.  alpha-aux(opr;vs;ws;varterm(b);varterm(c))
\mvdash{}  alpha-aux(opr;us;ws;varterm(a);varterm(c))


By

---

Latex:
(All  (Unfold  `alpha-aux`)  THEN  All  Reduce  THEN  FLemma  `same-binding-trans`  [-1;-2]  THEN  Auto)

---

Home Index