YES(?,O(n^1)) 5.46/1.73 YES(?,O(n^1)) 5.46/1.74 5.46/1.74 Problem: 5.46/1.74 a(b(a(x1))) -> a(a(b(b(a(a(x1)))))) 5.46/1.74 b(a(a(b(x1)))) -> b(a(b(x1))) 5.46/1.74 5.46/1.74 Proof: 5.46/1.74 Complexity Transformation Processor: 5.46/1.74 strict: 5.46/1.74 a(b(a(x1))) -> a(a(b(b(a(a(x1)))))) 5.46/1.74 b(a(a(b(x1)))) -> b(a(b(x1))) 5.46/1.74 weak: 5.46/1.74 5.46/1.74 Matrix Interpretation Processor: dim=1 5.46/1.74 5.46/1.74 max_matrix: 5.46/1.74 1 5.46/1.74 interpretation: 5.46/1.74 [b](x0) = x0 + 2, 5.46/1.74 5.46/1.74 [a](x0) = x0 + 17 5.46/1.74 orientation: 5.46/1.74 a(b(a(x1))) = x1 + 36 >= x1 + 72 = a(a(b(b(a(a(x1)))))) 5.46/1.74 5.46/1.74 b(a(a(b(x1)))) = x1 + 38 >= x1 + 21 = b(a(b(x1))) 5.46/1.74 problem: 5.46/1.74 strict: 5.46/1.74 a(b(a(x1))) -> a(a(b(b(a(a(x1)))))) 5.46/1.74 weak: 5.46/1.74 b(a(a(b(x1)))) -> b(a(b(x1))) 5.46/1.74 Matrix Interpretation Processor: dim=4 5.46/1.74 5.46/1.74 max_matrix: 5.46/1.74 [1 1 0 0] 5.46/1.74 [0 0 1 0] 5.46/1.74 [0 0 0 0] 5.46/1.74 [0 0 0 0] 5.46/1.74 interpretation: 5.46/1.74 [1 0 0 0] 5.46/1.74 [0 0 1 0] 5.46/1.74 [b](x0) = [0 0 0 0]x0 5.46/1.74 [0 0 0 0] , 5.46/1.74 5.46/1.74 [1 1 0 0] [0] 5.46/1.74 [0 0 0 0] [0] 5.46/1.74 [a](x0) = [0 0 0 0]x0 + [1] 5.46/1.74 [0 0 0 0] [0] 5.46/1.74 orientation: 5.46/1.74 [1 1 0 0] [1] [1 1 0 0] [0] 5.46/1.74 [0 0 0 0] [0] [0 0 0 0] [0] 5.46/1.74 a(b(a(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = a(a(b(b(a(a(x1)))))) 5.46/1.74 [0 0 0 0] [0] [0 0 0 0] [0] 5.46/1.74 5.46/1.74 [1 0 1 0] [0] [1 0 1 0] [0] 5.46/1.74 [0 0 0 0] [1] [0 0 0 0] [1] 5.46/1.74 b(a(a(b(x1)))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = b(a(b(x1))) 5.46/1.74 [0 0 0 0] [0] [0 0 0 0] [0] 5.46/1.74 problem: 5.46/1.74 strict: 5.46/1.74 5.46/1.74 weak: 5.46/1.74 a(b(a(x1))) -> a(a(b(b(a(a(x1)))))) 5.46/1.74 b(a(a(b(x1)))) -> b(a(b(x1))) 5.46/1.74 Qed 5.46/1.74 EOF