YES(?,O(n^1)) 0.17/0.68 YES(?,O(n^1)) 0.17/0.68 0.17/0.68 Problem: 0.17/0.68 f(j(x,y),y) -> g(f(x,k(y))) 0.17/0.68 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.17/0.68 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.17/0.68 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.17/0.68 i(f(x,h(y))) -> y 0.17/0.68 i(h2(s(x),y,h1(x,z))) -> z 0.17/0.68 k(h(x)) -> h1(0(),x) 0.17/0.68 k(h1(x,y)) -> h1(s(x),y) 0.17/0.68 0.17/0.68 Proof: 0.17/0.68 Complexity Transformation Processor: 0.17/0.68 strict: 0.17/0.68 f(j(x,y),y) -> g(f(x,k(y))) 0.17/0.68 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.17/0.68 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.17/0.68 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.17/0.68 i(f(x,h(y))) -> y 0.17/0.68 i(h2(s(x),y,h1(x,z))) -> z 0.17/0.68 k(h(x)) -> h1(0(),x) 0.17/0.68 k(h1(x,y)) -> h1(s(x),y) 0.17/0.68 weak: 0.17/0.68 0.17/0.68 Matrix Interpretation Processor: dim=1 0.17/0.68 0.17/0.68 max_matrix: 0.17/0.68 1 0.17/0.68 interpretation: 0.17/0.68 [i](x0) = x0 + 8, 0.17/0.68 0.17/0.68 [h](x0) = x0 + 6, 0.17/0.68 0.17/0.68 [s](x0) = x0 + 2, 0.17/0.68 0.17/0.68 [h2](x0, x1, x2) = x0 + x1 + x2 + 12, 0.17/0.68 0.17/0.68 [0] = 4, 0.17/0.68 0.17/0.68 [h1](x0, x1) = x0 + x1 + 6, 0.17/0.68 0.17/0.68 [g](x0) = x0 + 4, 0.17/0.68 0.17/0.68 [k](x0) = x0 + 3, 0.17/0.68 0.17/0.68 [f](x0, x1) = x0 + x1 + 10, 0.17/0.68 0.17/0.68 [j](x0, x1) = x0 + x1 + 6 0.17/0.68 orientation: 0.17/0.68 f(j(x,y),y) = x + 2y + 16 >= x + y + 17 = g(f(x,k(y))) 0.17/0.68 0.17/0.68 f(x,h1(y,z)) = x + y + z + 16 >= x + y + z + 22 = h2(0(),x,h1(y,z)) 0.17/0.68 0.17/0.68 g(h2(x,y,h1(z,u))) = u + x + y + z + 22 >= u + x + y + z + 20 = h2(s(x),y,h1(z,u)) 0.17/0.68 0.17/0.68 h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 30 >= u + x + y + z + 22 = h2(s(x),y,h1(s(z),u)) 0.17/0.68 0.17/0.68 i(f(x,h(y))) = x + y + 24 >= y = y 0.17/0.68 0.17/0.68 i(h2(s(x),y,h1(x,z))) = 2x + y + z + 28 >= z = z 0.17/0.68 0.17/0.68 k(h(x)) = x + 9 >= x + 10 = h1(0(),x) 0.17/0.68 0.17/0.68 k(h1(x,y)) = x + y + 9 >= x + y + 8 = h1(s(x),y) 0.17/0.68 problem: 0.17/0.68 strict: 0.17/0.68 f(j(x,y),y) -> g(f(x,k(y))) 0.17/0.68 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.17/0.68 k(h(x)) -> h1(0(),x) 0.17/0.68 weak: 0.17/0.68 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.17/0.68 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.17/0.68 i(f(x,h(y))) -> y 0.17/0.68 i(h2(s(x),y,h1(x,z))) -> z 0.17/0.68 k(h1(x,y)) -> h1(s(x),y) 0.17/0.68 Matrix Interpretation Processor: dim=1 0.17/0.68 0.17/0.68 max_matrix: 0.17/0.68 1 0.17/0.68 interpretation: 0.17/0.68 [i](x0) = x0 + 58, 0.17/0.68 0.17/0.68 [h](x0) = x0 + 96, 0.17/0.68 0.17/0.68 [s](x0) = x0 + 85, 0.17/0.68 0.17/0.68 [h2](x0, x1, x2) = x0 + x1 + x2 + 49, 0.17/0.68 0.17/0.68 [0] = 133, 0.17/0.68 0.17/0.68 [h1](x0, x1) = x0 + x1 + 13, 0.17/0.68 0.17/0.68 [g](x0) = x0 + 112, 0.17/0.68 0.17/0.68 [k](x0) = x0 + 161, 0.17/0.68 0.17/0.68 [f](x0, x1) = x0 + x1 + 93, 0.17/0.68 0.17/0.68 [j](x0, x1) = x0 + x1 + 240 0.17/0.68 orientation: 0.17/0.68 f(j(x,y),y) = x + 2y + 333 >= x + y + 366 = g(f(x,k(y))) 0.17/0.68 0.17/0.68 f(x,h1(y,z)) = x + y + z + 106 >= x + y + z + 195 = h2(0(),x,h1(y,z)) 0.17/0.68 0.17/0.68 k(h(x)) = x + 257 >= x + 146 = h1(0(),x) 0.17/0.68 0.17/0.68 g(h2(x,y,h1(z,u))) = u + x + y + z + 174 >= u + x + y + z + 147 = h2(s(x),y,h1(z,u)) 0.17/0.68 0.17/0.68 h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 315 >= u + x + y + z + 232 = h2(s(x),y,h1(s(z),u)) 0.17/0.68 0.17/0.68 i(f(x,h(y))) = x + y + 247 >= y = y 0.17/0.68 0.17/0.68 i(h2(s(x),y,h1(x,z))) = 2x + y + z + 205 >= z = z 0.17/0.68 0.17/0.68 k(h1(x,y)) = x + y + 174 >= x + y + 98 = h1(s(x),y) 0.17/0.68 problem: 0.17/0.68 strict: 0.17/0.68 f(j(x,y),y) -> g(f(x,k(y))) 0.17/0.68 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.17/0.68 weak: 0.17/0.68 k(h(x)) -> h1(0(),x) 0.17/0.68 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.17/0.68 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.17/0.69 i(f(x,h(y))) -> y 0.17/0.69 i(h2(s(x),y,h1(x,z))) -> z 0.17/0.69 k(h1(x,y)) -> h1(s(x),y) 0.17/0.69 Matrix Interpretation Processor: dim=1 0.17/0.69 0.17/0.69 max_matrix: 0.17/0.69 1 0.17/0.69 interpretation: 0.17/0.69 [i](x0) = x0 + 19, 0.17/0.69 0.17/0.69 [h](x0) = x0 + 96, 0.17/0.69 0.17/0.69 [s](x0) = x0 + 1, 0.17/0.69 0.17/0.69 [h2](x0, x1, x2) = x0 + x1 + x2 + 1, 0.17/0.69 0.17/0.69 [0] = 2, 0.17/0.69 0.17/0.69 [h1](x0, x1) = x0 + x1 + 32, 0.17/0.69 0.17/0.69 [g](x0) = x0 + 1, 0.17/0.69 0.17/0.69 [k](x0) = x0 + 2, 0.17/0.69 0.17/0.69 [f](x0, x1) = x0 + x1 + 8, 0.17/0.69 0.17/0.69 [j](x0, x1) = x0 + x1 0.17/0.69 orientation: 0.17/0.69 f(j(x,y),y) = x + 2y + 8 >= x + y + 11 = g(f(x,k(y))) 0.17/0.69 0.17/0.69 f(x,h1(y,z)) = x + y + z + 40 >= x + y + z + 35 = h2(0(),x,h1(y,z)) 0.17/0.69 0.17/0.69 k(h(x)) = x + 98 >= x + 34 = h1(0(),x) 0.17/0.69 0.17/0.69 g(h2(x,y,h1(z,u))) = u + x + y + z + 34 >= u + x + y + z + 34 = h2(s(x),y,h1(z,u)) 0.17/0.69 0.17/0.69 h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 65 >= u + x + y + z + 35 = h2(s(x),y,h1(s(z),u)) 0.17/0.69 0.17/0.69 i(f(x,h(y))) = x + y + 123 >= y = y 0.17/0.69 0.17/0.69 i(h2(s(x),y,h1(x,z))) = 2x + y + z + 53 >= z = z 0.17/0.69 0.17/0.69 k(h1(x,y)) = x + y + 34 >= x + y + 33 = h1(s(x),y) 0.17/0.69 problem: 0.17/0.69 strict: 0.17/0.69 f(j(x,y),y) -> g(f(x,k(y))) 0.17/0.69 weak: 0.17/0.69 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.17/0.69 k(h(x)) -> h1(0(),x) 0.17/0.69 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.17/0.69 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.17/0.69 i(f(x,h(y))) -> y 0.17/0.69 i(h2(s(x),y,h1(x,z))) -> z 0.17/0.69 k(h1(x,y)) -> h1(s(x),y) 0.17/0.69 Matrix Interpretation Processor: dim=1 0.17/0.69 0.17/0.69 max_matrix: 0.17/0.69 1 0.17/0.69 interpretation: 0.17/0.69 [i](x0) = x0 + 96, 0.17/0.69 0.17/0.69 [h](x0) = x0 + 126, 0.17/0.69 0.17/0.69 [s](x0) = x0 + 2, 0.17/0.69 0.17/0.69 [h2](x0, x1, x2) = x0 + x1 + x2 + 15, 0.17/0.69 0.17/0.69 [0] = 3, 0.17/0.69 0.17/0.69 [h1](x0, x1) = x0 + x1 + 113, 0.17/0.69 0.17/0.69 [g](x0) = x0 + 2, 0.17/0.69 0.17/0.69 [k](x0) = x0 + 2, 0.17/0.69 0.17/0.69 [f](x0, x1) = x0 + x1 + 28, 0.17/0.69 0.17/0.69 [j](x0, x1) = x0 + x1 + 9 0.17/0.69 orientation: 0.17/0.69 f(j(x,y),y) = x + 2y + 37 >= x + y + 32 = g(f(x,k(y))) 0.17/0.69 0.17/0.69 f(x,h1(y,z)) = x + y + z + 141 >= x + y + z + 131 = h2(0(),x,h1(y,z)) 0.17/0.69 0.17/0.69 k(h(x)) = x + 128 >= x + 116 = h1(0(),x) 0.17/0.69 0.17/0.69 g(h2(x,y,h1(z,u))) = u + x + y + z + 130 >= u + x + y + z + 130 = h2(s(x),y,h1(z,u)) 0.17/0.69 0.17/0.69 h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 250 >= u + x + y + z + 132 = h2(s(x),y,h1(s(z),u)) 0.17/0.69 0.17/0.69 i(f(x,h(y))) = x + y + 250 >= y = y 0.17/0.69 0.17/0.69 i(h2(s(x),y,h1(x,z))) = 2x + y + z + 226 >= z = z 0.17/0.69 0.17/0.69 k(h1(x,y)) = x + y + 115 >= x + y + 115 = h1(s(x),y) 0.17/0.69 problem: 0.17/0.69 strict: 0.17/0.69 0.17/0.69 weak: 0.17/0.69 f(j(x,y),y) -> g(f(x,k(y))) 0.17/0.69 f(x,h1(y,z)) -> h2(0(),x,h1(y,z)) 0.17/0.69 k(h(x)) -> h1(0(),x) 0.17/0.69 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) 0.17/0.69 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) 0.17/0.69 i(f(x,h(y))) -> y 0.17/0.69 i(h2(s(x),y,h1(x,z))) -> z 0.17/0.69 k(h1(x,y)) -> h1(s(x),y) 0.17/0.69 Qed 0.17/0.69 EOF