(VAR x y z) (RULES a(lambda(x),y) -> lambda(a(x,p(1,a(y,t)))) a(p(x,y),z) -> p(a(x,z),a(y,z)) a(a(x,y),z) -> a(x,a(y,z)) a(id,x) -> x a(1,id) -> 1 a(t,id) -> t a(1,p(x,y)) -> x a(t,p(x,y)) -> y ) (COMMENT termination of SUBST, see TERESE book page 248)