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) Usable Rule Processor: DPs: app#(app(apply(),f),x) -> app#(f,x) TRS: Restore Modifier: DPs: app#(app(apply(),f),x) -> app#(f,x) TRS: app(app(apply(),f),x) -> app(f,x) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: app#(app(apply(),f),x) -> app#(f,x) TRS: app(app(apply(),f),x) -> app(f,x) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0, [app](x0, x1) = x0 + x1 + 1, [apply] = 1 orientation: app#(app(apply(),f),x) = f + 2 >= f = app#(f,x) app(app(apply(),f),x) = f + x + 3 >= f + x + 1 = app(f,x) problem: DPs: TRS: app(app(apply(),f),x) -> app(f,x) Qed