YES Problem: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(app(curry(),f),x),y) -> app(app(f,x),y) add() -> app(curry(),plus()) 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)) app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) add#() -> app#(curry(),plus()) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(app(curry(),f),x),y) -> app(app(f,x),y) add() -> app(curry(),plus()) TDG 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)) app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) add#() -> app#(curry(),plus()) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(app(curry(),f),x),y) -> app(app(f,x),y) add() -> app(curry(),plus()) graph: add#() -> app#(curry(),plus()) -> app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) add#() -> app#(curry(),plus()) -> app#(app(app(curry(),f),x),y) -> app#(f,x) add#() -> app#(curry(),plus()) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) add#() -> app#(curry(),plus()) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) add#() -> app#(curry(),plus()) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) -> app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) -> app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(plus(),app(s(),x)),y) -> app#(s(),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)) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) -> app#(app(app(curry(),f),x),y) -> app#(f,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)) 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#(plus(),x) app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) -> app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) -> app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),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#(plus(),x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) 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)) app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) add#() -> app#(curry(),plus()) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(app(curry(),f),x),y) -> app(app(f,x),y) add() -> app(curry(),plus()) graph: app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) 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)) app#(app(app(curry(),f),x),y) -> app#(f,x) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) add#() -> app#(curry(),plus()) TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(app(curry(),f),x),y) -> app(app(f,x),y) add() -> app(curry(),plus()) graph: app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),f),x),y) -> app#(app(f,x),y) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(app(plus(),x),y) app#(app(app(curry(),f),x),y) -> app#(f,x) -> app#(app(plus(),app(s(),x)),y) -> app#(plus(),x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 6/36