YES Problem: app(app(app(compose(),f),g),x) -> app(f,app(g,x)) Proof: DP Processor: DPs: app#(app(app(compose(),f),g),x) -> app#(g,x) app#(app(app(compose(),f),g),x) -> app#(f,app(g,x)) TRS: app(app(app(compose(),f),g),x) -> app(f,app(g,x)) CDG Processor: DPs: app#(app(app(compose(),f),g),x) -> app#(g,x) app#(app(app(compose(),f),g),x) -> app#(f,app(g,x)) TRS: app(app(app(compose(),f),g),x) -> app(f,app(g,x)) graph: Qed