YES(?,O(n^1)) 6.83/1.96 YES(?,O(n^1)) 6.83/1.96 6.83/1.96 Problem: 6.83/1.96 b(b(b(x1))) -> a(b(x1)) 6.83/1.96 a(a(x1)) -> a(b(a(x1))) 6.83/1.96 a(a(a(x1))) -> a(b(b(x1))) 6.83/1.96 6.83/1.96 Proof: 6.83/1.96 Complexity Transformation Processor: 6.83/1.96 strict: 6.83/1.96 b(b(b(x1))) -> a(b(x1)) 6.83/1.96 a(a(x1)) -> a(b(a(x1))) 6.83/1.96 a(a(a(x1))) -> a(b(b(x1))) 6.83/1.96 weak: 6.83/1.96 6.83/1.96 Matrix Interpretation Processor: dim=1 6.83/1.96 6.83/1.96 max_matrix: 6.83/1.96 1 6.83/1.96 interpretation: 6.83/1.96 [a](x0) = x0 + 132, 6.83/1.96 6.83/1.96 [b](x0) = x0 + 2 6.83/1.96 orientation: 6.83/1.96 b(b(b(x1))) = x1 + 6 >= x1 + 134 = a(b(x1)) 6.83/1.96 6.83/1.96 a(a(x1)) = x1 + 264 >= x1 + 266 = a(b(a(x1))) 6.83/1.96 6.83/1.96 a(a(a(x1))) = x1 + 396 >= x1 + 136 = a(b(b(x1))) 6.83/1.96 problem: 6.83/1.96 strict: 6.83/1.96 b(b(b(x1))) -> a(b(x1)) 6.83/1.96 a(a(x1)) -> a(b(a(x1))) 6.83/1.96 weak: 6.83/1.96 a(a(a(x1))) -> a(b(b(x1))) 6.83/1.96 Matrix Interpretation Processor: dim=1 6.83/1.96 6.83/1.96 max_matrix: 6.83/1.96 1 6.83/1.96 interpretation: 6.83/1.96 [a](x0) = x0 + 128, 6.83/1.96 6.83/1.96 [b](x0) = x0 + 128 6.83/1.96 orientation: 6.83/1.96 b(b(b(x1))) = x1 + 384 >= x1 + 256 = a(b(x1)) 6.83/1.96 6.83/1.96 a(a(x1)) = x1 + 256 >= x1 + 384 = a(b(a(x1))) 6.83/1.96 6.83/1.96 a(a(a(x1))) = x1 + 384 >= x1 + 384 = a(b(b(x1))) 6.83/1.96 problem: 6.83/1.96 strict: 6.83/1.96 a(a(x1)) -> a(b(a(x1))) 6.83/1.96 weak: 6.83/1.96 b(b(b(x1))) -> a(b(x1)) 6.83/1.96 a(a(a(x1))) -> a(b(b(x1))) 6.83/1.96 Arctic Interpretation Processor: 6.83/1.96 dimension: 2 6.83/1.96 interpretation: 6.83/1.96 [0 1] 6.83/1.96 [a](x0) = [1 2]x0, 6.83/1.96 6.83/1.96 [1 0 ] 6.83/1.96 [b](x0) = [0 -&]x0 6.83/1.96 orientation: 6.83/1.96 [2 3] [1 2] 6.83/1.96 a(a(x1)) = [3 4]x1 >= [2 3]x1 = a(b(a(x1))) 6.83/1.96 6.83/1.96 [3 2] [1 0] 6.83/1.96 b(b(b(x1))) = [2 1]x1 >= [2 1]x1 = a(b(x1)) 6.83/1.96 6.83/1.96 [4 5] [2 1] 6.83/1.96 a(a(a(x1))) = [5 6]x1 >= [3 2]x1 = a(b(b(x1))) 6.83/1.96 problem: 6.83/1.96 strict: 6.83/1.96 6.83/1.96 weak: 6.83/1.96 a(a(x1)) -> a(b(a(x1))) 6.83/1.96 b(b(b(x1))) -> a(b(x1)) 6.83/1.96 a(a(a(x1))) -> a(b(b(x1))) 6.83/1.96 Qed 6.83/1.96 EOF