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) CDG Processor: DPs: app#(app(apply(),f),x) -> app#(f,x) TRS: app(app(apply(),f),x) -> app(f,x) graph: Qed