YES(?,O(n^1)) 0.16/0.51 YES(?,O(n^1)) 0.16/0.51 0.16/0.51 Problem: 0.16/0.51 a(a(x1)) -> b(c(x1)) 0.16/0.51 b(b(x1)) -> c(d(x1)) 0.16/0.51 b(x1) -> a(x1) 0.16/0.51 c(c(x1)) -> d(f(x1)) 0.16/0.51 d(d(x1)) -> f(f(f(x1))) 0.16/0.51 d(x1) -> b(x1) 0.16/0.51 f(f(x1)) -> g(a(x1)) 0.16/0.51 g(g(x1)) -> a(x1) 0.16/0.51 0.16/0.51 Proof: 0.16/0.51 Complexity Transformation Processor: 0.16/0.51 strict: 0.16/0.51 a(a(x1)) -> b(c(x1)) 0.16/0.51 b(b(x1)) -> c(d(x1)) 0.16/0.51 b(x1) -> a(x1) 0.16/0.51 c(c(x1)) -> d(f(x1)) 0.16/0.51 d(d(x1)) -> f(f(f(x1))) 0.16/0.51 d(x1) -> b(x1) 0.16/0.51 f(f(x1)) -> g(a(x1)) 0.16/0.51 g(g(x1)) -> a(x1) 0.16/0.51 weak: 0.16/0.51 0.16/0.51 Matrix Interpretation Processor: dim=1 0.16/0.51 0.16/0.51 max_matrix: 0.16/0.51 1 0.16/0.51 interpretation: 0.16/0.51 [g](x0) = x0, 0.16/0.51 0.16/0.51 [f](x0) = x0 + 32, 0.16/0.51 0.16/0.51 [d](x0) = x0 + 143, 0.16/0.51 0.16/0.51 [b](x0) = x0 + 2, 0.16/0.51 0.16/0.51 [c](x0) = x0 + 168, 0.16/0.51 0.16/0.51 [a](x0) = x0 + 192 0.16/0.51 orientation: 0.16/0.51 a(a(x1)) = x1 + 384 >= x1 + 170 = b(c(x1)) 0.16/0.51 0.16/0.51 b(b(x1)) = x1 + 4 >= x1 + 311 = c(d(x1)) 0.16/0.51 0.16/0.51 b(x1) = x1 + 2 >= x1 + 192 = a(x1) 0.16/0.51 0.16/0.51 c(c(x1)) = x1 + 336 >= x1 + 175 = d(f(x1)) 0.16/0.51 0.16/0.51 d(d(x1)) = x1 + 286 >= x1 + 96 = f(f(f(x1))) 0.16/0.51 0.16/0.51 d(x1) = x1 + 143 >= x1 + 2 = b(x1) 0.16/0.51 0.16/0.51 f(f(x1)) = x1 + 64 >= x1 + 192 = g(a(x1)) 0.16/0.51 0.16/0.51 g(g(x1)) = x1 >= x1 + 192 = a(x1) 0.16/0.51 problem: 0.16/0.51 strict: 0.16/0.51 b(b(x1)) -> c(d(x1)) 0.16/0.51 b(x1) -> a(x1) 0.16/0.51 f(f(x1)) -> g(a(x1)) 0.16/0.51 g(g(x1)) -> a(x1) 0.16/0.51 weak: 0.16/0.51 a(a(x1)) -> b(c(x1)) 0.16/0.51 c(c(x1)) -> d(f(x1)) 0.16/0.51 d(d(x1)) -> f(f(f(x1))) 0.16/0.51 d(x1) -> b(x1) 0.16/0.51 Matrix Interpretation Processor: dim=1 0.16/0.51 0.16/0.51 max_matrix: 0.16/0.51 1 0.16/0.51 interpretation: 0.16/0.51 [g](x0) = x0 + 68, 0.16/0.51 0.16/0.51 [f](x0) = x0 + 25, 0.16/0.51 0.16/0.51 [d](x0) = x0 + 129, 0.16/0.51 0.16/0.51 [b](x0) = x0 + 129, 0.16/0.51 0.16/0.51 [c](x0) = x0 + 129, 0.16/0.51 0.16/0.51 [a](x0) = x0 + 129 0.16/0.51 orientation: 0.16/0.51 b(b(x1)) = x1 + 258 >= x1 + 258 = c(d(x1)) 0.16/0.51 0.16/0.51 b(x1) = x1 + 129 >= x1 + 129 = a(x1) 0.16/0.51 0.16/0.51 f(f(x1)) = x1 + 50 >= x1 + 197 = g(a(x1)) 0.16/0.51 0.16/0.51 g(g(x1)) = x1 + 136 >= x1 + 129 = a(x1) 0.16/0.51 0.16/0.51 a(a(x1)) = x1 + 258 >= x1 + 258 = b(c(x1)) 0.16/0.51 0.16/0.51 c(c(x1)) = x1 + 258 >= x1 + 154 = d(f(x1)) 0.16/0.51 0.16/0.51 d(d(x1)) = x1 + 258 >= x1 + 75 = f(f(f(x1))) 0.16/0.51 0.16/0.51 d(x1) = x1 + 129 >= x1 + 129 = b(x1) 0.16/0.51 problem: 0.16/0.51 strict: 0.16/0.51 b(b(x1)) -> c(d(x1)) 0.16/0.51 b(x1) -> a(x1) 0.16/0.51 f(f(x1)) -> g(a(x1)) 0.16/0.51 weak: 0.16/0.51 g(g(x1)) -> a(x1) 0.16/0.51 a(a(x1)) -> b(c(x1)) 0.16/0.51 c(c(x1)) -> d(f(x1)) 0.16/0.51 d(d(x1)) -> f(f(f(x1))) 0.16/0.51 d(x1) -> b(x1) 0.16/0.51 Matrix Interpretation Processor: dim=1 0.16/0.51 0.16/0.51 max_matrix: 0.16/0.51 1 0.16/0.51 interpretation: 0.16/0.51 [g](x0) = x0 + 116, 0.16/0.51 0.16/0.51 [f](x0) = x0 + 15, 0.16/0.51 0.16/0.51 [d](x0) = x0 + 97, 0.16/0.51 0.16/0.51 [b](x0) = x0 + 90, 0.16/0.51 0.16/0.51 [c](x0) = x0 + 77, 0.16/0.51 0.16/0.51 [a](x0) = x0 + 88 0.16/0.51 orientation: 0.16/0.51 b(b(x1)) = x1 + 180 >= x1 + 174 = c(d(x1)) 0.16/0.51 0.16/0.51 b(x1) = x1 + 90 >= x1 + 88 = a(x1) 0.16/0.51 0.16/0.51 f(f(x1)) = x1 + 30 >= x1 + 204 = g(a(x1)) 0.16/0.51 0.16/0.51 g(g(x1)) = x1 + 232 >= x1 + 88 = a(x1) 0.16/0.51 0.16/0.51 a(a(x1)) = x1 + 176 >= x1 + 167 = b(c(x1)) 0.16/0.51 0.16/0.51 c(c(x1)) = x1 + 154 >= x1 + 112 = d(f(x1)) 0.16/0.51 0.16/0.51 d(d(x1)) = x1 + 194 >= x1 + 45 = f(f(f(x1))) 0.16/0.51 0.16/0.51 d(x1) = x1 + 97 >= x1 + 90 = b(x1) 0.16/0.51 problem: 0.16/0.51 strict: 0.16/0.51 f(f(x1)) -> g(a(x1)) 0.16/0.51 weak: 0.16/0.51 b(b(x1)) -> c(d(x1)) 0.16/0.51 b(x1) -> a(x1) 0.16/0.51 g(g(x1)) -> a(x1) 0.16/0.51 a(a(x1)) -> b(c(x1)) 0.16/0.51 c(c(x1)) -> d(f(x1)) 0.16/0.51 d(d(x1)) -> f(f(f(x1))) 0.16/0.51 d(x1) -> b(x1) 0.16/0.51 Matrix Interpretation Processor: dim=1 0.16/0.51 0.16/0.51 max_matrix: 0.16/0.51 1 0.16/0.51 interpretation: 0.16/0.51 [g](x0) = x0 + 107, 0.16/0.51 0.16/0.51 [f](x0) = x0 + 161, 0.16/0.51 0.16/0.51 [d](x0) = x0 + 243, 0.16/0.51 0.16/0.51 [b](x0) = x0 + 226, 0.16/0.51 0.16/0.51 [c](x0) = x0 + 202, 0.16/0.51 0.16/0.51 [a](x0) = x0 + 214 0.16/0.51 orientation: 0.16/0.51 f(f(x1)) = x1 + 322 >= x1 + 321 = g(a(x1)) 0.16/0.51 0.16/0.51 b(b(x1)) = x1 + 452 >= x1 + 445 = c(d(x1)) 0.16/0.51 0.16/0.51 b(x1) = x1 + 226 >= x1 + 214 = a(x1) 0.16/0.51 0.16/0.51 g(g(x1)) = x1 + 214 >= x1 + 214 = a(x1) 0.16/0.51 0.16/0.51 a(a(x1)) = x1 + 428 >= x1 + 428 = b(c(x1)) 0.16/0.51 0.16/0.51 c(c(x1)) = x1 + 404 >= x1 + 404 = d(f(x1)) 0.16/0.51 0.16/0.51 d(d(x1)) = x1 + 486 >= x1 + 483 = f(f(f(x1))) 0.16/0.51 0.16/0.51 d(x1) = x1 + 243 >= x1 + 226 = b(x1) 0.16/0.51 problem: 0.16/0.51 strict: 0.16/0.51 0.16/0.51 weak: 0.16/0.51 f(f(x1)) -> g(a(x1)) 0.16/0.51 b(b(x1)) -> c(d(x1)) 0.16/0.51 b(x1) -> a(x1) 0.16/0.51 g(g(x1)) -> a(x1) 0.16/0.51 a(a(x1)) -> b(c(x1)) 0.16/0.51 c(c(x1)) -> d(f(x1)) 0.16/0.51 d(d(x1)) -> f(f(f(x1))) 0.16/0.51 d(x1) -> b(x1) 0.16/0.51 Qed 0.16/0.52 EOF