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) CDG 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) graph: Qed