YES(?,O(n^1)) 294.13/75.31 YES(?,O(n^1)) 294.13/75.32 294.13/75.32 Problem: 294.13/75.32 a(a(x1)) -> b(a(b(x1))) 294.13/75.32 a(a(a(x1))) -> a(b(a(b(a(x1))))) 294.13/75.32 a(b(a(x1))) -> b(b(a(b(b(x1))))) 294.13/75.32 a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) 294.13/75.32 a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) 294.13/75.32 a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) 294.13/75.32 a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) 294.13/75.32 a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.32 a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.32 a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.32 a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.32 a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.32 a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.32 a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.32 a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.32 294.13/75.32 Proof: 294.13/75.32 Complexity Transformation Processor: 294.13/75.32 strict: 294.13/75.32 a(a(x1)) -> b(a(b(x1))) 294.13/75.32 a(a(a(x1))) -> a(b(a(b(a(x1))))) 294.13/75.32 a(b(a(x1))) -> b(b(a(b(b(x1))))) 294.13/75.32 a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) 294.13/75.32 a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) 294.13/75.32 a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) 294.13/75.32 a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) 294.13/75.32 a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.32 a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.32 a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.32 a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.32 a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.32 a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.32 a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.32 a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.32 weak: 294.13/75.32 294.13/75.32 Matrix Interpretation Processor: dim=1 294.13/75.32 294.13/75.32 max_matrix: 294.13/75.32 1 294.13/75.32 interpretation: 294.13/75.32 [b](x0) = x0, 294.13/75.32 294.13/75.32 [a](x0) = x0 + 21 294.13/75.32 orientation: 294.13/75.32 a(a(x1)) = x1 + 42 >= x1 + 21 = b(a(b(x1))) 294.13/75.32 294.13/75.32 a(a(a(x1))) = x1 + 63 >= x1 + 63 = a(b(a(b(a(x1))))) 294.13/75.32 294.13/75.32 a(b(a(x1))) = x1 + 42 >= x1 + 21 = b(b(a(b(b(x1))))) 294.13/75.32 294.13/75.32 a(a(a(a(x1)))) = x1 + 84 >= x1 + 105 = a(a(b(a(b(a(a(x1))))))) 294.13/75.32 294.13/75.32 a(a(b(a(x1)))) = x1 + 63 >= x1 + 63 = a(b(b(a(b(a(b(x1))))))) 294.13/75.32 294.13/75.32 a(b(a(a(x1)))) = x1 + 63 >= x1 + 63 = b(a(b(a(b(b(a(x1))))))) 294.13/75.32 294.13/75.32 a(b(b(a(x1)))) = x1 + 42 >= x1 + 21 = b(b(b(a(b(b(b(x1))))))) 294.13/75.32 294.13/75.32 a(a(a(a(a(x1))))) = x1 + 105 >= x1 + 147 = a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.32 294.13/75.32 a(a(a(b(a(x1))))) = x1 + 84 >= x1 + 105 = a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.32 294.13/75.32 a(a(b(a(a(x1))))) = x1 + 84 >= x1 + 105 = a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.32 294.13/75.32 a(a(b(b(a(x1))))) = x1 + 63 >= x1 + 63 = a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.32 294.13/75.32 a(b(a(a(a(x1))))) = x1 + 84 >= x1 + 105 = b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.32 294.13/75.32 a(b(a(b(a(x1))))) = x1 + 63 >= x1 + 63 = b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.32 294.13/75.32 a(b(b(a(a(x1))))) = x1 + 63 >= x1 + 63 = b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.32 294.13/75.32 a(b(b(b(a(x1))))) = x1 + 42 >= x1 + 21 = b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.32 problem: 294.13/75.32 strict: 294.13/75.32 a(a(a(x1))) -> a(b(a(b(a(x1))))) 294.13/75.32 a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) 294.13/75.32 a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) 294.13/75.32 a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) 294.13/75.32 a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.32 a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.32 a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.32 a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.32 a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.32 a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.32 a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.32 weak: 294.13/75.32 a(a(x1)) -> b(a(b(x1))) 294.13/75.32 a(b(a(x1))) -> b(b(a(b(b(x1))))) 294.13/75.32 a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) 294.13/75.32 a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.32 Matrix Interpretation Processor: dim=3 294.13/75.32 294.13/75.32 max_matrix: 294.13/75.32 [1 1 0] 294.13/75.32 [0 0 1] 294.13/75.32 [0 0 0] 294.13/75.32 interpretation: 294.13/75.32 [1 0 0] 294.13/75.32 [b](x0) = [0 0 0]x0 294.13/75.32 [0 0 0] , 294.13/75.32 294.13/75.32 [1 1 0] [0] 294.13/75.32 [a](x0) = [0 0 1]x0 + [0] 294.13/75.32 [0 0 0] [1] 294.13/75.32 orientation: 294.13/75.32 [1 1 1] [1] [1 1 0] [0] 294.13/75.32 a(a(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = a(b(a(b(a(x1))))) 294.13/75.32 [0 0 0] [1] [0 0 0] [1] 294.13/75.32 294.13/75.32 [1 1 1] [2] [1 1 1] [0] 294.13/75.33 a(a(a(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(b(a(b(a(a(x1))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] [1] 294.13/75.33 294.13/75.33 [1 1 0] [0] [1 0 0] [0] 294.13/75.33 a(a(b(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = a(b(b(a(b(a(b(x1))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] [1] 294.13/75.33 294.13/75.33 [1 1 1] [0] [1 1 0] 294.13/75.33 a(b(a(a(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(a(b(a(b(b(a(x1))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] 294.13/75.33 294.13/75.33 [1 1 1] [3] [1 1 1] [2] 294.13/75.33 a(a(a(a(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] [1] 294.13/75.33 294.13/75.33 [1 1 0] [1] [1 0 0] [0] 294.13/75.33 a(a(a(b(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] [1] 294.13/75.33 294.13/75.33 [1 1 1] [0] [1 1 0] [0] 294.13/75.33 a(a(b(a(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] [1] 294.13/75.33 294.13/75.33 [1 1 0] [0] [1 0 0] [0] 294.13/75.33 a(a(b(b(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] [1] 294.13/75.33 294.13/75.33 [1 1 1] [1] [1 1 1] 294.13/75.33 a(b(a(a(a(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] 294.13/75.33 294.13/75.33 [1 1 0] [0] [1 0 0] 294.13/75.33 a(b(a(b(a(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] 294.13/75.33 294.13/75.33 [1 1 1] [0] [1 1 0] 294.13/75.33 a(b(b(a(a(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] 294.13/75.33 294.13/75.33 [1 1 1] [0] [1 0 0] 294.13/75.33 a(a(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(a(b(x1))) 294.13/75.33 [0 0 0] [1] [0 0 0] 294.13/75.33 294.13/75.33 [1 1 0] [0] [1 0 0] 294.13/75.33 a(b(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(b(a(b(b(x1))))) 294.13/75.33 [0 0 0] [1] [0 0 0] 294.13/75.33 294.13/75.33 [1 1 0] [0] [1 0 0] 294.13/75.33 a(b(b(a(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(b(b(a(b(b(b(x1))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] 294.13/75.33 294.13/75.33 [1 1 0] [0] [1 0 0] 294.13/75.33 a(b(b(b(a(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.33 [0 0 0] [1] [0 0 0] 294.13/75.33 problem: 294.13/75.33 strict: 294.13/75.33 a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) 294.13/75.33 a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) 294.13/75.33 a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.33 a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.33 a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.33 a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.33 weak: 294.13/75.33 a(a(a(x1))) -> a(b(a(b(a(x1))))) 294.13/75.33 a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) 294.13/75.33 a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.33 a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.33 a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.34 a(a(x1)) -> b(a(b(x1))) 294.13/75.34 a(b(a(x1))) -> b(b(a(b(b(x1))))) 294.13/75.34 a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) 294.13/75.34 a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.34 Matrix Interpretation Processor: dim=2 294.13/75.34 294.13/75.34 max_matrix: 294.13/75.34 [1 1] 294.13/75.34 [0 0] 294.13/75.34 interpretation: 294.13/75.34 [1 0] 294.13/75.34 [b](x0) = [0 0]x0, 294.13/75.34 294.13/75.34 [1 1] [0] 294.13/75.34 [a](x0) = [0 0]x0 + [1] 294.13/75.34 orientation: 294.13/75.34 [1 1] [1] [1 0] [0] 294.13/75.34 a(a(b(a(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(b(a(b(a(b(x1))))))) 294.13/75.34 294.13/75.34 [1 1] [1] [1 1] 294.13/75.34 a(b(a(a(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = b(a(b(a(b(b(a(x1))))))) 294.13/75.34 294.13/75.34 [1 1] [2] [1 1] [0] 294.13/75.34 a(a(b(a(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.34 294.13/75.34 [1 1] [1] [1 0] [0] 294.13/75.34 a(a(b(b(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.34 294.13/75.34 [1 1] [0] [1 0] 294.13/75.34 a(b(a(b(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.34 294.13/75.34 [1 1] [1] [1 1] 294.13/75.34 a(b(b(a(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.34 294.13/75.34 [1 1] [2] [1 1] [0] 294.13/75.34 a(a(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(a(b(a(x1))))) 294.13/75.34 294.13/75.34 [1 1] [3] [1 1] [2] 294.13/75.34 a(a(a(a(x1)))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(a(b(a(b(a(a(x1))))))) 294.13/75.34 294.13/75.34 [1 1] [4] [1 1] [4] 294.13/75.34 a(a(a(a(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.34 294.13/75.34 [1 1] [2] [1 0] [2] 294.13/75.34 a(a(a(b(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.34 294.13/75.34 [1 1] [2] [1 1] [2] 294.13/75.34 a(b(a(a(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.34 294.13/75.34 [1 1] [1] [1 0] 294.13/75.34 a(a(x1)) = [0 0]x1 + [1] >= [0 0]x1 = b(a(b(x1))) 294.13/75.34 294.13/75.34 [1 1] [0] [1 0] 294.13/75.34 a(b(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(a(b(b(x1))))) 294.13/75.34 294.13/75.34 [1 1] [0] [1 0] 294.13/75.34 a(b(b(a(x1)))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(b(a(b(b(b(x1))))))) 294.13/75.34 294.13/75.34 [1 1] [0] [1 0] 294.13/75.34 a(b(b(b(a(x1))))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.34 problem: 294.13/75.34 strict: 294.13/75.34 a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.34 weak: 294.13/75.34 a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) 294.13/75.34 a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) 294.13/75.34 a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.34 a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.34 a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.34 a(a(a(x1))) -> a(b(a(b(a(x1))))) 294.13/75.34 a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) 294.13/75.34 a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.34 a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.34 a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.34 a(a(x1)) -> b(a(b(x1))) 294.13/75.34 a(b(a(x1))) -> b(b(a(b(b(x1))))) 294.13/75.34 a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) 294.13/75.34 a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.34 Matrix Interpretation Processor: dim=3 294.13/75.34 294.13/75.34 max_matrix: 294.13/75.34 [1 1 1] 294.13/75.34 [0 0 2] 294.13/75.34 [0 0 0] 294.13/75.34 interpretation: 294.13/75.34 [1 0 0] 294.13/75.34 [b](x0) = [0 0 1]x0 294.13/75.34 [0 0 0] , 294.13/75.34 294.13/75.34 [1 1 1] [0] 294.13/75.34 [a](x0) = [0 0 2]x0 + [1] 294.13/75.34 [0 0 0] [1] 294.13/75.34 orientation: 294.13/75.34 [1 1 1] [2] [1 0 1] [0] 294.13/75.35 a(b(a(b(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [0] 294.13/75.35 294.13/75.35 [1 1 1] [3] [1 0 1] [1] 294.13/75.35 a(a(b(a(x1)))) = [0 0 0]x1 + [3] >= [0 0 0]x1 + [1] = a(b(b(a(b(a(b(x1))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [1] 294.13/75.35 294.13/75.35 [1 1 3] [3] [1 1 1] [1] 294.13/75.35 a(b(a(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(a(b(a(b(b(a(x1))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [0] 294.13/75.35 294.13/75.35 [1 1 3] [5] [1 1 1] [4] 294.13/75.35 a(a(b(a(a(x1))))) = [0 0 0]x1 + [3] >= [0 0 0]x1 + [1] = a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [1] 294.13/75.35 294.13/75.35 [1 1 1] [2] [1 0 0] [1] 294.13/75.35 a(a(b(b(a(x1))))) = [0 0 0]x1 + [3] >= [0 0 0]x1 + [1] = a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [1] 294.13/75.35 294.13/75.35 [1 1 3] [2] [1 1 1] [1] 294.13/75.35 a(b(b(a(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [0] 294.13/75.35 294.13/75.35 [1 1 3] [6] [1 1 1] [2] 294.13/75.35 a(a(a(x1))) = [0 0 0]x1 + [3] >= [0 0 0]x1 + [1] = a(b(a(b(a(x1))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [1] 294.13/75.35 294.13/75.35 [1 1 3] [10] [1 1 3] [6] 294.13/75.35 a(a(a(a(x1)))) = [0 0 0]x1 + [3 ] >= [0 0 0]x1 + [3] = a(a(b(a(b(a(a(x1))))))) 294.13/75.35 [0 0 0] [1 ] [0 0 0] [1] 294.13/75.35 294.13/75.35 [1 1 3] [14] [1 1 3] [14] 294.13/75.35 a(a(a(a(a(x1))))) = [0 0 0]x1 + [3 ] >= [0 0 0]x1 + [3 ] = a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.35 [0 0 0] [1 ] [0 0 0] [1 ] 294.13/75.35 294.13/75.35 [1 1 1] [7] [1 0 1] [5] 294.13/75.35 a(a(a(b(a(x1))))) = [0 0 0]x1 + [3] >= [0 0 0]x1 + [3] = a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [1] 294.13/75.35 294.13/75.35 [1 1 3] [7] [1 1 3] [5] 294.13/75.35 a(b(a(a(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] [0] 294.13/75.35 294.13/75.35 [1 1 3] [2] [1 0 1] [0] 294.13/75.35 a(a(x1)) = [0 0 0]x1 + [3] >= [0 0 0]x1 + [1] = b(a(b(x1))) 294.13/75.35 [0 0 0] [1] [0 0 0] [0] 294.13/75.35 294.13/75.35 [1 1 1] [1] [1 0 0] 294.13/75.35 a(b(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(a(b(b(x1))))) 294.13/75.35 [0 0 0] [1] [0 0 0] 294.13/75.35 294.13/75.35 [1 1 1] [0] [1 0 0] 294.13/75.35 a(b(b(a(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(b(a(b(b(b(x1))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] 294.13/75.35 294.13/75.35 [1 1 1] [0] [1 0 0] 294.13/75.35 a(b(b(b(a(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.35 [0 0 0] [1] [0 0 0] 294.13/75.35 problem: 294.13/75.35 strict: 294.13/75.35 294.13/75.35 weak: 294.13/75.35 a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) 294.13/75.35 a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) 294.13/75.35 a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) 294.13/75.35 a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) 294.13/75.35 a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) 294.13/75.35 a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) 294.13/75.35 a(a(a(x1))) -> a(b(a(b(a(x1))))) 294.13/75.35 a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) 294.13/75.35 a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) 294.13/75.35 a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) 294.13/75.35 a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) 294.13/75.35 a(a(x1)) -> b(a(b(x1))) 294.13/75.35 a(b(a(x1))) -> b(b(a(b(b(x1))))) 294.13/75.35 a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) 294.13/75.35 a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) 294.13/75.35 Qed 294.13/75.35 EOF