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)) KBO Processor: argument filtering: pi(compose) = [] pi(app) = [0,1] pi(app#) = [0,1] usable rules: app(app(app(compose(),f),g),x) -> app(f,app(g,x)) weight function: w0 = 1 w(app#) = w(compose) = 1 w(app) = 0 precedence: app ~ compose > app# problem: DPs: TRS: app(app(app(compose(),f),g),x) -> app(f,app(g,x)) Qed