YES Problem: f(s(x),y) -> f(x,f(x,y)) f(0(),y) -> c(y,y) Proof: DP Processor: DPs: f#(s(x),y) -> f#(x,y) f#(s(x),y) -> f#(x,f(x,y)) TRS: f(s(x),y) -> f(x,f(x,y)) f(0(),y) -> c(y,y) Subterm Criterion Processor: simple projection: pi(f#) = 0 problem: DPs: TRS: f(s(x),y) -> f(x,f(x,y)) f(0(),y) -> c(y,y) Qed