YES(?,O(n^1)) 4.43/1.39 YES(?,O(n^1)) 4.43/1.39 4.43/1.39 Problem: 4.43/1.39 b(a(b(x1))) -> a(x1) 4.43/1.39 a(a(a(x1))) -> b(x1) 4.43/1.39 b(b(x1)) -> b(a(b(x1))) 4.43/1.39 4.43/1.39 Proof: 4.43/1.39 Complexity Transformation Processor: 4.43/1.39 strict: 4.43/1.39 b(a(b(x1))) -> a(x1) 4.43/1.39 a(a(a(x1))) -> b(x1) 4.43/1.39 b(b(x1)) -> b(a(b(x1))) 4.43/1.39 weak: 4.43/1.39 4.43/1.39 Matrix Interpretation Processor: dim=1 4.43/1.39 4.43/1.39 max_matrix: 4.43/1.39 1 4.43/1.39 interpretation: 4.43/1.39 [a](x0) = x0 + 45, 4.43/1.39 4.43/1.39 [b](x0) = x0 + 33 4.43/1.39 orientation: 4.43/1.39 b(a(b(x1))) = x1 + 111 >= x1 + 45 = a(x1) 4.43/1.39 4.43/1.39 a(a(a(x1))) = x1 + 135 >= x1 + 33 = b(x1) 4.43/1.39 4.43/1.39 b(b(x1)) = x1 + 66 >= x1 + 111 = b(a(b(x1))) 4.43/1.39 problem: 4.43/1.39 strict: 4.43/1.39 b(b(x1)) -> b(a(b(x1))) 4.43/1.39 weak: 4.43/1.39 b(a(b(x1))) -> a(x1) 4.43/1.39 a(a(a(x1))) -> b(x1) 4.43/1.39 Arctic Interpretation Processor: 4.43/1.39 dimension: 2 4.43/1.39 interpretation: 4.43/1.39 [2 0 ] 4.43/1.39 [a](x0) = [1 -&]x0, 4.43/1.39 4.43/1.39 [0 1] 4.43/1.39 [b](x0) = [2 3]x0 4.43/1.39 orientation: 4.43/1.39 [3 4] [2 3] 4.43/1.39 b(b(x1)) = [5 6]x1 >= [4 5]x1 = b(a(b(x1))) 4.43/1.39 4.43/1.39 [2 3] [2 0 ] 4.43/1.39 b(a(b(x1))) = [4 5]x1 >= [1 -&]x1 = a(x1) 4.43/1.39 4.43/1.39 [6 4] [0 1] 4.43/1.39 a(a(a(x1))) = [5 3]x1 >= [2 3]x1 = b(x1) 4.43/1.39 problem: 4.43/1.39 strict: 4.43/1.39 4.43/1.39 weak: 4.43/1.39 b(b(x1)) -> b(a(b(x1))) 4.43/1.39 b(a(b(x1))) -> a(x1) 4.43/1.39 a(a(a(x1))) -> b(x1) 4.43/1.39 Qed 4.43/1.39 EOF