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()) Usable Rule 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) Matrix Interpretation Processor: dim=1 usable rules: 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) interpretation: [add#] = 7, [app#](x0, x1) = x0, [curry] = 6, [s] = 1, [app](x0, x1) = x0 + x1, [0] = 3, [plus] = 1 orientation: app#(app(plus(),app(s(),x)),y) = x + 2 >= 1 = app#(plus(),x) app#(app(plus(),app(s(),x)),y) = x + 2 >= x + 1 = app#(app(plus(),x),y) app#(app(plus(),app(s(),x)),y) = x + 2 >= 1 = app#(s(),app(app(plus(),x),y)) app#(app(app(curry(),f),x),y) = f + x + 6 >= f = app#(f,x) app#(app(app(curry(),f),x),y) = f + x + 6 >= f + x = app#(app(f,x),y) add#() = 7 >= 6 = app#(curry(),plus()) app(app(plus(),0()),y) = y + 4 >= y = y app(app(plus(),app(s(),x)),y) = x + y + 2 >= x + y + 2 = app(s(),app(app(plus(),x),y)) app(app(app(curry(),f),x),y) = f + x + y + 6 >= f + x + y = app(app(f,x),y) problem: DPs: 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) Qed