YES Problem: a(x1) -> b(b(x1)) b(b(b(x1))) -> a(x1) Proof: DP Processor: DPs: a#(x1) -> b#(x1) a#(x1) -> b#(b(x1)) b#(b(b(x1))) -> a#(x1) TRS: a(x1) -> b(b(x1)) b(b(b(x1))) -> a(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = 1x0, [a#](x0) = 8x0, [b](x0) = 5x0, [a](x0) = 14x0 orientation: a#(x1) = 8x1 >= 1x1 = b#(x1) a#(x1) = 8x1 >= 6x1 = b#(b(x1)) b#(b(b(x1))) = 11x1 >= 8x1 = a#(x1) a(x1) = 14x1 >= 10x1 = b(b(x1)) b(b(b(x1))) = 15x1 >= 14x1 = a(x1) problem: DPs: TRS: a(x1) -> b(b(x1)) b(b(b(x1))) -> a(x1) Qed