YES(O(1),O(n^2)) 229.11/103.56 YES(O(1),O(n^2)) 229.11/103.56 229.11/103.56 We are left with following problem, upon which TcT provides the 229.11/103.56 certificate YES(O(1),O(n^2)). 229.11/103.56 229.11/103.56 Strict Trs: 229.11/103.56 { f(x, 0()) -> x 229.11/103.56 , f(f(x, y), z) -> f(x, f(y, z)) 229.11/103.56 , f(0(), y) -> y 229.11/103.56 , f(i(x), y) -> i(x) 229.11/103.56 , f(g(x, y), z) -> g(f(x, z), f(y, z)) 229.11/103.56 , f(1(), g(x, y)) -> x 229.11/103.56 , f(2(), g(x, y)) -> y } 229.11/103.56 Obligation: 229.11/103.56 runtime complexity 229.11/103.56 Answer: 229.11/103.56 YES(O(1),O(n^2)) 229.11/103.56 229.11/103.56 We add the following weak dependency pairs: 229.11/103.56 229.11/103.56 Strict DPs: 229.11/103.56 { f^#(x, 0()) -> c_1(x) 229.11/103.56 , f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) 229.11/103.56 , f^#(0(), y) -> c_3(y) 229.11/103.56 , f^#(i(x), y) -> c_4(x) 229.11/103.56 , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.56 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.56 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.56 229.11/103.56 and mark the set of starting terms. 229.11/103.56 229.11/103.56 We are left with following problem, upon which TcT provides the 229.11/103.56 certificate YES(O(1),O(n^2)). 229.11/103.56 229.11/103.56 Strict DPs: 229.11/103.56 { f^#(x, 0()) -> c_1(x) 229.11/103.56 , f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) 229.11/103.56 , f^#(0(), y) -> c_3(y) 229.11/103.56 , f^#(i(x), y) -> c_4(x) 229.11/103.56 , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.56 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.56 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.56 Strict Trs: 229.11/103.56 { f(x, 0()) -> x 229.11/103.56 , f(f(x, y), z) -> f(x, f(y, z)) 229.11/103.56 , f(0(), y) -> y 229.11/103.56 , f(i(x), y) -> i(x) 229.11/103.56 , f(g(x, y), z) -> g(f(x, z), f(y, z)) 229.11/103.56 , f(1(), g(x, y)) -> x 229.11/103.56 , f(2(), g(x, y)) -> y } 229.11/103.56 Obligation: 229.11/103.56 runtime complexity 229.11/103.56 Answer: 229.11/103.56 YES(O(1),O(n^2)) 229.11/103.56 229.11/103.56 We use the processor 'polynomial interpretation' to orient 229.11/103.56 following rules strictly. 229.11/103.56 229.11/103.56 DPs: 229.11/103.56 { f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.56 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.56 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.56 Trs: 229.11/103.56 { f(1(), g(x, y)) -> x 229.11/103.56 , f(2(), g(x, y)) -> y } 229.11/103.56 229.11/103.56 The induced complexity on above rules (modulo remaining rules) is 229.11/103.56 YES(?,O(n^2)) . These rules are moved into the corresponding weak 229.11/103.56 component(s). 229.11/103.56 229.11/103.56 Sub-proof: 229.11/103.56 ---------- 229.11/103.56 We consider the following typing: 229.11/103.56 229.11/103.56 f :: (b,b) -> b 229.11/103.56 0 :: b 229.11/103.56 i :: a -> b 229.11/103.56 g :: (b,b) -> b 229.11/103.56 1 :: b 229.11/103.56 2 :: b 229.11/103.56 f^# :: (b,b) -> c 229.11/103.56 c_1 :: b -> c 229.11/103.56 c_2 :: c -> c 229.11/103.56 c_3 :: b -> c 229.11/103.56 c_4 :: a -> c 229.11/103.56 c_5 :: (c,c) -> c 229.11/103.56 c_6 :: b -> c 229.11/103.56 c_7 :: b -> c 229.11/103.56 229.11/103.56 The following argument positions are considered usable: 229.11/103.56 229.11/103.56 Uargs(f) = {2}, Uargs(g) = {1, 2}, Uargs(f^#) = {2}, 229.11/103.56 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, 229.11/103.56 Uargs(c_6) = {1}, Uargs(c_7) = {1} 229.11/103.56 229.11/103.56 TcT has computed the following constructor-restricted 229.11/103.56 typedpolynomial interpretation. 229.11/103.56 229.11/103.56 [f](x1, x2) = x1 + x1*x2 + x2 229.11/103.56 229.11/103.56 [0]() = 0 229.11/103.56 229.11/103.56 [i](x1) = 0 229.11/103.56 229.11/103.56 [g](x1, x2) = 1 + x1 + x2 229.11/103.56 229.11/103.56 [1]() = 0 229.11/103.56 229.11/103.56 [2]() = 0 229.11/103.56 229.11/103.56 [f^#](x1, x2) = x1 + x1*x2 + x2 229.11/103.56 229.11/103.56 [c_1](x1) = x1 229.11/103.56 229.11/103.56 [c_2](x1) = x1 229.11/103.56 229.11/103.56 [c_3](x1) = x1 229.11/103.56 229.11/103.56 [c_4](x1) = 0 229.11/103.56 229.11/103.56 [c_5](x1, x2) = x1 + x2 229.11/103.56 229.11/103.56 [c_6](x1) = x1 229.11/103.56 229.11/103.56 [c_7](x1) = x1 229.11/103.56 229.11/103.56 229.11/103.56 This order satisfies the following ordering constraints. 229.11/103.56 229.11/103.56 [f(x, 0())] = x 229.11/103.56 >= x 229.11/103.56 = [x] 229.11/103.56 229.11/103.56 [f(f(x, y), z)] = x + x*y + y + x*z + x*y*z + y*z + z 229.11/103.56 >= x + x*y + x*y*z + x*z + y + y*z + z 229.11/103.56 = [f(x, f(y, z))] 229.11/103.56 229.11/103.56 [f(0(), y)] = y 229.11/103.56 >= y 229.11/103.56 = [y] 229.11/103.56 229.11/103.56 [f(i(x), y)] = y 229.11/103.56 >= 229.11/103.56 = [i(x)] 229.11/103.56 229.11/103.56 [f(g(x, y), z)] = 1 + x + y + 2*z + x*z + y*z 229.11/103.56 >= 1 + x + x*z + 2*z + y + y*z 229.11/103.56 = [g(f(x, z), f(y, z))] 229.11/103.56 229.11/103.56 [f(1(), g(x, y))] = 1 + x + y 229.11/103.56 > x 229.11/103.56 = [x] 229.11/103.56 229.11/103.56 [f(2(), g(x, y))] = 1 + x + y 229.11/103.56 > y 229.11/103.56 = [y] 229.11/103.56 229.11/103.56 229.11/103.56 We return to the main proof. 229.11/103.56 229.11/103.56 We are left with following problem, upon which TcT provides the 229.11/103.56 certificate YES(O(1),O(n^2)). 229.11/103.56 229.11/103.56 Strict DPs: 229.11/103.56 { f^#(x, 0()) -> c_1(x) 229.11/103.56 , f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) 229.11/103.56 , f^#(0(), y) -> c_3(y) 229.11/103.56 , f^#(i(x), y) -> c_4(x) } 229.11/103.56 Strict Trs: 229.11/103.56 { f(x, 0()) -> x 229.11/103.56 , f(f(x, y), z) -> f(x, f(y, z)) 229.11/103.56 , f(0(), y) -> y 229.11/103.56 , f(i(x), y) -> i(x) 229.11/103.56 , f(g(x, y), z) -> g(f(x, z), f(y, z)) } 229.11/103.56 Weak DPs: 229.11/103.56 { f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.56 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.56 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.56 Weak Trs: 229.11/103.56 { f(1(), g(x, y)) -> x 229.11/103.56 , f(2(), g(x, y)) -> y } 229.11/103.56 Obligation: 229.11/103.56 runtime complexity 229.11/103.56 Answer: 229.11/103.56 YES(O(1),O(n^2)) 229.11/103.56 229.11/103.56 We use the processor 'polynomial interpretation' to orient 229.11/103.56 following rules strictly. 229.11/103.56 229.11/103.56 DPs: 229.11/103.56 { f^#(x, 0()) -> c_1(x) 229.11/103.56 , f^#(0(), y) -> c_3(y) } 229.11/103.56 Trs: 229.11/103.56 { f(x, 0()) -> x 229.11/103.56 , f(0(), y) -> y } 229.11/103.56 229.11/103.56 The induced complexity on above rules (modulo remaining rules) is 229.11/103.56 YES(?,O(n^2)) . These rules are moved into the corresponding weak 229.11/103.56 component(s). 229.11/103.56 229.11/103.56 Sub-proof: 229.11/103.56 ---------- 229.11/103.56 We consider the following typing: 229.11/103.56 229.11/103.56 f :: (b,b) -> b 229.11/103.56 0 :: b 229.11/103.56 i :: a -> b 229.11/103.56 g :: (b,b) -> b 229.11/103.56 1 :: b 229.11/103.56 2 :: b 229.11/103.56 f^# :: (b,b) -> c 229.11/103.56 c_1 :: b -> c 229.11/103.56 c_2 :: c -> c 229.11/103.56 c_3 :: b -> c 229.11/103.56 c_4 :: a -> c 229.11/103.56 c_5 :: (c,c) -> c 229.11/103.56 c_6 :: b -> c 229.11/103.56 c_7 :: b -> c 229.11/103.56 229.11/103.56 The following argument positions are considered usable: 229.11/103.56 229.11/103.56 Uargs(f) = {2}, Uargs(g) = {1, 2}, Uargs(f^#) = {2}, 229.11/103.56 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, 229.11/103.56 Uargs(c_6) = {1}, Uargs(c_7) = {1} 229.11/103.56 229.11/103.56 TcT has computed the following constructor-restricted 229.11/103.56 typedpolynomial interpretation. 229.11/103.56 229.11/103.56 [f](x1, x2) = x1 + x1*x2 + x2 229.11/103.56 229.11/103.56 [0]() = 1 229.11/103.56 229.11/103.56 [i](x1) = 0 229.11/103.56 229.11/103.56 [g](x1, x2) = 1 + x1 + x2 229.11/103.56 229.11/103.56 [1]() = 0 229.11/103.56 229.11/103.56 [2]() = 0 229.11/103.56 229.11/103.56 [f^#](x1, x2) = x1 + x1*x2 + x2 229.11/103.56 229.11/103.56 [c_1](x1) = x1 229.11/103.56 229.11/103.56 [c_2](x1) = x1 229.11/103.56 229.11/103.56 [c_3](x1) = 2*x1 229.11/103.56 229.11/103.56 [c_4](x1) = 0 229.11/103.56 229.11/103.56 [c_5](x1, x2) = x1 + x2 229.11/103.56 229.11/103.56 [c_6](x1) = x1 229.11/103.56 229.11/103.56 [c_7](x1) = x1 229.11/103.56 229.11/103.56 229.11/103.56 This order satisfies the following ordering constraints. 229.11/103.56 229.11/103.56 [f(x, 0())] = 2*x + 1 229.11/103.56 > x 229.11/103.56 = [x] 229.11/103.56 229.11/103.56 [f(f(x, y), z)] = x + x*y + y + x*z + x*y*z + y*z + z 229.11/103.56 >= x + x*y + x*y*z + x*z + y + y*z + z 229.11/103.56 = [f(x, f(y, z))] 229.11/103.56 229.11/103.56 [f(0(), y)] = 1 + 2*y 229.11/103.56 > y 229.11/103.56 = [y] 229.11/103.56 229.11/103.56 [f(i(x), y)] = y 229.11/103.56 >= 229.11/103.56 = [i(x)] 229.11/103.56 229.11/103.56 [f(g(x, y), z)] = 1 + x + y + 2*z + x*z + y*z 229.11/103.56 >= 1 + x + x*z + 2*z + y + y*z 229.11/103.56 = [g(f(x, z), f(y, z))] 229.11/103.56 229.11/103.56 [f(1(), g(x, y))] = 1 + x + y 229.11/103.56 > x 229.11/103.56 = [x] 229.11/103.56 229.11/103.56 [f(2(), g(x, y))] = 1 + x + y 229.11/103.56 > y 229.11/103.56 = [y] 229.11/103.56 229.11/103.56 229.11/103.56 We return to the main proof. 229.11/103.56 229.11/103.56 We are left with following problem, upon which TcT provides the 229.11/103.56 certificate YES(O(1),O(n^2)). 229.11/103.56 229.11/103.56 Strict DPs: 229.11/103.56 { f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) 229.11/103.56 , f^#(i(x), y) -> c_4(x) } 229.11/103.56 Strict Trs: 229.11/103.56 { f(f(x, y), z) -> f(x, f(y, z)) 229.11/103.56 , f(i(x), y) -> i(x) 229.11/103.56 , f(g(x, y), z) -> g(f(x, z), f(y, z)) } 229.11/103.56 Weak DPs: 229.11/103.56 { f^#(x, 0()) -> c_1(x) 229.11/103.56 , f^#(0(), y) -> c_3(y) 229.11/103.56 , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.56 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.56 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.56 Weak Trs: 229.11/103.56 { f(x, 0()) -> x 229.11/103.56 , f(0(), y) -> y 229.11/103.56 , f(1(), g(x, y)) -> x 229.11/103.56 , f(2(), g(x, y)) -> y } 229.11/103.56 Obligation: 229.11/103.56 runtime complexity 229.11/103.56 Answer: 229.11/103.56 YES(O(1),O(n^2)) 229.11/103.56 229.11/103.56 We use the processor 'polynomial interpretation' to orient 229.11/103.56 following rules strictly. 229.11/103.56 229.11/103.56 DPs: { f^#(i(x), y) -> c_4(x) } 229.11/103.56 Trs: 229.11/103.56 { f(i(x), y) -> i(x) 229.11/103.56 , f(g(x, y), z) -> g(f(x, z), f(y, z)) } 229.11/103.56 229.11/103.56 The induced complexity on above rules (modulo remaining rules) is 229.11/103.56 YES(?,O(n^2)) . These rules are moved into the corresponding weak 229.11/103.56 component(s). 229.11/103.56 229.11/103.56 Sub-proof: 229.11/103.56 ---------- 229.11/103.56 We consider the following typing: 229.11/103.56 229.11/103.56 f :: (b,b) -> b 229.11/103.56 0 :: b 229.11/103.56 i :: a -> b 229.11/103.56 g :: (b,b) -> b 229.11/103.56 1 :: b 229.11/103.56 2 :: b 229.11/103.56 f^# :: (b,b) -> c 229.11/103.56 c_1 :: b -> c 229.11/103.56 c_2 :: c -> c 229.11/103.56 c_3 :: b -> c 229.11/103.56 c_4 :: a -> c 229.11/103.56 c_5 :: (c,c) -> c 229.11/103.56 c_6 :: b -> c 229.11/103.56 c_7 :: b -> c 229.11/103.56 229.11/103.56 The following argument positions are considered usable: 229.11/103.56 229.11/103.56 Uargs(f) = {2}, Uargs(g) = {1, 2}, Uargs(f^#) = {2}, 229.11/103.56 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, 229.11/103.56 Uargs(c_6) = {1}, Uargs(c_7) = {1} 229.11/103.56 229.11/103.56 TcT has computed the following constructor-restricted 229.11/103.56 typedpolynomial interpretation. 229.11/103.56 229.11/103.56 [f](x1, x2) = x1 + x1*x2 + x1^2 + x2 229.11/103.56 229.11/103.56 [0]() = 0 229.11/103.56 229.11/103.56 [i](x1) = 2 229.11/103.56 229.11/103.56 [g](x1, x2) = 2 + x1 + x2 229.11/103.56 229.11/103.56 [1]() = 0 229.11/103.56 229.11/103.56 [2]() = 0 229.11/103.56 229.11/103.56 [f^#](x1, x2) = x1 + x1*x2 + x1^2 + x2 229.11/103.56 229.11/103.56 [c_1](x1) = x1 + x1^2 229.11/103.56 229.11/103.56 [c_2](x1) = x1 229.11/103.56 229.11/103.56 [c_3](x1) = x1 229.11/103.56 229.11/103.56 [c_4](x1) = 1 229.11/103.56 229.11/103.56 [c_5](x1, x2) = 1 + x1 + x2 229.11/103.56 229.11/103.56 [c_6](x1) = x1 229.11/103.56 229.11/103.56 [c_7](x1) = x1 229.11/103.56 229.11/103.56 229.11/103.56 This order satisfies the following ordering constraints. 229.11/103.56 229.11/103.56 [f(x, 0())] = x + x^2 229.11/103.56 >= x 229.11/103.56 = [x] 229.11/103.56 229.11/103.56 [f(f(x, y), z)] = x + 2*x*y + 2*x^2 + y + x*z + x*y*z + x^2*z + y*z + 3*x^2*y + 2*x^3 + x^2*y^2 + 2*x^3*y + x*y^2 + x^4 + y*x + y^2*x + y*x^2 + y^2 + z 229.11/103.56 >= x + x*y + x*y*z + x*y^2 + x*z + x^2 + y + y*z + y^2 + z 229.11/103.56 = [f(x, f(y, z))] 229.11/103.56 229.11/103.56 [f(0(), y)] = y 229.11/103.56 >= y 229.11/103.56 = [y] 229.11/103.56 229.11/103.56 [f(i(x), y)] = 6 + 3*y 229.11/103.56 > 2 229.11/103.56 = [i(x)] 229.11/103.56 229.11/103.56 [f(g(x, y), z)] = 6 + 5*x + 5*y + 3*z + x*z + y*z + x^2 + x*y + y*x + y^2 229.11/103.56 > 2 + x + x*z + x^2 + 2*z + y + y*z + y^2 229.11/103.56 = [g(f(x, z), f(y, z))] 229.11/103.56 229.11/103.56 [f(1(), g(x, y))] = 2 + x + y 229.11/103.56 > x 229.11/103.56 = [x] 229.11/103.56 229.11/103.56 [f(2(), g(x, y))] = 2 + x + y 229.11/103.56 > y 229.11/103.56 = [y] 229.11/103.56 229.11/103.56 229.11/103.56 We return to the main proof. 229.11/103.56 229.11/103.56 We are left with following problem, upon which TcT provides the 229.11/103.56 certificate YES(O(1),O(n^2)). 229.11/103.56 229.11/103.56 Strict DPs: { f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) } 229.11/103.56 Strict Trs: { f(f(x, y), z) -> f(x, f(y, z)) } 229.11/103.56 Weak DPs: 229.11/103.56 { f^#(x, 0()) -> c_1(x) 229.11/103.56 , f^#(0(), y) -> c_3(y) 229.11/103.56 , f^#(i(x), y) -> c_4(x) 229.11/103.56 , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.56 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.56 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.56 Weak Trs: 229.11/103.56 { f(x, 0()) -> x 229.11/103.56 , f(0(), y) -> y 229.11/103.56 , f(i(x), y) -> i(x) 229.11/103.56 , f(g(x, y), z) -> g(f(x, z), f(y, z)) 229.11/103.56 , f(1(), g(x, y)) -> x 229.11/103.56 , f(2(), g(x, y)) -> y } 229.11/103.56 Obligation: 229.11/103.56 runtime complexity 229.11/103.56 Answer: 229.11/103.56 YES(O(1),O(n^2)) 229.11/103.56 229.11/103.56 We use the processor 'polynomial interpretation' to orient 229.11/103.56 following rules strictly. 229.11/103.56 229.11/103.56 Trs: { f(f(x, y), z) -> f(x, f(y, z)) } 229.11/103.56 229.11/103.56 The induced complexity on above rules (modulo remaining rules) is 229.11/103.56 YES(?,O(n^2)) . These rules are moved into the corresponding weak 229.11/103.56 component(s). 229.11/103.56 229.11/103.56 Sub-proof: 229.11/103.56 ---------- 229.11/103.56 We consider the following typing: 229.11/103.56 229.11/103.56 f :: (b,b) -> b 229.11/103.56 0 :: b 229.11/103.56 i :: a -> b 229.11/103.56 g :: (b,b) -> b 229.11/103.56 1 :: b 229.11/103.56 2 :: b 229.11/103.56 f^# :: (b,b) -> c 229.11/103.56 c_1 :: b -> c 229.11/103.56 c_2 :: c -> c 229.11/103.56 c_3 :: b -> c 229.11/103.56 c_4 :: a -> c 229.11/103.56 c_5 :: (c,c) -> c 229.11/103.56 c_6 :: b -> c 229.11/103.56 c_7 :: b -> c 229.11/103.56 229.11/103.56 The following argument positions are considered usable: 229.11/103.56 229.11/103.56 Uargs(f) = {2}, Uargs(g) = {1, 2}, Uargs(f^#) = {2}, 229.11/103.56 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, 229.11/103.56 Uargs(c_6) = {1}, Uargs(c_7) = {1} 229.11/103.56 229.11/103.56 TcT has computed the following constructor-restricted 229.11/103.56 typedpolynomial interpretation. 229.11/103.56 229.11/103.56 [f](x1, x2) = 1 + x1 + x1*x2 + x1^2 + x2 229.11/103.56 229.11/103.56 [0]() = 0 229.11/103.56 229.11/103.56 [i](x1) = 0 229.11/103.56 229.11/103.56 [g](x1, x2) = 1 + x1 + x2 229.11/103.56 229.11/103.56 [1]() = 0 229.11/103.56 229.11/103.56 [2]() = 0 229.11/103.56 229.11/103.56 [f^#](x1, x2) = x1*x2 + x1^2 + x2 229.11/103.56 229.11/103.56 [c_1](x1) = x1^2 229.11/103.56 229.11/103.56 [c_2](x1) = x1 229.11/103.56 229.11/103.56 [c_3](x1) = x1 229.11/103.56 229.11/103.56 [c_4](x1) = 0 229.11/103.56 229.11/103.56 [c_5](x1, x2) = 1 + x1 + x2 229.11/103.56 229.11/103.56 [c_6](x1) = x1 229.11/103.56 229.11/103.56 [c_7](x1) = 1 + x1 229.11/103.56 229.11/103.56 229.11/103.56 This order satisfies the following ordering constraints. 229.11/103.56 229.11/103.56 [f(x, 0())] = 1 + x + x^2 229.11/103.56 > x 229.11/103.56 = [x] 229.11/103.56 229.11/103.56 [f(f(x, y), z)] = 3 + 3*x + 4*x*y + 4*x^2 + 3*y + 2*z + x*z + x*y*z + x^2*z + y*z + 3*x^2*y + 2*x^3 + x^2*y^2 + 2*x^3*y + x*y^2 + x^4 + y*x + y^2*x + y*x^2 + y^2 229.11/103.56 > 2 + 2*x + x*y + x*y*z + x*y^2 + x*z + x^2 + y + y*z + y^2 + z 229.11/103.56 = [f(x, f(y, z))] 229.11/103.56 229.11/103.56 [f(0(), y)] = 1 + y 229.11/103.56 > y 229.11/103.56 = [y] 229.11/103.56 229.11/103.56 [f(i(x), y)] = 1 + y 229.11/103.56 > 229.11/103.56 = [i(x)] 229.11/103.56 229.11/103.56 [f(g(x, y), z)] = 3 + 3*x + 3*y + 2*z + x*z + y*z + x^2 + x*y + y*x + y^2 229.11/103.56 >= 3 + x + x*z + x^2 + 2*z + y + y*z + y^2 229.11/103.56 = [g(f(x, z), f(y, z))] 229.11/103.56 229.11/103.56 [f(1(), g(x, y))] = 2 + x + y 229.11/103.56 > x 229.11/103.56 = [x] 229.11/103.56 229.11/103.56 [f(2(), g(x, y))] = 2 + x + y 229.11/103.56 > y 229.11/103.56 = [y] 229.11/103.56 229.11/103.56 229.11/103.56 We return to the main proof. 229.11/103.56 229.11/103.56 We are left with following problem, upon which TcT provides the 229.11/103.56 certificate YES(O(1),O(n^2)). 229.11/103.56 229.11/103.56 Strict DPs: { f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) } 229.11/103.56 Weak DPs: 229.11/103.56 { f^#(x, 0()) -> c_1(x) 229.11/103.56 , f^#(0(), y) -> c_3(y) 229.11/103.56 , f^#(i(x), y) -> c_4(x) 229.11/103.56 , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.56 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.56 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.56 Weak Trs: 229.11/103.56 { f(x, 0()) -> x 229.11/103.56 , f(f(x, y), z) -> f(x, f(y, z)) 229.11/103.56 , f(0(), y) -> y 229.11/103.56 , f(i(x), y) -> i(x) 229.11/103.56 , f(g(x, y), z) -> g(f(x, z), f(y, z)) 229.11/103.56 , f(1(), g(x, y)) -> x 229.11/103.56 , f(2(), g(x, y)) -> y } 229.11/103.56 Obligation: 229.11/103.56 runtime complexity 229.11/103.56 Answer: 229.11/103.56 YES(O(1),O(n^2)) 229.11/103.56 229.11/103.56 We use the processor 'polynomial interpretation' to orient 229.11/103.56 following rules strictly. 229.11/103.56 229.11/103.56 DPs: 229.11/103.56 { 1: f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) 229.11/103.56 , 3: f^#(0(), y) -> c_3(y) 229.11/103.56 , 5: f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.56 , 6: f^#(1(), g(x, y)) -> c_6(x) 229.11/103.56 , 7: f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.56 Trs: 229.11/103.56 { f(x, 0()) -> x 229.11/103.56 , f(f(x, y), z) -> f(x, f(y, z)) 229.11/103.56 , f(0(), y) -> y 229.11/103.57 , f(i(x), y) -> i(x) 229.11/103.57 , f(g(x, y), z) -> g(f(x, z), f(y, z)) 229.11/103.57 , f(1(), g(x, y)) -> x 229.11/103.57 , f(2(), g(x, y)) -> y } 229.11/103.57 229.11/103.57 Sub-proof: 229.11/103.57 ---------- 229.11/103.57 We consider the following typing: 229.11/103.57 229.11/103.57 f :: (b,b) -> b 229.11/103.57 0 :: b 229.11/103.57 i :: a -> b 229.11/103.57 g :: (b,b) -> b 229.11/103.57 1 :: b 229.11/103.57 2 :: b 229.11/103.57 f^# :: (b,b) -> c 229.11/103.57 c_1 :: b -> c 229.11/103.57 c_2 :: c -> c 229.11/103.57 c_3 :: b -> c 229.11/103.57 c_4 :: a -> c 229.11/103.57 c_5 :: (c,c) -> c 229.11/103.57 c_6 :: b -> c 229.11/103.57 c_7 :: b -> c 229.11/103.57 229.11/103.57 The following argument positions are considered usable: 229.11/103.57 229.11/103.57 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, 229.11/103.57 Uargs(c_6) = {1}, Uargs(c_7) = {1} 229.11/103.57 229.11/103.57 TcT has computed the following constructor-restricted 229.11/103.57 typedpolynomial interpretation. 229.11/103.57 229.11/103.57 [f](x1, x2) = 1 + x1 + x1*x2 + x1^2 + x2 229.11/103.57 229.11/103.57 [0]() = 1 229.11/103.57 229.11/103.57 [i](x1) = 0 229.11/103.57 229.11/103.57 [g](x1, x2) = 2 + x1 + x2 229.11/103.57 229.11/103.57 [1]() = 1 229.11/103.57 229.11/103.57 [2]() = 1 229.11/103.57 229.11/103.57 [f^#](x1, x2) = x1 + x1*x2 + x1^2 229.11/103.57 229.11/103.57 [c_1](x1) = x1 + x1^2 229.11/103.57 229.11/103.57 [c_2](x1) = x1 229.11/103.57 229.11/103.57 [c_3](x1) = x1 229.11/103.57 229.11/103.57 [c_4](x1) = 0 229.11/103.57 229.11/103.57 [c_5](x1, x2) = 1 + x1 + x2 229.11/103.57 229.11/103.57 [c_6](x1) = 2 + x1 229.11/103.57 229.11/103.57 [c_7](x1) = 2 + x1 229.11/103.57 229.11/103.57 229.11/103.57 This order satisfies the following ordering constraints. 229.11/103.57 229.11/103.57 [f(x, 0())] = 2 + 2*x + x^2 229.11/103.57 > x 229.11/103.57 = [x] 229.11/103.57 229.11/103.57 [f(f(x, y), z)] = 3 + 3*x + 4*x*y + 4*x^2 + 3*y + 2*z + x*z + x*y*z + x^2*z + y*z + 3*x^2*y + 2*x^3 + x^2*y^2 + 2*x^3*y + x*y^2 + x^4 + y*x + y^2*x + y*x^2 + y^2 229.11/103.57 > 2 + 2*x + x*y + x*y*z + x*y^2 + x*z + x^2 + y + y*z + y^2 + z 229.11/103.57 = [f(x, f(y, z))] 229.11/103.57 229.11/103.57 [f(0(), y)] = 3 + 2*y 229.11/103.57 > y 229.11/103.57 = [y] 229.11/103.57 229.11/103.57 [f(i(x), y)] = 1 + y 229.11/103.57 > 229.11/103.57 = [i(x)] 229.11/103.57 229.11/103.57 [f(g(x, y), z)] = 7 + 5*x + 5*y + 3*z + x*z + y*z + x^2 + x*y + y*x + y^2 229.11/103.57 > 4 + x + x*z + x^2 + 2*z + y + y*z + y^2 229.11/103.57 = [g(f(x, z), f(y, z))] 229.11/103.57 229.11/103.57 [f(1(), g(x, y))] = 7 + 2*x + 2*y 229.11/103.57 > x 229.11/103.57 = [x] 229.11/103.57 229.11/103.57 [f(2(), g(x, y))] = 7 + 2*x + 2*y 229.11/103.57 > y 229.11/103.57 = [y] 229.11/103.57 229.11/103.57 [f^#(x, 0())] = 2*x + x^2 229.11/103.57 >= x + x^2 229.11/103.57 = [c_1(x)] 229.11/103.57 229.11/103.57 [f^#(f(x, y), z)] = 2 + 3*x + 4*x*y + 4*x^2 + 3*y + z + x*z + x*y*z + x^2*z + y*z + 3*x^2*y + 2*x^3 + x^2*y^2 + 2*x^3*y + x*y^2 + x^4 + y*x + y^2*x + y*x^2 + y^2 229.11/103.57 > 2*x + x*y + x*y*z + x*y^2 + x*z + x^2 229.11/103.57 = [c_2(f^#(x, f(y, z)))] 229.11/103.57 229.11/103.57 [f^#(0(), y)] = 2 + y 229.11/103.57 > y 229.11/103.57 = [c_3(y)] 229.11/103.57 229.11/103.57 [f^#(i(x), y)] = 229.11/103.57 >= 229.11/103.57 = [c_4(x)] 229.11/103.57 229.11/103.57 [f^#(g(x, y), z)] = 6 + 5*x + 5*y + 2*z + x*z + y*z + x^2 + x*y + y*x + y^2 229.11/103.57 > 1 + x + x*z + x^2 + y + y*z + y^2 229.11/103.57 = [c_5(f^#(x, z), f^#(y, z))] 229.11/103.57 229.11/103.57 [f^#(1(), g(x, y))] = 4 + x + y 229.11/103.57 > 2 + x 229.11/103.57 = [c_6(x)] 229.11/103.57 229.11/103.57 [f^#(2(), g(x, y))] = 4 + x + y 229.11/103.57 > 2 + y 229.11/103.57 = [c_7(y)] 229.11/103.57 229.11/103.57 229.11/103.57 The strictly oriented rules are moved into the weak component. 229.11/103.57 229.11/103.57 We are left with following problem, upon which TcT provides the 229.11/103.57 certificate YES(O(1),O(1)). 229.11/103.57 229.11/103.57 Weak DPs: 229.11/103.57 { f^#(x, 0()) -> c_1(x) 229.11/103.57 , f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) 229.11/103.57 , f^#(0(), y) -> c_3(y) 229.11/103.57 , f^#(i(x), y) -> c_4(x) 229.11/103.57 , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.57 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.57 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.57 Weak Trs: 229.11/103.57 { f(x, 0()) -> x 229.11/103.57 , f(f(x, y), z) -> f(x, f(y, z)) 229.11/103.57 , f(0(), y) -> y 229.11/103.57 , f(i(x), y) -> i(x) 229.11/103.57 , f(g(x, y), z) -> g(f(x, z), f(y, z)) 229.11/103.57 , f(1(), g(x, y)) -> x 229.11/103.57 , f(2(), g(x, y)) -> y } 229.11/103.57 Obligation: 229.11/103.57 runtime complexity 229.11/103.57 Answer: 229.11/103.57 YES(O(1),O(1)) 229.11/103.57 229.11/103.57 The following weak DPs constitute a sub-graph of the DG that is 229.11/103.57 closed under successors. The DPs are removed. 229.11/103.57 229.11/103.57 { f^#(x, 0()) -> c_1(x) 229.11/103.57 , f^#(f(x, y), z) -> c_2(f^#(x, f(y, z))) 229.11/103.57 , f^#(0(), y) -> c_3(y) 229.11/103.57 , f^#(i(x), y) -> c_4(x) 229.11/103.57 , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) 229.11/103.57 , f^#(1(), g(x, y)) -> c_6(x) 229.11/103.57 , f^#(2(), g(x, y)) -> c_7(y) } 229.11/103.57 229.11/103.57 We are left with following problem, upon which TcT provides the 229.11/103.57 certificate YES(O(1),O(1)). 229.11/103.57 229.11/103.57 Weak Trs: 229.11/103.57 { f(x, 0()) -> x 229.11/103.57 , f(f(x, y), z) -> f(x, f(y, z)) 229.11/103.57 , f(0(), y) -> y 229.11/103.57 , f(i(x), y) -> i(x) 229.11/103.57 , f(g(x, y), z) -> g(f(x, z), f(y, z)) 229.11/103.57 , f(1(), g(x, y)) -> x 229.11/103.57 , f(2(), g(x, y)) -> y } 229.11/103.57 Obligation: 229.11/103.57 runtime complexity 229.11/103.57 Answer: 229.11/103.57 YES(O(1),O(1)) 229.11/103.57 229.11/103.57 No rule is usable, rules are removed from the input problem. 229.11/103.57 229.11/103.57 We are left with following problem, upon which TcT provides the 229.11/103.57 certificate YES(O(1),O(1)). 229.11/103.57 229.11/103.57 Rules: Empty 229.11/103.57 Obligation: 229.11/103.57 runtime complexity 229.11/103.57 Answer: 229.11/103.57 YES(O(1),O(1)) 229.11/103.57 229.11/103.57 Empty rules are trivially bounded 229.11/103.57 229.11/103.57 Hurray, we answered YES(O(1),O(n^2)) 229.31/103.63 EOF