YES Problem: 0(0(1(0(2(x1))))) -> 0(0(1(2(2(x1))))) 0(0(1(0(2(x1))))) -> 0(0(2(1(2(x1))))) 0(0(1(0(2(x1))))) -> 0(1(0(2(2(x1))))) 0(0(1(0(2(x1))))) -> 0(1(1(2(2(x1))))) 0(0(1(0(2(x1))))) -> 0(1(2(0(2(x1))))) 0(0(1(0(2(x1))))) -> 0(1(2(2(0(x1))))) 0(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 0(0(1(0(2(x1))))) -> 0(2(1(0(2(x1))))) 0(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 0(0(1(0(2(x1))))) -> 0(2(2(1(0(x1))))) 0(0(1(0(2(x1))))) -> 0(2(2(1(2(x1))))) 0(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 0(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 0(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 0(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 0(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 0(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 0(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 0(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 0(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 0(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 0(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 0(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 0(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 0(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 0(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 0(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 0(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 0(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 0(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 1(0(1(0(2(x1))))) -> 0(1(2(2(2(x1))))) 1(0(1(0(2(x1))))) -> 0(2(1(2(2(x1))))) 1(0(1(0(2(x1))))) -> 1(0(0(2(2(x1))))) 1(0(1(0(2(x1))))) -> 1(0(1(2(2(x1))))) 1(0(1(0(2(x1))))) -> 1(0(2(0(2(x1))))) 1(0(1(0(2(x1))))) -> 1(0(2(1(2(x1))))) 1(0(1(0(2(x1))))) -> 1(0(2(2(0(x1))))) 1(0(1(0(2(x1))))) -> 1(0(2(2(2(x1))))) 1(0(1(0(2(x1))))) -> 1(1(0(2(2(x1))))) 1(0(1(0(2(x1))))) -> 1(2(0(2(2(x1))))) 1(0(1(0(2(x1))))) -> 1(2(1(0(2(x1))))) 1(0(1(0(2(x1))))) -> 1(2(2(0(2(x1))))) 1(0(1(0(2(x1))))) -> 1(2(2(2(0(x1))))) 1(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 1(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 1(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 1(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 1(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 1(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 1(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 1(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 1(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 1(0(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 1(0(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 1(0(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 1(0(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 1(0(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 1(0(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 1(1(2(0(2(x1))))) -> 0(1(2(2(2(x1))))) 1(1(2(0(2(x1))))) -> 0(2(1(2(2(x1))))) 1(1(2(0(2(x1))))) -> 0(2(2(1(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 1(1(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(2(0(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 1(1(2(0(2(x1))))) -> 1(2(2(0(2(x1))))) 1(1(2(0(2(x1))))) -> 1(2(2(2(0(x1))))) 1(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 1(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 1(1(2(0(2(x1))))) -> 2(1(2(0(2(x1))))) 1(1(2(0(2(x1))))) -> 2(2(0(1(2(x1))))) 1(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 1(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 2(0(1(0(2(x1))))) -> 2(0(1(2(2(x1))))) 2(0(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 2(0(1(0(2(x1))))) -> 2(1(0(2(2(x1))))) 2(0(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 2(0(1(0(2(x1))))) -> 2(1(2(2(0(x1))))) 2(0(1(0(2(x1))))) -> 2(2(0(1(2(x1))))) 2(0(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 2(0(1(0(2(x1))))) -> 2(2(1(2(0(x1))))) 2(0(1(0(2(x1))))) -> 2(2(2(1(0(x1))))) 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 2(1(1(0(2(x1))))) -> 2(0(2(1(2(x1))))) 2(1(1(0(2(x1))))) -> 2(1(2(0(2(x1))))) 2(1(1(0(2(x1))))) -> 2(2(1(0(2(x1))))) 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [1](x0) = 1x0, [0](x0) = 1x0, [2](x0) = x0 orientation: 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 0(0(1(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 0(0(2(1(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 0(1(0(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 0(1(1(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 0(1(2(0(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 0(1(2(2(0(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 0(1(2(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 0(2(1(0(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 0(2(1(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 0(2(2(1(0(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 0(2(2(1(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(0(0(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(0(2(0(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(0(2(2(0(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 1(0(2(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(1(0(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 1(2(0(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(2(1(0(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 1(2(2(0(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 1(2(2(2(0(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(1(0(2(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(2(1(0(2(x1))))) 0(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(2(2(1(0(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 3x1 = 0(1(0(2(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 3x1 = 0(1(1(2(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 2x1 = 0(1(2(2(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 3x1 = 0(2(1(0(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 2x1 = 0(2(1(2(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 3x1 = 0(2(2(1(0(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 2x1 = 0(2(2(1(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 2x1 = 1(0(2(2(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(0(2(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(2(0(2(x1))))) 0(1(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(2(2(0(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 0(1(2(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 0(2(1(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(0(0(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(0(1(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(0(2(0(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(0(2(1(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(0(2(2(0(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 1(0(2(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(1(0(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 1(2(0(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 3x1 = 1(2(1(0(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 1(2(2(0(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 1(2(2(2(0(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(0(1(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(0(2(1(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(1(0(2(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(1(2(0(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(1(2(2(0(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(2(0(1(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(2(1(0(2(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(2(1(2(0(x1))))) 1(0(1(0(2(x1))))) = 4x1 >= 2x1 = 2(2(2(1(0(x1))))) 1(0(2(0(2(x1))))) = 3x1 >= 2x1 = 1(0(2(2(2(x1))))) 1(0(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(0(2(2(x1))))) 1(0(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(2(0(2(x1))))) 1(0(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(2(2(0(x1))))) 1(0(2(0(2(x1))))) = 3x1 >= 2x1 = 2(1(0(2(2(x1))))) 1(0(2(0(2(x1))))) = 3x1 >= 2x1 = 2(2(1(0(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 0(1(2(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 0(2(1(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 0(2(2(1(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 3x1 = 1(0(0(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 3x1 = 1(0(1(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 3x1 = 1(0(2(0(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 3x1 = 1(0(2(1(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 3x1 = 1(0(2(2(0(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 1(0(2(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 3x1 = 1(1(0(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(0(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 3x1 = 1(2(1(0(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(2(0(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 1(2(2(2(0(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 2(0(1(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 2(1(0(2(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 2(1(2(0(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 2(2(0(1(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 2(2(1(0(2(x1))))) 1(1(2(0(2(x1))))) = 3x1 >= 2x1 = 2(2(2(1(0(x1))))) 1(2(2(0(2(x1))))) = 2x1 >= 2x1 = 1(0(2(2(2(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(0(1(2(2(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(0(2(1(2(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(1(0(2(2(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(1(2(0(2(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(1(2(2(0(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(2(0(1(2(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(2(1(0(2(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(2(1(2(0(x1))))) 2(0(1(0(2(x1))))) = 3x1 >= 2x1 = 2(2(2(1(0(x1))))) 2(1(1(0(2(x1))))) = 3x1 >= 3x1 = 2(0(1(0(2(x1))))) 2(1(1(0(2(x1))))) = 3x1 >= 2x1 = 2(0(2(1(2(x1))))) 2(1(1(0(2(x1))))) = 3x1 >= 2x1 = 2(1(2(0(2(x1))))) 2(1(1(0(2(x1))))) = 3x1 >= 2x1 = 2(2(1(0(2(x1))))) 2(1(2(0(2(x1))))) = 2x1 >= 2x1 = 2(0(1(2(2(x1))))) 2(1(2(0(2(x1))))) = 2x1 >= 2x1 = 2(1(0(2(2(x1))))) 2(1(2(0(2(x1))))) = 2x1 >= 2x1 = 2(2(1(0(2(x1))))) 2(1(2(0(2(x1))))) = 2x1 >= 2x1 = 2(2(2(1(0(x1))))) problem: 0(1(2(0(2(x1))))) -> 0(1(0(2(2(x1))))) 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 0(1(2(0(2(x1))))) -> 0(2(1(0(2(x1))))) 0(1(2(0(2(x1))))) -> 0(2(2(1(0(x1))))) 1(1(2(0(2(x1))))) -> 1(0(0(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(2(0(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(2(2(0(x1))))) 1(1(2(0(2(x1))))) -> 1(1(0(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 1(2(2(0(2(x1))))) -> 1(0(2(2(2(x1))))) 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) 2(1(2(0(2(x1))))) -> 2(1(0(2(2(x1))))) 2(1(2(0(2(x1))))) -> 2(2(1(0(2(x1))))) 2(1(2(0(2(x1))))) -> 2(2(2(1(0(x1))))) Matrix Interpretation Processor: dim=3 interpretation: [1 1 0] [1](x0) = [0 0 0]x0 [0 0 0] , [1 0 0] [0](x0) = [0 0 0]x0 [0 0 0] , [1 0 0] [0] [2](x0) = [0 0 0]x0 + [1] [0 0 0] [0] orientation: [1 0 0] [1] [1 0 0] 0(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(1(0(2(2(x1))))) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] [1] 0(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(1(1(2(2(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] 0(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(1(0(2(x1))))) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] 0(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(2(2(1(0(x1))))) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] 1(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(0(2(2(x1))))) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] [1] 1(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(1(2(2(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] 1(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(2(0(2(x1))))) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] [1] 1(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(0(2(1(2(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] 1(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(2(2(0(x1))))) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] 1(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(1(0(2(2(x1))))) [0 0 0] [0] [0 0 0] [1 0 0] [1] [1 0 0] [1] 1(1(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(0(2(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] 1(2(2(0(2(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 1(0(2(2(2(x1))))) [0 0 0] [0] [0 0 0] [1 0 0] [0] [1 0 0] [0] 2(1(1(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(1(0(2(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] [1] 2(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(0(1(2(2(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] [0] 2(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(1(0(2(2(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] [0] 2(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(2(1(0(2(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1] [1 0 0] [0] 2(1(2(0(2(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(2(2(1(0(x1))))) [0 0 0] [0] [0 0 0] [0] problem: 0(1(2(0(2(x1))))) -> 0(1(1(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(1(2(2(x1))))) 1(1(2(0(2(x1))))) -> 1(0(2(1(2(x1))))) 1(1(2(0(2(x1))))) -> 1(2(1(0(2(x1))))) 2(1(1(0(2(x1))))) -> 2(0(1(0(2(x1))))) 2(1(2(0(2(x1))))) -> 2(0(1(2(2(x1))))) String Reversal Processor: 2(0(2(1(0(x1))))) -> 2(2(1(1(0(x1))))) 2(0(2(1(1(x1))))) -> 2(2(1(0(1(x1))))) 2(0(2(1(1(x1))))) -> 2(1(2(0(1(x1))))) 2(0(2(1(1(x1))))) -> 2(0(1(2(1(x1))))) 2(0(1(1(2(x1))))) -> 2(0(1(0(2(x1))))) 2(0(2(1(2(x1))))) -> 2(2(1(0(2(x1))))) Bounds Processor: bound: 1 enrichment: match automaton: final states: {4} transitions: 21(15) -> 16* 21(27) -> 28* 21(39) -> 40* 21(24) -> 25* 21(14) -> 15* 21(36) -> 37* 11(25) -> 26* 11(17) -> 18* 11(12) -> 13* 11(28) -> 29* 11(13) -> 14* 01(37) -> 38* 01(29) -> 30* 01(11) -> 12* 01(53) -> 54* 01(18) -> 19* 20(4) -> 4* 00(4) -> 4* 10(4) -> 4* 4 -> 36,17,11 16 -> 25,37,4 18 -> 27* 19 -> 24,13 25 -> 53* 26 -> 15* 29 -> 39* 30 -> 15* 38 -> 28* 40 -> 15* 54 -> 13* problem: Qed