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