YES(?,O(n^1)) 14.30/3.87 YES(?,O(n^1)) 14.30/3.88 14.30/3.88 Problem: 14.30/3.88 a(b(b(x1))) -> a(x1) 14.30/3.88 a(a(x1)) -> b(b(b(x1))) 14.30/3.88 b(b(a(x1))) -> a(b(a(x1))) 14.30/3.88 14.30/3.88 Proof: 14.30/3.88 Complexity Transformation Processor: 14.30/3.88 strict: 14.30/3.88 a(b(b(x1))) -> a(x1) 14.30/3.88 a(a(x1)) -> b(b(b(x1))) 14.30/3.88 b(b(a(x1))) -> a(b(a(x1))) 14.30/3.88 weak: 14.30/3.88 14.30/3.88 Matrix Interpretation Processor: dim=1 14.30/3.88 14.30/3.88 max_matrix: 14.30/3.88 1 14.30/3.88 interpretation: 14.30/3.88 [a](x0) = x0 + 16, 14.30/3.88 14.30/3.88 [b](x0) = x0 + 128 14.30/3.88 orientation: 14.30/3.88 a(b(b(x1))) = x1 + 272 >= x1 + 16 = a(x1) 14.30/3.88 14.30/3.88 a(a(x1)) = x1 + 32 >= x1 + 384 = b(b(b(x1))) 14.30/3.88 14.30/3.88 b(b(a(x1))) = x1 + 272 >= x1 + 160 = a(b(a(x1))) 14.30/3.88 problem: 14.30/3.88 strict: 14.30/3.88 a(a(x1)) -> b(b(b(x1))) 14.30/3.88 weak: 14.30/3.88 a(b(b(x1))) -> a(x1) 14.30/3.88 b(b(a(x1))) -> a(b(a(x1))) 14.30/3.88 Arctic Interpretation Processor: 14.30/3.88 dimension: 3 14.30/3.88 interpretation: 14.30/3.88 [0 0 -&] 14.30/3.88 [a](x0) = [2 2 0 ]x0 14.30/3.88 [0 0 -&] , 14.30/3.88 14.30/3.88 [0 -& -&] 14.30/3.88 [b](x0) = [-& -& 0 ]x0 14.30/3.88 [-& 0 -&] 14.30/3.88 orientation: 14.30/3.88 [2 2 0] [0 -& -&] 14.30/3.88 a(a(x1)) = [4 4 2]x1 >= [-& -& 0 ]x1 = b(b(b(x1))) 14.30/3.88 [2 2 0] [-& 0 -&] 14.30/3.88 14.30/3.88 [0 0 -&] [0 0 -&] 14.30/3.88 a(b(b(x1))) = [2 2 0 ]x1 >= [2 2 0 ]x1 = a(x1) 14.30/3.88 [0 0 -&] [0 0 -&] 14.30/3.88 14.30/3.88 [0 0 -&] [0 0 -&] 14.30/3.88 b(b(a(x1))) = [2 2 0 ]x1 >= [2 2 0 ]x1 = a(b(a(x1))) 14.30/3.88 [0 0 -&] [0 0 -&] 14.30/3.88 problem: 14.30/3.88 strict: 14.30/3.88 14.30/3.88 weak: 14.30/3.88 a(a(x1)) -> b(b(b(x1))) 14.30/3.88 a(b(b(x1))) -> a(x1) 14.30/3.88 b(b(a(x1))) -> a(b(a(x1))) 14.30/3.88 Qed 14.30/3.88 EOF