YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { f(x, 0()) -> x , f(f(x, y), z) -> f(x, f(y, z)) , f(0(), y) -> y , f(i(x), y) -> i(x) , f(g(x, y), z) -> g(f(x, z), f(y, z)) , f(1(), g(x, y)) -> x , f(2(), g(x, y)) -> y } Obligation: runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { f(1(), g(x, y)) -> x , f(2(), g(x, y)) -> y } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(f) = {2}, Uargs(g) = {1, 2} TcT has computed the following constructor-restricted polynomial interpretation. [f](x1, x2) = x1 + x1*x2 + x2 [0]() = 0 [i](x1) = 0 [g](x1, x2) = 1 + x1 + x2 [1]() = 0 [2]() = 0 The following symbols are considered usable {f} This order satisfies the following ordering constraints. [f(x, 0())] = x >= x = [x] [f(f(x, y), z)] = x + x*y + y + x*z + x*y*z + y*z + z >= x + x*y + x*y*z + x*z + y + y*z + z = [f(x, f(y, z))] [f(0(), y)] = y >= y = [y] [f(i(x), y)] = y >= = [i(x)] [f(g(x, y), z)] = 1 + x + y + 2*z + x*z + y*z >= 1 + x + x*z + 2*z + y + y*z = [g(f(x, z), f(y, z))] [f(1(), g(x, y))] = 1 + x + y > x = [x] [f(2(), g(x, y))] = 1 + x + y > y = [y] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { f(x, 0()) -> x , f(f(x, y), z) -> f(x, f(y, z)) , f(0(), y) -> y , f(i(x), y) -> i(x) , f(g(x, y), z) -> g(f(x, z), f(y, z)) } Weak Trs: { f(1(), g(x, y)) -> x , f(2(), g(x, y)) -> y } Obligation: runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { f(g(x, y), z) -> g(f(x, z), f(y, z)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(f) = {2}, Uargs(g) = {1, 2} TcT has computed the following constructor-restricted polynomial interpretation. [f](x1, x2) = x1 + x1*x2 + 2*x1^2 + x2 [0]() = 0 [i](x1) = 0 [g](x1, x2) = 1 + x1 + x2 [1]() = 0 [2]() = 0 The following symbols are considered usable {f} This order satisfies the following ordering constraints. [f(x, 0())] = x + 2*x^2 >= x = [x] [f(f(x, y), z)] = x + 3*x*y + 4*x^2 + y + x*z + x*y*z + 2*x^2*z + y*z + 8*x^2*y + 8*x^3 + 2*x^2*y^2 + 8*x^3*y + 2*x*y^2 + 8*x^4 + 2*y*x + 2*y^2*x + 4*y*x^2 + 2*y^2 + z >= x + x*y + x*y*z + 2*x*y^2 + x*z + 2*x^2 + y + y*z + 2*y^2 + z = [f(x, f(y, z))] [f(0(), y)] = y >= y = [y] [f(i(x), y)] = y >= = [i(x)] [f(g(x, y), z)] = 3 + 5*x + 5*y + 2*z + x*z + y*z + 2*x^2 + 2*x*y + 2*y*x + 2*y^2 > 1 + x + x*z + 2*x^2 + 2*z + y + y*z + 2*y^2 = [g(f(x, z), f(y, z))] [f(1(), g(x, y))] = 1 + x + y > x = [x] [f(2(), g(x, y))] = 1 + x + y > y = [y] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { f(x, 0()) -> x , f(f(x, y), z) -> f(x, f(y, z)) , f(0(), y) -> y , f(i(x), y) -> i(x) } Weak Trs: { f(g(x, y), z) -> g(f(x, z), f(y, z)) , f(1(), g(x, y)) -> x , f(2(), g(x, y)) -> y } Obligation: runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { f(i(x), y) -> i(x) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(f) = {2}, Uargs(g) = {1, 2} TcT has computed the following constructor-restricted polynomial interpretation. [f](x1, x2) = x1 + x1*x2 + 2*x1^2 + x2 [0]() = 0 [i](x1) = 1 [g](x1, x2) = 1 + x1 + x2 [1]() = 0 [2]() = 0 The following symbols are considered usable {f} This order satisfies the following ordering constraints. [f(x, 0())] = x + 2*x^2 >= x = [x] [f(f(x, y), z)] = x + 3*x*y + 4*x^2 + y + x*z + x*y*z + 2*x^2*z + y*z + 8*x^2*y + 8*x^3 + 2*x^2*y^2 + 8*x^3*y + 2*x*y^2 + 8*x^4 + 2*y*x + 2*y^2*x + 4*y*x^2 + 2*y^2 + z >= x + x*y + x*y*z + 2*x*y^2 + x*z + 2*x^2 + y + y*z + 2*y^2 + z = [f(x, f(y, z))] [f(0(), y)] = y >= y = [y] [f(i(x), y)] = 3 + 2*y > 1 = [i(x)] [f(g(x, y), z)] = 3 + 5*x + 5*y + 2*z + x*z + y*z + 2*x^2 + 2*x*y + 2*y*x + 2*y^2 > 1 + x + x*z + 2*x^2 + 2*z + y + y*z + 2*y^2 = [g(f(x, z), f(y, z))] [f(1(), g(x, y))] = 1 + x + y > x = [x] [f(2(), g(x, y))] = 1 + x + y > y = [y] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { f(x, 0()) -> x , f(f(x, y), z) -> f(x, f(y, z)) , f(0(), y) -> y } Weak Trs: { f(i(x), y) -> i(x) , f(g(x, y), z) -> g(f(x, z), f(y, z)) , f(1(), g(x, y)) -> x , f(2(), g(x, y)) -> y } Obligation: runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { f(x, 0()) -> x , f(0(), y) -> y } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(f) = {2}, Uargs(g) = {1, 2} TcT has computed the following constructor-restricted polynomial interpretation. [f](x1, x2) = x1 + x1*x2 + x2 [0]() = 1 [i](x1) = 0 [g](x1, x2) = 1 + x1 + x2 [1]() = 0 [2]() = 0 The following symbols are considered usable {f} This order satisfies the following ordering constraints. [f(x, 0())] = 2*x + 1 > x = [x] [f(f(x, y), z)] = x + x*y + y + x*z + x*y*z + y*z + z >= x + x*y + x*y*z + x*z + y + y*z + z = [f(x, f(y, z))] [f(0(), y)] = 1 + 2*y > y = [y] [f(i(x), y)] = y >= = [i(x)] [f(g(x, y), z)] = 1 + x + y + 2*z + x*z + y*z >= 1 + x + x*z + 2*z + y + y*z = [g(f(x, z), f(y, z))] [f(1(), g(x, y))] = 1 + x + y > x = [x] [f(2(), g(x, y))] = 1 + x + y > y = [y] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { f(f(x, y), z) -> f(x, f(y, z)) } Weak Trs: { f(x, 0()) -> x , f(0(), y) -> y , f(i(x), y) -> i(x) , f(g(x, y), z) -> g(f(x, z), f(y, z)) , f(1(), g(x, y)) -> x , f(2(), g(x, y)) -> y } Obligation: runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { f(f(x, y), z) -> f(x, f(y, z)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(f) = {2}, Uargs(g) = {1, 2} TcT has computed the following constructor-restricted polynomial interpretation. [f](x1, x2) = 2 + 2*x1 + x1*x2 + x2 [0]() = 0 [i](x1) = 0 [g](x1, x2) = 2 + x1 + x2 [1]() = 0 [2]() = 0 The following symbols are considered usable {f} This order satisfies the following ordering constraints. [f(x, 0())] = 2 + 2*x > x = [x] [f(f(x, y), z)] = 6 + 4*x + 2*x*y + 2*y + 3*z + 2*x*z + x*y*z + y*z > 4 + 4*x + 2*x*y + x*y*z + x*z + 2*y + y*z + z = [f(x, f(y, z))] [f(0(), y)] = 2 + y > y = [y] [f(i(x), y)] = 2 + y > = [i(x)] [f(g(x, y), z)] = 6 + 2*x + 2*y + 3*z + x*z + y*z >= 6 + 2*x + x*z + 2*z + 2*y + y*z = [g(f(x, z), f(y, z))] [f(1(), g(x, y))] = 4 + x + y > x = [x] [f(2(), g(x, y))] = 4 + x + y > y = [y] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { f(x, 0()) -> x , f(f(x, y), z) -> f(x, f(y, z)) , f(0(), y) -> y , f(i(x), y) -> i(x) , f(g(x, y), z) -> g(f(x, z), f(y, z)) , f(1(), g(x, y)) -> x , f(2(), g(x, y)) -> y } Obligation: runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))