(VAR x xs xs' ys ) (STRATEGY INNERMOST) (RULES addlist(Cons(x,xs'),Cons(S(0),xs)) -> Cons(S(x),addlist(xs',xs)) addlist(Cons(S(0),xs'),Cons(x,xs)) -> Cons(S(x),addlist(xs',xs)) addlist(Nil,ys) -> Nil notEmpty(Cons(x,xs)) -> True notEmpty(Nil) -> False goal(xs,ys) -> addlist(xs,ys) )