YES(?,O(n^1)) 0.16/0.56 YES(?,O(n^1)) 0.16/0.57 0.16/0.57 Problem: 0.16/0.57 f(j(x,y),y) -> g(f(x,k(y))) 0.16/0.57 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.16/0.57 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.16/0.57 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.16/0.57 i(f(x,h(y))) -> y 0.16/0.57 i(h2(s(x),y,h1(x,z))) -> z 0.16/0.57 k(h(x)) -> h1(0(),x) 0.16/0.57 k(h1(x,y)) -> h1(s(x),y) 0.16/0.57 0.16/0.57 Proof: 0.16/0.57 Complexity Transformation Processor: 0.16/0.57 strict: 0.16/0.57 f(j(x,y),y) -> g(f(x,k(y))) 0.16/0.57 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.16/0.57 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.16/0.57 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.16/0.57 i(f(x,h(y))) -> y 0.16/0.57 i(h2(s(x),y,h1(x,z))) -> z 0.16/0.57 k(h(x)) -> h1(0(),x) 0.16/0.57 k(h1(x,y)) -> h1(s(x),y) 0.16/0.57 weak: 0.16/0.57 0.16/0.57 Matrix Interpretation Processor: dim=1 0.16/0.57 0.16/0.57 max_matrix: 0.16/0.57 1 0.16/0.57 interpretation: 0.16/0.57 [i](x0) = x0 + 6, 0.16/0.57 0.16/0.57 [h](x0) = x0 + 17, 0.16/0.57 0.16/0.57 [s](x0) = x0 + 2, 0.16/0.57 0.16/0.57 [h2](x0, x1, x2) = x0 + x1 + x2 + 248, 0.16/0.57 0.16/0.57 [0] = 33, 0.16/0.57 0.16/0.57 [h1](x0, x1) = x0 + x1 + 40, 0.16/0.57 0.16/0.57 [g](x0) = x0 + 136, 0.16/0.57 0.16/0.57 [k](x0) = x0 + 3, 0.16/0.57 0.16/0.57 [f](x0, x1) = x0 + x1 + 249, 0.16/0.57 0.16/0.57 [j](x0, x1) = x0 + x1 + 84 0.16/0.57 orientation: 0.16/0.57 f(j(x,y),y) = x + 2y + 333 >= x + y + 388 = g(f(x,k(y))) 0.16/0.57 0.16/0.57 f(x,h1(y,z)) = x + y + z + 289 >= x + y + z + 321 = h2(0(),x,h1(y,z)) 0.16/0.57 0.16/0.57 g(h2(x,y,h1(z,u))) = u + x + y + z + 424 >= u + x + y + z + 290 = h2(s(x),y,h1(z,u)) 0.16/0.57 0.16/0.57 h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 412 >= u + x + y + z + 292 = h2(s(x),y,h1(s(z),u)) 0.16/0.57 0.16/0.57 i(f(x,h(y))) = x + y + 272 >= y = y 0.16/0.57 0.16/0.57 i(h2(s(x),y,h1(x,z))) = 2x + y + z + 296 >= z = z 0.16/0.57 0.16/0.57 k(h(x)) = x + 20 >= x + 73 = h1(0(),x) 0.16/0.57 0.16/0.57 k(h1(x,y)) = x + y + 43 >= x + y + 42 = h1(s(x),y) 0.16/0.57 problem: 0.16/0.57 strict: 0.16/0.57 f(j(x,y),y) -> g(f(x,k(y))) 0.16/0.57 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.16/0.57 k(h(x)) -> h1(0(),x) 0.16/0.57 weak: 0.16/0.57 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.16/0.57 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.16/0.57 i(f(x,h(y))) -> y 0.16/0.57 i(h2(s(x),y,h1(x,z))) -> z 0.16/0.57 k(h1(x,y)) -> h1(s(x),y) 0.16/0.57 Matrix Interpretation Processor: dim=1 0.16/0.57 0.16/0.57 max_matrix: 0.16/0.57 1 0.16/0.57 interpretation: 0.16/0.57 [i](x0) = x0 + 10, 0.16/0.57 0.16/0.57 [h](x0) = x0 + 14, 0.16/0.57 0.16/0.57 [s](x0) = x0 + 5, 0.16/0.57 0.16/0.57 [h2](x0, x1, x2) = x0 + x1 + x2, 0.16/0.57 0.16/0.57 [0] = 4, 0.16/0.57 0.16/0.57 [h1](x0, x1) = x0 + x1 + 14, 0.16/0.57 0.16/0.57 [g](x0) = x0 + 6, 0.16/0.57 0.16/0.57 [k](x0) = x0 + 5, 0.16/0.57 0.16/0.57 [f](x0, x1) = x0 + x1 + 7, 0.16/0.57 0.16/0.57 [j](x0, x1) = x0 + x1 + 3 0.16/0.57 orientation: 0.16/0.57 f(j(x,y),y) = x + 2y + 10 >= x + y + 18 = g(f(x,k(y))) 0.16/0.57 0.16/0.57 f(x,h1(y,z)) = x + y + z + 21 >= x + y + z + 18 = h2(0(),x,h1(y,z)) 0.16/0.57 0.16/0.57 k(h(x)) = x + 19 >= x + 18 = h1(0(),x) 0.16/0.57 0.16/0.57 g(h2(x,y,h1(z,u))) = u + x + y + z + 20 >= u + x + y + z + 19 = h2(s(x),y,h1(z,u)) 0.16/0.57 0.16/0.57 h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 31 >= u + x + y + z + 24 = h2(s(x),y,h1(s(z),u)) 0.16/0.57 0.16/0.57 i(f(x,h(y))) = x + y + 31 >= y = y 0.16/0.57 0.16/0.57 i(h2(s(x),y,h1(x,z))) = 2x + y + z + 29 >= z = z 0.16/0.57 0.16/0.57 k(h1(x,y)) = x + y + 19 >= x + y + 19 = h1(s(x),y) 0.16/0.57 problem: 0.16/0.57 strict: 0.16/0.57 f(j(x,y),y) -> g(f(x,k(y))) 0.16/0.57 weak: 0.16/0.57 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.16/0.57 k(h(x)) -> h1(0(),x) 0.16/0.57 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.16/0.57 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.16/0.57 i(f(x,h(y))) -> y 0.16/0.57 i(h2(s(x),y,h1(x,z))) -> z 0.16/0.57 k(h1(x,y)) -> h1(s(x),y) 0.16/0.57 Matrix Interpretation Processor: dim=1 0.16/0.57 0.16/0.57 max_matrix: 0.16/0.57 1 0.16/0.57 interpretation: 0.16/0.57 [i](x0) = x0 + 2, 0.16/0.57 0.16/0.57 [h](x0) = x0 + 1, 0.16/0.57 0.16/0.57 [s](x0) = x0, 0.16/0.57 0.16/0.57 [h2](x0, x1, x2) = x0 + x1 + x2, 0.16/0.57 0.16/0.57 [0] = 0, 0.16/0.57 0.16/0.57 [h1](x0, x1) = x0 + x1, 0.16/0.57 0.16/0.57 [g](x0) = x0 + 1, 0.16/0.57 0.16/0.57 [k](x0) = x0, 0.16/0.57 0.16/0.57 [f](x0, x1) = x0 + x1, 0.16/0.57 0.16/0.57 [j](x0, x1) = x0 + x1 + 3 0.16/0.57 orientation: 0.16/0.57 f(j(x,y),y) = x + 2y + 3 >= x + y + 1 = g(f(x,k(y))) 0.16/0.57 0.16/0.57 f(x,h1(y,z)) = x + y + z >= x + y + z = h2(0(),x,h1(y,z)) 0.16/0.57 0.16/0.57 k(h(x)) = x + 1 >= x = h1(0(),x) 0.16/0.57 0.16/0.57 g(h2(x,y,h1(z,u))) = u + x + y + z + 1 >= u + x + y + z = h2(s(x),y,h1(z,u)) 0.16/0.57 0.16/0.57 h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 3 >= u + x + y + z = h2(s(x),y,h1(s(z),u)) 0.16/0.57 0.16/0.57 i(f(x,h(y))) = x + y + 3 >= y = y 0.16/0.57 0.16/0.57 i(h2(s(x),y,h1(x,z))) = 2x + y + z + 2 >= z = z 0.16/0.57 0.16/0.57 k(h1(x,y)) = x + y >= x + y = h1(s(x),y) 0.16/0.57 problem: 0.16/0.57 strict: 0.16/0.57 0.16/0.57 weak: 0.16/0.57 f(j(x,y),y) -> g(f(x,k(y))) 0.16/0.57 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.16/0.57 k(h(x)) -> h1(0(),x) 0.16/0.57 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.16/0.57 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.16/0.57 i(f(x,h(y))) -> y 0.16/0.57 i(h2(s(x),y,h1(x,z))) -> z 0.16/0.57 k(h1(x,y)) -> h1(s(x),y) 0.16/0.57 Qed 0.16/0.57 EOF