YES(?,O(n^1)) 18.24/4.80 YES(?,O(n^1)) 18.24/4.81 18.24/4.81 Problem: 18.24/4.81 a(a(x1)) -> b(c(x1)) 18.24/4.81 b(b(x1)) -> c(d(x1)) 18.24/4.81 c(c(x1)) -> d(d(d(x1))) 18.24/4.81 d(c(x1)) -> b(f(x1)) 18.24/4.81 d(d(d(x1))) -> a(c(x1)) 18.24/4.81 f(f(x1)) -> f(b(x1)) 18.24/4.81 18.24/4.81 Proof: 18.24/4.81 Complexity Transformation Processor: 18.24/4.81 strict: 18.24/4.81 a(a(x1)) -> b(c(x1)) 18.24/4.81 b(b(x1)) -> c(d(x1)) 18.24/4.81 c(c(x1)) -> d(d(d(x1))) 18.24/4.81 d(c(x1)) -> b(f(x1)) 18.24/4.81 d(d(d(x1))) -> a(c(x1)) 18.24/4.81 f(f(x1)) -> f(b(x1)) 18.24/4.81 weak: 18.24/4.81 18.24/4.81 Matrix Interpretation Processor: dim=1 18.24/4.81 18.24/4.81 max_matrix: 18.24/4.81 1 18.24/4.81 interpretation: 18.24/4.81 [f](x0) = x0 + 3, 18.24/4.81 18.24/4.81 [d](x0) = x0, 18.24/4.81 18.24/4.81 [b](x0) = x0 + 89, 18.24/4.81 18.24/4.81 [c](x0) = x0 + 65, 18.24/4.81 18.24/4.81 [a](x0) = x0 + 8 18.24/4.81 orientation: 18.24/4.81 a(a(x1)) = x1 + 16 >= x1 + 154 = b(c(x1)) 18.24/4.81 18.24/4.81 b(b(x1)) = x1 + 178 >= x1 + 65 = c(d(x1)) 18.24/4.81 18.24/4.81 c(c(x1)) = x1 + 130 >= x1 = d(d(d(x1))) 18.24/4.81 18.24/4.81 d(c(x1)) = x1 + 65 >= x1 + 92 = b(f(x1)) 18.24/4.81 18.24/4.81 d(d(d(x1))) = x1 >= x1 + 73 = a(c(x1)) 18.24/4.81 18.24/4.81 f(f(x1)) = x1 + 6 >= x1 + 92 = f(b(x1)) 18.24/4.81 problem: 18.24/4.81 strict: 18.24/4.81 a(a(x1)) -> b(c(x1)) 18.24/4.81 d(c(x1)) -> b(f(x1)) 18.24/4.81 d(d(d(x1))) -> a(c(x1)) 18.24/4.81 f(f(x1)) -> f(b(x1)) 18.24/4.81 weak: 18.24/4.81 b(b(x1)) -> c(d(x1)) 18.24/4.81 c(c(x1)) -> d(d(d(x1))) 18.24/4.81 Matrix Interpretation Processor: dim=1 18.24/4.81 18.24/4.81 max_matrix: 18.24/4.81 1 18.24/4.81 interpretation: 18.24/4.81 [f](x0) = x0, 18.24/4.81 18.24/4.81 [d](x0) = x0, 18.24/4.81 18.24/4.81 [b](x0) = x0, 18.24/4.81 18.24/4.81 [c](x0) = x0, 18.24/4.81 18.24/4.81 [a](x0) = x0 + 4 18.24/4.81 orientation: 18.24/4.81 a(a(x1)) = x1 + 8 >= x1 = b(c(x1)) 18.24/4.81 18.24/4.81 d(c(x1)) = x1 >= x1 = b(f(x1)) 18.24/4.81 18.24/4.81 d(d(d(x1))) = x1 >= x1 + 4 = a(c(x1)) 18.24/4.81 18.24/4.81 f(f(x1)) = x1 >= x1 = f(b(x1)) 18.24/4.81 18.24/4.81 b(b(x1)) = x1 >= x1 = c(d(x1)) 18.24/4.81 18.24/4.81 c(c(x1)) = x1 >= x1 = d(d(d(x1))) 18.24/4.81 problem: 18.24/4.81 strict: 18.24/4.81 d(c(x1)) -> b(f(x1)) 18.24/4.81 d(d(d(x1))) -> a(c(x1)) 18.24/4.81 f(f(x1)) -> f(b(x1)) 18.24/4.81 weak: 18.24/4.81 a(a(x1)) -> b(c(x1)) 18.24/4.81 b(b(x1)) -> c(d(x1)) 18.24/4.81 c(c(x1)) -> d(d(d(x1))) 18.24/4.81 Matrix Interpretation Processor: dim=1 18.24/4.81 18.24/4.81 max_matrix: 18.24/4.81 1 18.24/4.81 interpretation: 18.24/4.81 [f](x0) = x0 + 4, 18.24/4.81 18.24/4.81 [d](x0) = x0 + 32, 18.24/4.81 18.24/4.81 [b](x0) = x0 + 68, 18.24/4.81 18.24/4.81 [c](x0) = x0 + 60, 18.24/4.81 18.24/4.81 [a](x0) = x0 + 64 18.24/4.81 orientation: 18.24/4.81 d(c(x1)) = x1 + 92 >= x1 + 72 = b(f(x1)) 18.24/4.81 18.24/4.81 d(d(d(x1))) = x1 + 96 >= x1 + 124 = a(c(x1)) 18.24/4.81 18.24/4.81 f(f(x1)) = x1 + 8 >= x1 + 72 = f(b(x1)) 18.24/4.81 18.24/4.81 a(a(x1)) = x1 + 128 >= x1 + 128 = b(c(x1)) 18.24/4.81 18.24/4.81 b(b(x1)) = x1 + 136 >= x1 + 92 = c(d(x1)) 18.24/4.81 18.24/4.81 c(c(x1)) = x1 + 120 >= x1 + 96 = d(d(d(x1))) 18.24/4.81 problem: 18.24/4.81 strict: 18.24/4.81 d(d(d(x1))) -> a(c(x1)) 18.24/4.81 f(f(x1)) -> f(b(x1)) 18.24/4.81 weak: 18.24/4.81 d(c(x1)) -> b(f(x1)) 18.24/4.81 a(a(x1)) -> b(c(x1)) 18.24/4.81 b(b(x1)) -> c(d(x1)) 18.24/4.81 c(c(x1)) -> d(d(d(x1))) 18.24/4.81 Matrix Interpretation Processor: dim=1 18.24/4.81 18.24/4.81 max_matrix: 18.24/4.81 1 18.24/4.81 interpretation: 18.24/4.81 [f](x0) = x0, 18.24/4.81 18.24/4.81 [d](x0) = x0 + 51, 18.24/4.81 18.24/4.81 [b](x0) = x0 + 65, 18.24/4.81 18.24/4.81 [c](x0) = x0 + 78, 18.24/4.81 18.24/4.81 [a](x0) = x0 + 74 18.24/4.81 orientation: 18.24/4.81 d(d(d(x1))) = x1 + 153 >= x1 + 152 = a(c(x1)) 18.24/4.81 18.24/4.81 f(f(x1)) = x1 >= x1 + 65 = f(b(x1)) 18.24/4.81 18.24/4.81 d(c(x1)) = x1 + 129 >= x1 + 65 = b(f(x1)) 18.24/4.81 18.24/4.81 a(a(x1)) = x1 + 148 >= x1 + 143 = b(c(x1)) 18.24/4.81 18.24/4.81 b(b(x1)) = x1 + 130 >= x1 + 129 = c(d(x1)) 18.24/4.81 18.24/4.81 c(c(x1)) = x1 + 156 >= x1 + 153 = d(d(d(x1))) 18.24/4.81 problem: 18.24/4.81 strict: 18.24/4.81 f(f(x1)) -> f(b(x1)) 18.24/4.81 weak: 18.24/4.81 d(d(d(x1))) -> a(c(x1)) 18.24/4.81 d(c(x1)) -> b(f(x1)) 18.24/4.81 a(a(x1)) -> b(c(x1)) 18.24/4.81 b(b(x1)) -> c(d(x1)) 18.24/4.81 c(c(x1)) -> d(d(d(x1))) 18.24/4.81 Arctic Interpretation Processor: 18.24/4.81 dimension: 2 18.24/4.81 interpretation: 18.24/4.81 [0 0] 18.24/4.81 [f](x0) = [7 7]x0, 18.24/4.81 18.24/4.81 [4 0 ] 18.24/4.81 [d](x0) = [-& -&]x0, 18.24/4.81 18.24/4.81 [6 0 ] 18.24/4.81 [b](x0) = [-& -&]x0, 18.24/4.81 18.24/4.81 [6 1 ] 18.24/4.81 [c](x0) = [-& 7 ]x0, 18.24/4.81 18.24/4.81 [6 1 ] 18.24/4.81 [a](x0) = [-& -&]x0 18.24/4.81 orientation: 18.24/4.81 [7 7 ] [6 0 ] 18.24/4.81 f(f(x1)) = [14 14]x1 >= [13 7 ]x1 = f(b(x1)) 18.24/4.81 18.24/4.81 [12 8 ] [12 8 ] 18.24/4.81 d(d(d(x1))) = [-& -&]x1 >= [-& -&]x1 = a(c(x1)) 18.24/4.81 18.24/4.81 [10 7 ] [7 7 ] 18.24/4.81 d(c(x1)) = [-& -&]x1 >= [-& -&]x1 = b(f(x1)) 18.24/4.81 18.24/4.81 [12 7 ] [12 7 ] 18.24/4.81 a(a(x1)) = [-& -&]x1 >= [-& -&]x1 = b(c(x1)) 18.24/4.81 18.24/4.81 [12 6 ] [10 6 ] 18.24/4.81 b(b(x1)) = [-& -&]x1 >= [-& -&]x1 = c(d(x1)) 18.24/4.81 18.24/4.81 [12 8 ] [12 8 ] 18.24/4.81 c(c(x1)) = [-& 14]x1 >= [-& -&]x1 = d(d(d(x1))) 18.24/4.81 problem: 18.24/4.81 strict: 18.24/4.81 18.24/4.81 weak: 18.24/4.81 f(f(x1)) -> f(b(x1)) 18.24/4.81 d(d(d(x1))) -> a(c(x1)) 18.24/4.81 d(c(x1)) -> b(f(x1)) 18.24/4.81 a(a(x1)) -> b(c(x1)) 18.24/4.81 b(b(x1)) -> c(d(x1)) 18.24/4.81 c(c(x1)) -> d(d(d(x1))) 18.24/4.81 Qed 18.24/4.81 EOF