YES Problem: b(c(a(x1))) -> a(b(x1)) b(b(b(x1))) -> c(a(c(x1))) c(d(x1)) -> d(c(x1)) c(d(b(x1))) -> d(c(c(x1))) d(c(x1)) -> b(b(b(x1))) c(b(x1)) -> d(a(x1)) d(b(c(x1))) -> a(a(x1)) d(a(x1)) -> b(x1) Proof: DP Processor: DPs: b#(c(a(x1))) -> b#(x1) b#(b(b(x1))) -> c#(x1) b#(b(b(x1))) -> c#(a(c(x1))) c#(d(x1)) -> c#(x1) c#(d(x1)) -> d#(c(x1)) c#(d(b(x1))) -> c#(x1) c#(d(b(x1))) -> c#(c(x1)) c#(d(b(x1))) -> d#(c(c(x1))) d#(c(x1)) -> b#(x1) d#(c(x1)) -> b#(b(x1)) d#(c(x1)) -> b#(b(b(x1))) c#(b(x1)) -> d#(a(x1)) d#(a(x1)) -> b#(x1) TRS: b(c(a(x1))) -> a(b(x1)) b(b(b(x1))) -> c(a(c(x1))) c(d(x1)) -> d(c(x1)) c(d(b(x1))) -> d(c(c(x1))) d(c(x1)) -> b(b(b(x1))) c(b(x1)) -> d(a(x1)) d(b(c(x1))) -> a(a(x1)) d(a(x1)) -> b(x1) Matrix Interpretation Processor: dim=1 interpretation: [d#](x0) = 8x0 + 17, [c#](x0) = 8x0 + 2, [b#](x0) = 8x0, [d](x0) = x0 + 4, [b](x0) = x0 + 2, [c](x0) = x0 + 2, [a](x0) = x0 orientation: b#(c(a(x1))) = 8x1 + 16 >= 8x1 = b#(x1) b#(b(b(x1))) = 8x1 + 32 >= 8x1 + 2 = c#(x1) b#(b(b(x1))) = 8x1 + 32 >= 8x1 + 18 = c#(a(c(x1))) c#(d(x1)) = 8x1 + 34 >= 8x1 + 2 = c#(x1) c#(d(x1)) = 8x1 + 34 >= 8x1 + 33 = d#(c(x1)) c#(d(b(x1))) = 8x1 + 50 >= 8x1 + 2 = c#(x1) c#(d(b(x1))) = 8x1 + 50 >= 8x1 + 18 = c#(c(x1)) c#(d(b(x1))) = 8x1 + 50 >= 8x1 + 49 = d#(c(c(x1))) d#(c(x1)) = 8x1 + 33 >= 8x1 = b#(x1) d#(c(x1)) = 8x1 + 33 >= 8x1 + 16 = b#(b(x1)) d#(c(x1)) = 8x1 + 33 >= 8x1 + 32 = b#(b(b(x1))) c#(b(x1)) = 8x1 + 18 >= 8x1 + 17 = d#(a(x1)) d#(a(x1)) = 8x1 + 17 >= 8x1 = b#(x1) b(c(a(x1))) = x1 + 4 >= x1 + 2 = a(b(x1)) b(b(b(x1))) = x1 + 6 >= x1 + 4 = c(a(c(x1))) c(d(x1)) = x1 + 6 >= x1 + 6 = d(c(x1)) c(d(b(x1))) = x1 + 8 >= x1 + 8 = d(c(c(x1))) d(c(x1)) = x1 + 6 >= x1 + 6 = b(b(b(x1))) c(b(x1)) = x1 + 4 >= x1 + 4 = d(a(x1)) d(b(c(x1))) = x1 + 8 >= x1 = a(a(x1)) d(a(x1)) = x1 + 4 >= x1 + 2 = b(x1) problem: DPs: TRS: b(c(a(x1))) -> a(b(x1)) b(b(b(x1))) -> c(a(c(x1))) c(d(x1)) -> d(c(x1)) c(d(b(x1))) -> d(c(c(x1))) d(c(x1)) -> b(b(b(x1))) c(b(x1)) -> d(a(x1)) d(b(c(x1))) -> a(a(x1)) d(a(x1)) -> b(x1) Qed