YES Problem: app(id(),x) -> x app(plus(),0()) -> id() app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) Proof: DP Processor: DPs: app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) TRS: app(id(),x) -> x app(plus(),0()) -> id() app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) EDG Processor: DPs: app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) TRS: app(id(),x) -> x app(plus(),0()) -> id() app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) graph: app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) CDG Processor: DPs: app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) TRS: app(id(),x) -> x app(plus(),0()) -> id() app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) graph: Qed