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)) KBO Processor: argument filtering: pi(nil) = [] pi(app) = 0 pi(cons) = [0,1] pi(app#) = 0 weight function: w0 = 1 w(app#) = w(app) = w(nil) = 1 w(cons) = 0 precedence: app# ~ cons ~ app ~ nil problem: DPs: TRS: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) Qed