YES Problem: a(b(x1)) -> x1 a(b(x1)) -> b(c(x1)) a(c(x1)) -> c(b(a(a(x1)))) Proof: DP Processor: DPs: a#(c(x1)) -> a#(x1) a#(c(x1)) -> a#(a(x1)) TRS: a(b(x1)) -> x1 a(b(x1)) -> b(c(x1)) a(c(x1)) -> c(b(a(a(x1)))) Matrix Interpretation Processor: dim=1 interpretation: [a#](x0) = 2x0 + 4, [c](x0) = 2x0 + 4, [a](x0) = 2x0 + 2, [b](x0) = 1/2x0 orientation: a#(c(x1)) = 4x1 + 12 >= 2x1 + 4 = a#(x1) a#(c(x1)) = 4x1 + 12 >= 4x1 + 8 = a#(a(x1)) a(b(x1)) = x1 + 2 >= x1 = x1 a(b(x1)) = x1 + 2 >= x1 + 2 = b(c(x1)) a(c(x1)) = 4x1 + 10 >= 4x1 + 10 = c(b(a(a(x1)))) problem: DPs: TRS: a(b(x1)) -> x1 a(b(x1)) -> b(c(x1)) a(c(x1)) -> c(b(a(a(x1)))) Qed