YES(?,O(n^1)) 5.62/1.63 YES(?,O(n^1)) 5.62/1.63 5.62/1.63 Problem: 5.62/1.63 a(a(a(x1))) -> a(c(a(a(x1)))) 5.62/1.63 c(c(c(x1))) -> a(x1) 5.62/1.63 a(x1) -> x1 5.62/1.63 5.62/1.63 Proof: 5.62/1.63 Complexity Transformation Processor: 5.62/1.63 strict: 5.62/1.63 a(a(a(x1))) -> a(c(a(a(x1)))) 5.62/1.63 c(c(c(x1))) -> a(x1) 5.62/1.63 a(x1) -> x1 5.62/1.63 weak: 5.62/1.63 5.62/1.63 Matrix Interpretation Processor: dim=1 5.62/1.63 5.62/1.63 max_matrix: 5.62/1.63 1 5.62/1.63 interpretation: 5.62/1.63 [c](x0) = x0 + 34, 5.62/1.63 5.62/1.63 [a](x0) = x0 + 138 5.62/1.63 orientation: 5.62/1.63 a(a(a(x1))) = x1 + 414 >= x1 + 448 = a(c(a(a(x1)))) 5.62/1.63 5.62/1.63 c(c(c(x1))) = x1 + 102 >= x1 + 138 = a(x1) 5.62/1.63 5.62/1.63 a(x1) = x1 + 138 >= x1 = x1 5.62/1.63 problem: 5.62/1.63 strict: 5.62/1.63 a(a(a(x1))) -> a(c(a(a(x1)))) 5.62/1.63 c(c(c(x1))) -> a(x1) 5.62/1.63 weak: 5.62/1.63 a(x1) -> x1 5.62/1.63 Matrix Interpretation Processor: dim=1 5.62/1.63 5.62/1.63 max_matrix: 5.62/1.63 1 5.62/1.63 interpretation: 5.62/1.63 [c](x0) = x0 + 34, 5.62/1.63 5.62/1.63 [a](x0) = x0 + 16 5.62/1.63 orientation: 5.62/1.63 a(a(a(x1))) = x1 + 48 >= x1 + 82 = a(c(a(a(x1)))) 5.62/1.63 5.62/1.63 c(c(c(x1))) = x1 + 102 >= x1 + 16 = a(x1) 5.62/1.63 5.62/1.63 a(x1) = x1 + 16 >= x1 = x1 5.62/1.63 problem: 5.62/1.63 strict: 5.62/1.63 a(a(a(x1))) -> a(c(a(a(x1)))) 5.62/1.63 weak: 5.62/1.63 c(c(c(x1))) -> a(x1) 5.62/1.63 a(x1) -> x1 5.62/1.63 Arctic Interpretation Processor: 5.62/1.63 dimension: 2 5.62/1.63 interpretation: 5.62/1.63 [2 0 ] 5.62/1.63 [c](x0) = [1 -&]x0, 5.62/1.63 5.62/1.63 [0 1] 5.62/1.63 [a](x0) = [0 3]x0 5.62/1.63 orientation: 5.62/1.63 [4 7] [3 6] 5.62/1.63 a(a(a(x1))) = [6 9]x1 >= [5 8]x1 = a(c(a(a(x1)))) 5.62/1.63 5.62/1.63 [6 4] [0 1] 5.62/1.63 c(c(c(x1))) = [5 3]x1 >= [0 3]x1 = a(x1) 5.62/1.63 5.62/1.63 [0 1] 5.62/1.63 a(x1) = [0 3]x1 >= x1 = x1 5.62/1.63 problem: 5.62/1.63 strict: 5.62/1.63 5.62/1.63 weak: 5.62/1.63 a(a(a(x1))) -> a(c(a(a(x1)))) 5.62/1.63 c(c(c(x1))) -> a(x1) 5.62/1.63 a(x1) -> x1 5.62/1.63 Qed 5.62/1.63 EOF