YES Problem: app(app(app(uncurry(),f),x),y) -> app(app(f,x),y) Proof: DP Processor: DPs: app#(app(app(uncurry(),f),x),y) -> app#(f,x) app#(app(app(uncurry(),f),x),y) -> app#(app(f,x),y) TRS: app(app(app(uncurry(),f),x),y) -> app(app(f,x),y) KBO Processor: argument filtering: pi(uncurry) = [] pi(app) = [0,1] pi(app#) = 0 usable rules: app(app(app(uncurry(),f),x),y) -> app(app(f,x),y) weight function: w0 = 1 w(app#) = w(uncurry) = 1 w(app) = 0 precedence: app# ~ app ~ uncurry problem: DPs: TRS: app(app(app(uncurry(),f),x),y) -> app(app(f,x),y) Qed