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