(from AG01 4.35)
(VAR k l l' s s' t t' x x' y z)
(RULES
and(true,y) -> y
and(false,y) -> false
eq(nil,nil) -> true
eq(cons(t,l),nil) -> false
eq(nil,cons(t,l)) -> false
eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
eq(var(l),var(l')) -> eq(l,l')
eq(var(l),apply(t,s)) -> false
eq(var(l),lambda(x,t)) -> false
eq(apply(t,s),var(l)) -> false
eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
eq(apply(t,s),lambda(x,t)) -> false
eq(lambda(x,t),var(l)) -> false
eq(lambda(x,t),apply(t,s)) -> false
eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
if(true,var(k),var(l')) -> var(k)
if(false,var(k),var(l')) -> var(l')
ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
ren(x,y,lambda(z,t)) -> lambda(var(cons(x,cons(y,cons(lambda(z,t),nil)))),ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil)))),t))))