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)) Subterm Criterion Processor: simple projection: pi(app#) = 0 problem: DPs: TRS: app(app(app(compose(),f),g),x) -> app(f,app(g,x)) Qed