YES Problem: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(a(b(x1)))) -> a(a(b(b(a(a(b(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) Proof: String Reversal Processor: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) b(a(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) b(a(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) b(b(a(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(a(b(b(a(a(b(x1))))))) b(a(b(a(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> a(b(b(b(a(b(b(x1))))))) b(b(b(a(x1)))) -> b(b(b(b(b(b(b(x1))))))) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [b](x0) = [0 0 0]x0 [0 0 0] , [1 0 1] [0] [a](x0) = [0 0 0]x0 + [1] [0 1 0] [0] orientation: [1 0 1] [0] [1 0 0] a(x1) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(x1) [0 1 0] [0] [0 0 0] [1 1 1] [0] [1 0 1] [0] a(a(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(b(a(x1))) [0 0 0] [1] [0 0 0] [0] [1 0 1] [1 0 0] b(a(x1)) = [0 0 0]x1 >= [0 0 0]x1 = b(b(b(x1))) [0 0 0] [0 0 0] [1 1 1] [1] [1 1 1] [0] a(a(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(b(a(a(x1))))) [0 0 0] [1] [0 0 0] [1] [1 1 1] [1 0 1] b(a(a(x1))) = [0 0 0]x1 >= [0 0 0]x1 = b(a(b(b(a(x1))))) [0 0 0] [0 0 0] [1 0 1] [0] [1 0 0] [0] a(b(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(b(b(a(b(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 1] [1 0 0] b(b(a(x1))) = [0 0 0]x1 >= [0 0 0]x1 = b(b(b(b(b(x1))))) [0 0 0] [0 0 0] [1 1 1] [2] [1 1 1] [2] a(a(a(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(a(b(a(a(a(x1))))))) [0 0 0] [1] [0 0 0] [1] [1 1 1] [1] [1 1 1] b(a(a(a(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(a(a(b(b(a(a(x1))))))) [0 0 0] [0] [0 0 0] [1 1 1] [0] [1 0 1] [0] a(b(a(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(b(a(b(a(b(a(x1))))))) [0 0 0] [0] [0 0 0] [0] [1 1 1] [1 0 1] b(b(a(a(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = b(b(a(b(b(b(a(x1))))))) [0 0 0] [0 0 0] [1 0 1] [0] [1 0 0] [0] a(a(b(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(b(b(a(a(b(x1))))))) [0 0 0] [1] [0 0 0] [1] [1 0 1] [1 0 0] b(a(b(a(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = b(a(b(b(b(a(b(x1))))))) [0 0 0] [0 0 0] [1 0 1] [0] [1 0 0] [0] a(b(b(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(b(b(b(a(b(b(x1))))))) [0 0 0] [0] [0 0 0] [0] [1 0 1] [1 0 0] b(b(b(a(x1)))) = [0 0 0]x1 >= [0 0 0]x1 = b(b(b(b(b(b(b(x1))))))) [0 0 0] [0 0 0] problem: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) b(a(x1)) -> b(b(b(x1))) b(a(a(x1))) -> b(a(b(b(a(x1))))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(b(a(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) b(b(a(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(a(b(b(a(a(b(x1))))))) b(a(b(a(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> a(b(b(b(a(b(b(x1))))))) b(b(b(a(x1)))) -> b(b(b(b(b(b(b(x1))))))) String Reversal Processor: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) DP Processor: DPs: a#(a(x1)) -> a#(b(a(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) EDG Processor: DPs: a#(a(x1)) -> a#(b(a(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) graph: a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) CDG Processor: DPs: a#(a(x1)) -> a#(b(a(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) graph: a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(b(b(x1)))) -> a#(b(b(b(a(b(b(x1))))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(b(x1)))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) SCC Processor: #sccs: 2 #rules: 5 #arcs: 57/169 DPs: a#(a(a(a(x1)))) -> a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(a(b(a(a(a(x1))))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) Arctic Interpretation Processor: dimension: 1 usable rules: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) interpretation: [a#](x0) = x0 + 9, [b](x0) = 6, [a](x0) = 2x0 + 8 orientation: a#(a(a(a(x1)))) = 6x1 + 12 >= 9 = a#(a(b(a(a(a(x1)))))) a#(a(a(a(x1)))) = 6x1 + 12 >= 10 = a#(a(a(b(a(a(a(x1))))))) a(x1) = 2x1 + 8 >= 6 = b(x1) a(a(x1)) = 4x1 + 10 >= 8 = a(b(a(x1))) a(b(x1)) = 8 >= 6 = b(b(b(x1))) a(a(b(x1))) = 10 >= 8 = a(b(b(a(b(x1))))) a(b(a(x1))) = 8 >= 6 = b(a(b(b(a(x1))))) a(b(b(x1))) = 8 >= 6 = b(b(b(b(b(x1))))) a(a(a(a(x1)))) = 8x1 + 14 >= 12 = a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) = 10 >= 8 = a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) = 10 >= 8 = a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) = 8 >= 6 = b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) = 8 >= 6 = b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) = 8 >= 6 = b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) = 8 >= 6 = b(b(b(b(b(b(b(x1))))))) problem: DPs: TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) Qed DPs: a#(b(a(a(x1)))) -> a#(a(b(b(a(a(x1)))))) a#(a(x1)) -> a#(b(a(x1))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: b0(5) -> 6* b0(87) -> 88* b0(62) -> 63* b0(42) -> 43* b0(32) -> 33* b0(99) -> 100* b0(54) -> 55* b0(34) -> 35* b0(4) -> 5* b0(131) -> 132* b0(143) -> 144* b0(133) -> 134* b0(118) -> 119* b0(18) -> 19* b0(145) -> 146* f40() -> 2* a{#,0}(7) -> 1* a0(117) -> 118* a0(97) -> 98* a0(72) -> 73* a0(52) -> 53* a0(2) -> 3* a0(119) -> 120* a0(44) -> 45* a0(121) -> 122* a0(6) -> 7* a0(3) -> 4* a0(120) -> 121* 2 -> 42* 3 -> 34* 4 -> 117* 5 -> 120,73,72,45,4 6 -> 53,32 7 -> 97,18 19 -> 7* 33 -> 52,7 35 -> 44,4 43 -> 3* 44 -> 62* 45 -> 3,34,4 52 -> 54* 53 -> 5* 55 -> 53* 63 -> 45,4 72 -> 87* 73 -> 98,4 88 -> 73,4 97 -> 99* 98 -> 4* 100 -> 98,4 117 -> 145* 118 -> 3,34,122 119 -> 131* 120 -> 143* 121 -> 133* 122 -> 121,4 132 -> 120* 134 -> 122* 144 -> 121* 146 -> 118* problem: DPs: a#(a(x1)) -> a#(b(a(x1))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) Restore Modifier: DPs: a#(a(x1)) -> a#(b(a(x1))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) EDG Processor: DPs: a#(a(x1)) -> a#(b(a(x1))) a#(a(b(a(x1)))) -> a#(b(a(b(a(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) graph: Qed