YES Problem: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) Proof: DP Processor: DPs: app#(cons(x,xs),ys) -> app#(xs,ys) TRS: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) CDG Processor: DPs: app#(cons(x,xs),ys) -> app#(xs,ys) TRS: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) graph: Qed