YES(?,O(n^1)) 41.19/11.01 YES(?,O(n^1)) 41.19/11.02 41.19/11.02 Problem: 41.19/11.02 a(x1) -> b(x1) 41.19/11.02 a(a(x1)) -> a(b(a(x1))) 41.19/11.02 a(b(x1)) -> b(b(b(x1))) 41.19/11.02 a(a(a(x1))) -> a(a(b(a(a(x1))))) 41.19/11.02 a(a(b(x1))) -> a(b(b(a(b(x1))))) 41.19/11.02 a(b(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.02 a(b(b(x1))) -> b(b(b(b(b(x1))))) 41.19/11.02 b(a(x1)) -> b(b(b(x1))) 41.19/11.02 a(b(a(x1))) -> a(b(b(a(b(x1))))) 41.19/11.02 b(a(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.02 b(b(a(x1))) -> b(b(b(b(b(x1))))) 41.19/11.02 41.19/11.02 Proof: 41.19/11.02 Complexity Transformation Processor: 41.19/11.02 strict: 41.19/11.02 a(x1) -> b(x1) 41.19/11.02 a(a(x1)) -> a(b(a(x1))) 41.19/11.02 a(b(x1)) -> b(b(b(x1))) 41.19/11.02 a(a(a(x1))) -> a(a(b(a(a(x1))))) 41.19/11.02 a(a(b(x1))) -> a(b(b(a(b(x1))))) 41.19/11.02 a(b(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.02 a(b(b(x1))) -> b(b(b(b(b(x1))))) 41.19/11.02 b(a(x1)) -> b(b(b(x1))) 41.19/11.02 a(b(a(x1))) -> a(b(b(a(b(x1))))) 41.19/11.02 b(a(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.02 b(b(a(x1))) -> b(b(b(b(b(x1))))) 41.19/11.02 weak: 41.19/11.02 41.19/11.02 Matrix Interpretation Processor: dim=1 41.19/11.02 41.19/11.02 max_matrix: 41.19/11.02 1 41.19/11.02 interpretation: 41.19/11.02 [b](x0) = x0, 41.19/11.02 41.19/11.02 [a](x0) = x0 + 2 41.19/11.02 orientation: 41.19/11.02 a(x1) = x1 + 2 >= x1 = b(x1) 41.19/11.02 41.19/11.02 a(a(x1)) = x1 + 4 >= x1 + 4 = a(b(a(x1))) 41.19/11.02 41.19/11.02 a(b(x1)) = x1 + 2 >= x1 = b(b(b(x1))) 41.19/11.02 41.19/11.02 a(a(a(x1))) = x1 + 6 >= x1 + 8 = a(a(b(a(a(x1))))) 41.19/11.02 41.19/11.02 a(a(b(x1))) = x1 + 4 >= x1 + 4 = a(b(b(a(b(x1))))) 41.19/11.02 41.19/11.02 a(b(a(x1))) = x1 + 4 >= x1 + 4 = b(a(b(b(a(x1))))) 41.19/11.02 41.19/11.02 a(b(b(x1))) = x1 + 2 >= x1 = b(b(b(b(b(x1))))) 41.19/11.02 41.19/11.02 b(a(x1)) = x1 + 2 >= x1 = b(b(b(x1))) 41.19/11.02 41.19/11.02 a(b(a(x1))) = x1 + 4 >= x1 + 4 = a(b(b(a(b(x1))))) 41.19/11.02 41.19/11.02 b(a(a(x1))) = x1 + 4 >= x1 + 4 = b(a(b(b(a(x1))))) 41.19/11.02 41.19/11.02 b(b(a(x1))) = x1 + 2 >= x1 = b(b(b(b(b(x1))))) 41.19/11.02 problem: 41.19/11.02 strict: 41.19/11.02 a(a(x1)) -> a(b(a(x1))) 41.19/11.02 a(a(a(x1))) -> a(a(b(a(a(x1))))) 41.19/11.02 a(a(b(x1))) -> a(b(b(a(b(x1))))) 41.19/11.02 a(b(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.02 a(b(a(x1))) -> a(b(b(a(b(x1))))) 41.19/11.02 b(a(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.02 weak: 41.19/11.02 a(x1) -> b(x1) 41.19/11.02 a(b(x1)) -> b(b(b(x1))) 41.19/11.02 a(b(b(x1))) -> b(b(b(b(b(x1))))) 41.19/11.02 b(a(x1)) -> b(b(b(x1))) 41.19/11.02 b(b(a(x1))) -> b(b(b(b(b(x1))))) 41.19/11.02 Matrix Interpretation Processor: dim=3 41.19/11.02 41.19/11.02 max_matrix: 41.19/11.02 [1 0 1] 41.19/11.02 [0 0 1] 41.19/11.02 [0 0 0] 41.19/11.02 interpretation: 41.19/11.02 [1 0 0] 41.19/11.02 [b](x0) = [0 0 0]x0 41.19/11.02 [0 0 0] , 41.19/11.02 41.19/11.02 [1 0 1] [0] 41.19/11.02 [a](x0) = [0 0 1]x0 + [0] 41.19/11.02 [0 0 0] [1] 41.19/11.02 orientation: 41.19/11.02 [1 0 1] [1] [1 0 1] [0] 41.19/11.02 a(a(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = a(b(a(x1))) 41.19/11.02 [0 0 0] [1] [0 0 0] [1] 41.19/11.02 41.19/11.02 [1 0 1] [2] [1 0 1] [2] 41.19/11.02 a(a(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(b(a(a(x1))))) 41.19/11.02 [0 0 0] [1] [0 0 0] [1] 41.19/11.02 41.19/11.02 [1 0 0] [1] [1 0 0] [0] 41.19/11.02 a(a(b(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = a(b(b(a(b(x1))))) 41.19/11.02 [0 0 0] [1] [0 0 0] [1] 41.19/11.02 41.19/11.02 [1 0 1] [0] [1 0 1] 41.19/11.02 a(b(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(a(b(b(a(x1))))) 41.19/11.02 [0 0 0] [1] [0 0 0] 41.19/11.02 41.19/11.02 [1 0 1] [0] [1 0 0] [0] 41.19/11.02 a(b(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = a(b(b(a(b(x1))))) 41.19/11.02 [0 0 0] [1] [0 0 0] [1] 41.19/11.02 41.19/11.02 [1 0 1] [1] [1 0 1] 41.19/11.02 b(a(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(a(b(b(a(x1))))) 41.19/11.02 [0 0 0] [0] [0 0 0] 41.19/11.02 41.19/11.02 [1 0 1] [0] [1 0 0] 41.19/11.02 a(x1) = [0 0 1]x1 + [0] >= [0 0 0]x1 = b(x1) 41.19/11.02 [0 0 0] [1] [0 0 0] 41.19/11.02 41.19/11.02 [1 0 0] [0] [1 0 0] 41.19/11.02 a(b(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(b(b(x1))) 41.19/11.02 [0 0 0] [1] [0 0 0] 41.19/11.02 41.19/11.02 [1 0 0] [0] [1 0 0] 41.19/11.02 a(b(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(b(b(b(b(x1))))) 41.19/11.02 [0 0 0] [1] [0 0 0] 41.19/11.02 41.19/11.02 [1 0 1] [1 0 0] 41.19/11.03 b(a(x1)) = [0 0 0]x1 >= [0 0 0]x1 = b(b(b(x1))) 41.19/11.03 [0 0 0] [0 0 0] 41.19/11.03 41.19/11.03 [1 0 1] [1 0 0] 41.19/11.03 b(b(a(x1))) = [0 0 0]x1 >= [0 0 0]x1 = b(b(b(b(b(x1))))) 41.19/11.03 [0 0 0] [0 0 0] 41.19/11.03 problem: 41.19/11.03 strict: 41.19/11.03 a(a(a(x1))) -> a(a(b(a(a(x1))))) 41.19/11.03 a(b(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.03 a(b(a(x1))) -> a(b(b(a(b(x1))))) 41.19/11.03 weak: 41.19/11.03 a(a(x1)) -> a(b(a(x1))) 41.19/11.03 a(a(b(x1))) -> a(b(b(a(b(x1))))) 41.19/11.03 b(a(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.03 a(x1) -> b(x1) 41.19/11.03 a(b(x1)) -> b(b(b(x1))) 41.19/11.03 a(b(b(x1))) -> b(b(b(b(b(x1))))) 41.19/11.03 b(a(x1)) -> b(b(b(x1))) 41.19/11.03 b(b(a(x1))) -> b(b(b(b(b(x1))))) 41.19/11.03 Splitting Processor: 41.19/11.03 strict: 41.19/11.03 a(a(a(x1))) -> a(a(b(a(a(x1))))) 41.19/11.03 weak: 41.19/11.03 a(a(x1)) -> a(b(a(x1))) 41.19/11.03 a(a(b(x1))) -> a(b(b(a(b(x1))))) 41.19/11.03 b(a(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.03 a(x1) -> b(x1) 41.19/11.03 a(b(x1)) -> b(b(b(x1))) 41.19/11.03 a(b(b(x1))) -> b(b(b(b(b(x1))))) 41.19/11.03 b(a(x1)) -> b(b(b(x1))) 41.19/11.03 b(b(a(x1))) -> b(b(b(b(b(x1))))) 41.19/11.03 a(b(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.03 a(b(a(x1))) -> a(b(b(a(b(x1))))) 41.19/11.03 Matrix Interpretation Processor: dim=3 41.19/11.03 41.19/11.03 max_matrix: 41.19/11.03 [1 1 1] 41.19/11.03 [0 0 3] 41.19/11.03 [0 0 0] 41.19/11.03 interpretation: 41.19/11.03 [1 0 0] 41.19/11.03 [b](x0) = [0 0 1]x0 41.19/11.03 [0 0 0] , 41.19/11.03 41.19/11.03 [1 1 1] [0] 41.19/11.03 [a](x0) = [0 0 3]x0 + [1] 41.19/11.03 [0 0 0] [1] 41.19/11.03 orientation: 41.19/11.03 [1 1 1] [1] [1 1 1] [0] 41.19/11.03 a(b(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(a(b(b(a(x1))))) 41.19/11.03 [0 0 0] [1] [0 0 0] [0] 41.19/11.03 41.19/11.03 [1 1 1] [1] [1 0 1] [0] 41.19/11.03 a(b(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(b(b(a(b(x1))))) 41.19/11.03 [0 0 0] [1] [0 0 0] [1] 41.19/11.03 41.19/11.03 [1 1 4] [7] [1 1 4] [5] 41.19/11.03 a(a(a(x1))) = [0 0 0]x1 + [4] >= [0 0 0]x1 + [4] = a(a(b(a(a(x1))))) 41.19/11.03 [0 0 0] [1] [0 0 0] [1] 41.19/11.03 41.19/11.03 [1 1 4] [2] [1 1 1] [1] 41.19/11.03 a(a(x1)) = [0 0 0]x1 + [4] >= [0 0 0]x1 + [1] = a(b(a(x1))) 41.19/11.03 [0 0 0] [1] [0 0 0] [1] 41.19/11.03 41.19/11.03 [1 0 1] [2] [1 0 1] [0] 41.19/11.03 a(a(b(x1))) = [0 0 0]x1 + [4] >= [0 0 0]x1 + [1] = a(b(b(a(b(x1))))) 41.19/11.03 [0 0 0] [1] [0 0 0] [1] 41.19/11.03 41.19/11.03 [1 1 4] [2] [1 1 1] [0] 41.19/11.03 b(a(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(a(b(b(a(x1))))) 41.19/11.03 [0 0 0] [0] [0 0 0] [0] 41.19/11.03 41.19/11.03 [1 1 1] [0] [1 0 0] 41.19/11.03 a(x1) = [0 0 3]x1 + [1] >= [0 0 1]x1 = b(x1) 41.19/11.03 [0 0 0] [1] [0 0 0] 41.19/11.03 41.19/11.03 [1 0 1] [0] [1 0 0] 41.19/11.03 a(b(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(b(x1))) 41.19/11.03 [0 0 0] [1] [0 0 0] 41.19/11.03 41.19/11.03 [1 0 0] [0] [1 0 0] 41.19/11.03 a(b(b(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(b(b(b(x1))))) 41.19/11.03 [0 0 0] [1] [0 0 0] 41.19/11.03 41.19/11.03 [1 1 1] [0] [1 0 0] 41.19/11.03 b(a(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(b(x1))) 41.19/11.03 [0 0 0] [0] [0 0 0] 41.19/11.03 41.19/11.03 [1 1 1] [1 0 0] 41.19/11.03 b(b(a(x1))) = [0 0 0]x1 >= [0 0 0]x1 = b(b(b(b(b(x1))))) 41.19/11.03 [0 0 0] [0 0 0] 41.19/11.03 problem: 41.19/11.03 strict: 41.19/11.03 41.19/11.03 weak: 41.19/11.03 a(b(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.03 a(b(a(x1))) -> a(b(b(a(b(x1))))) 41.19/11.03 a(a(a(x1))) -> a(a(b(a(a(x1))))) 41.19/11.03 a(a(x1)) -> a(b(a(x1))) 41.19/11.03 a(a(b(x1))) -> a(b(b(a(b(x1))))) 41.19/11.04 b(a(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.04 a(x1) -> b(x1) 41.19/11.04 a(b(x1)) -> b(b(b(x1))) 41.19/11.04 a(b(b(x1))) -> b(b(b(b(b(x1))))) 41.19/11.04 b(a(x1)) -> b(b(b(x1))) 41.19/11.04 b(b(a(x1))) -> b(b(b(b(b(x1))))) 41.19/11.04 Qed 41.19/11.04 41.19/11.04 strict: 41.19/11.04 a(b(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.04 a(b(a(x1))) -> a(b(b(a(b(x1))))) 41.19/11.04 weak: 41.19/11.04 a(a(a(x1))) -> a(a(b(a(a(x1))))) 41.19/11.04 a(a(x1)) -> a(b(a(x1))) 41.19/11.04 a(a(b(x1))) -> a(b(b(a(b(x1))))) 41.19/11.04 b(a(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.04 a(x1) -> b(x1) 41.19/11.04 a(b(x1)) -> b(b(b(x1))) 41.19/11.04 a(b(b(x1))) -> b(b(b(b(b(x1))))) 41.19/11.04 b(a(x1)) -> b(b(b(x1))) 41.19/11.04 b(b(a(x1))) -> b(b(b(b(b(x1))))) 41.19/11.04 Matrix Interpretation Processor: dim=5 41.19/11.04 41.19/11.04 max_matrix: 41.19/11.04 [1 0 0 1 0] 41.19/11.04 [0 0 0 0 0] 41.19/11.04 [0 0 0 0 0] 41.19/11.04 [0 0 0 0 1] 41.19/11.04 [0 0 0 0 0] 41.19/11.04 interpretation: 41.19/11.04 [1 0 0 0 0] 41.19/11.04 [0 0 0 0 0] 41.19/11.04 [b](x0) = [0 0 0 0 0]x0 41.19/11.04 [0 0 0 0 0] 41.19/11.04 [0 0 0 0 0] , 41.19/11.04 41.19/11.04 [1 0 0 1 0] [0] 41.19/11.04 [0 0 0 0 0] [0] 41.19/11.04 [a](x0) = [0 0 0 0 0]x0 + [0] 41.19/11.04 [0 0 0 0 1] [0] 41.19/11.04 [0 0 0 0 0] [1] 41.19/11.04 orientation: 41.19/11.04 [1 0 0 1 1] [1] [1 0 0 1 1] [0] 41.19/11.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 41.19/11.04 a(a(a(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = a(a(b(a(a(x1))))) 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 41.19/11.04 41.19/11.04 [1 0 0 1 1] [0] [1 0 0 1 0] [0] 41.19/11.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 41.19/11.04 a(a(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = a(b(a(x1))) 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 41.19/11.04 41.19/11.04 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 41.19/11.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 41.19/11.04 a(a(b(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = a(b(b(a(b(x1))))) 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 41.19/11.04 41.19/11.04 [1 0 0 1 1] [1 0 0 1 0] 41.19/11.04 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.04 b(a(a(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = b(a(b(b(a(x1))))) 41.19/11.04 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.04 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.04 41.19/11.04 [1 0 0 1 0] [0] [1 0 0 0 0] 41.19/11.04 [0 0 0 0 0] [0] [0 0 0 0 0] 41.19/11.04 a(x1) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = b(x1) 41.19/11.04 [0 0 0 0 1] [0] [0 0 0 0 0] 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] 41.19/11.04 41.19/11.04 [1 0 0 0 0] [0] [1 0 0 0 0] 41.19/11.04 [0 0 0 0 0] [0] [0 0 0 0 0] 41.19/11.04 a(b(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = b(b(b(x1))) 41.19/11.04 [0 0 0 0 0] [0] [0 0 0 0 0] 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] 41.19/11.04 41.19/11.04 [1 0 0 0 0] [0] [1 0 0 0 0] 41.19/11.04 [0 0 0 0 0] [0] [0 0 0 0 0] 41.19/11.04 a(b(b(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = b(b(b(b(b(x1))))) 41.19/11.04 [0 0 0 0 0] [0] [0 0 0 0 0] 41.19/11.04 [0 0 0 0 0] [1] [0 0 0 0 0] 41.19/11.04 41.19/11.04 [1 0 0 1 0] [1 0 0 0 0] 41.19/11.04 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.04 b(a(x1)) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = b(b(b(x1))) 41.19/11.04 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.05 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.05 41.19/11.05 [1 0 0 1 0] [1 0 0 0 0] 41.19/11.05 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.05 b(b(a(x1))) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = b(b(b(b(b(x1))))) 41.19/11.05 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.05 [0 0 0 0 0] [0 0 0 0 0] 41.19/11.05 41.19/11.05 [1 0 0 1 0] [0] [1 0 0 1 0] 41.19/11.05 [0 0 0 0 0] [0] [0 0 0 0 0] 41.19/11.05 a(b(a(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = b(a(b(b(a(x1))))) 41.19/11.05 [0 0 0 0 0] [0] [0 0 0 0 0] 41.19/11.05 [0 0 0 0 0] [1] [0 0 0 0 0] 41.19/11.05 41.19/11.05 [1 0 0 1 0] [0] [1 0 0 0 0] [0] 41.19/11.05 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 41.19/11.05 a(b(a(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = a(b(b(a(b(x1))))) 41.19/11.05 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 41.19/11.05 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 41.19/11.05 problem: 41.19/11.05 strict: 41.19/11.05 41.19/11.05 weak: 41.19/11.05 a(a(a(x1))) -> a(a(b(a(a(x1))))) 41.19/11.05 a(a(x1)) -> a(b(a(x1))) 41.19/11.05 a(a(b(x1))) -> a(b(b(a(b(x1))))) 41.19/11.05 b(a(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.05 a(x1) -> b(x1) 41.19/11.05 a(b(x1)) -> b(b(b(x1))) 41.19/11.05 a(b(b(x1))) -> b(b(b(b(b(x1))))) 41.19/11.05 b(a(x1)) -> b(b(b(x1))) 41.19/11.05 b(b(a(x1))) -> b(b(b(b(b(x1))))) 41.19/11.05 a(b(a(x1))) -> b(a(b(b(a(x1))))) 41.19/11.05 a(b(a(x1))) -> a(b(b(a(b(x1))))) 41.19/11.05 Qed 41.19/11.05 EOF