YES Problem: a(b(x)) -> a(c(b(x))) Proof: DP Processor: DPs: a#(b(x)) -> a#(c(b(x))) TRS: a(b(x)) -> a(c(b(x))) Usable Rule Processor: DPs: a#(b(x)) -> a#(c(b(x))) TRS: Restore Modifier: DPs: a#(b(x)) -> a#(c(b(x))) TRS: a(b(x)) -> a(c(b(x))) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: a#(b(x)) -> a#(c(b(x))) TRS: a(b(x)) -> a(c(b(x))) Matrix Interpretation Processor: dimension: 1 interpretation: [a#](x0) = x0, [c](x0) = 0, [a](x0) = 0, [b](x0) = 1 orientation: a#(b(x)) = 1 >= 0 = a#(c(b(x))) a(b(x)) = 0 >= 0 = a(c(b(x))) problem: DPs: TRS: a(b(x)) -> a(c(b(x))) Qed