YES(O(1),O(1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict Trs: { f1() -> g1() , f1() -> g2() , g1() -> h1() , g1() -> h2() , g2() -> h1() , g2() -> h2() , f2() -> g1() , f2() -> g2() , h1() -> i() , h2() -> i() , e1(x1, x1, x, y, z) -> e5(x1, x, y, z) , e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z) , e2(x, x, y, z, z) -> e6(x, y, z) , e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z) , e2(i(), x, y, z, i()) -> e6(x, y, z) , e5(i(), x, y, z) -> e6(x, y, z) , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) , e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z) , e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x) , e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) -> e1(x1, x1, x, y, z) , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> e5(x1, x, y, z) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Arguments of following rules are not normal-forms: { e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z) , e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z) , e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) -> e1(x1, x1, x, y, z) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict Trs: { f1() -> g1() , f1() -> g2() , g1() -> h1() , g1() -> h2() , g2() -> h1() , g2() -> h2() , f2() -> g1() , f2() -> g2() , h1() -> i() , h2() -> i() , e1(x1, x1, x, y, z) -> e5(x1, x, y, z) , e2(x, x, y, z, z) -> e6(x, y, z) , e2(i(), x, y, z, i()) -> e6(x, y, z) , e5(i(), x, y, z) -> e6(x, y, z) , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) , e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z) , e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x) , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> e5(x1, x, y, z) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We add the following innermost weak dependency pairs: Strict DPs: { f1^#() -> c_1(g1^#()) , f1^#() -> c_2(g2^#()) , g1^#() -> c_3(h1^#()) , g1^#() -> c_4(h2^#()) , g2^#() -> c_5(h1^#()) , g2^#() -> c_6(h2^#()) , h1^#() -> c_9() , h2^#() -> c_10() , f2^#() -> c_7(g1^#()) , f2^#() -> c_8(g2^#()) , e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , e5^#(i(), x, y, z) -> c_14() , e2^#(x, x, y, z, z) -> c_12() , e2^#(i(), x, y, z, i()) -> c_13() , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) , e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f1^#() -> c_1(g1^#()) , f1^#() -> c_2(g2^#()) , g1^#() -> c_3(h1^#()) , g1^#() -> c_4(h2^#()) , g2^#() -> c_5(h1^#()) , g2^#() -> c_6(h2^#()) , h1^#() -> c_9() , h2^#() -> c_10() , f2^#() -> c_7(g1^#()) , f2^#() -> c_8(g2^#()) , e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , e5^#(i(), x, y, z) -> c_14() , e2^#(x, x, y, z, z) -> c_12() , e2^#(i(), x, y, z, i()) -> c_13() , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) , e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } Strict Trs: { f1() -> g1() , f1() -> g2() , g1() -> h1() , g1() -> h2() , g2() -> h1() , g2() -> h2() , f2() -> g1() , f2() -> g2() , h1() -> i() , h2() -> i() , e1(x1, x1, x, y, z) -> e5(x1, x, y, z) , e2(x, x, y, z, z) -> e6(x, y, z) , e2(i(), x, y, z, i()) -> e6(x, y, z) , e5(i(), x, y, z) -> e6(x, y, z) , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) , e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z) , e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x) , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> e5(x1, x, y, z) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f1^#() -> c_1(g1^#()) , f1^#() -> c_2(g2^#()) , g1^#() -> c_3(h1^#()) , g1^#() -> c_4(h2^#()) , g2^#() -> c_5(h1^#()) , g2^#() -> c_6(h2^#()) , h1^#() -> c_9() , h2^#() -> c_10() , f2^#() -> c_7(g1^#()) , f2^#() -> c_8(g2^#()) , e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , e5^#(i(), x, y, z) -> c_14() , e2^#(x, x, y, z, z) -> c_12() , e2^#(i(), x, y, z, i()) -> c_13() , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) , e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_11) = {1}, Uargs(c_15) = {1}, Uargs(c_18) = {1} TcT has computed the following constructor-restricted matrix interpretation. [i] = [1] [1] [f1^#] = [1] [1] [c_1](x1) = [1 0] x1 + [1] [0 1] [1] [g1^#] = [1] [1] [c_2](x1) = [1 0] x1 + [2] [0 1] [2] [g2^#] = [1] [1] [c_3](x1) = [1 0] x1 + [2] [0 1] [1] [h1^#] = [1] [1] [c_4](x1) = [1 0] x1 + [2] [0 1] [2] [h2^#] = [1] [1] [c_5](x1) = [1 0] x1 + [1] [0 1] [2] [c_6](x1) = [1 0] x1 + [1] [0 1] [1] [f2^#] = [2] [1] [c_7](x1) = [1 0] x1 + [2] [0 1] [2] [c_8](x1) = [1 0] x1 + [1] [0 1] [1] [c_9] = [0] [1] [c_10] = [0] [1] [e1^#](x1, x2, x3, x4, x5) = [2 2] x1 + [2 2] x2 + [1 1] x3 + [2 2] x4 + [1 1] x5 + [2] [2 2] [2 1] [2 2] [1 1] [1 2] [1] [c_11](x1) = [1 0] x1 + [1] [0 1] [1] [e5^#](x1, x2, x3, x4) = [2 2] x1 + [1 1] x2 + [1 1] x3 + [1 1] x4 + [2] [2 2] [1 2] [2 2] [2 2] [2] [e2^#](x1, x2, x3, x4, x5) = [1 2] x1 + [2 2] x5 + [0] [1 2] [2 2] [0] [c_12] = [1] [0] [c_13] = [2] [1] [c_14] = [1] [1] [e3^#](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1 1] x1 + [1 1] x2 + [1 1] x3 + [1 1] x4 + [2 2] x5 + [2 2] x6 + [2 2] x7 + [1 2] x8 + [1 2] x9 + [2 1] x10 + [2 1] x11 + [1] [2 2] [2 1] [2 1] [1 2] [1 1] [2 2] [2 2] [1 2] [2 1] [2 1] [1 1] [2] [c_15](x1) = [1 0] x1 + [2] [0 1] [2] [e4^#](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [2 2] x2 + [0 1] x3 + [1 1] x4 + [2 2] x5 + [1 2] x6 + [1 1] x7 + [2 1] x8 + [1 1] x9 + [1 1] x10 + [1 1] x11 + [0] [2 1] [0 1] [2 1] [2 1] [1 1] [1 2] [1 1] [2 2] [2 2] [2 2] [0] [c_16] = [0] [1] [c_17] = [2] [0] [c_18](x1) = [1 0] x1 + [1] [0 1] [1] The following symbols are considered usable {f1^#, g1^#, g2^#, h1^#, h2^#, f2^#, e1^#, e5^#, e2^#, e3^#, e4^#} The order satisfies the following ordering constraints: [f1^#()] = [1] [1] ? [2] [2] = [c_1(g1^#())] [f1^#()] = [1] [1] ? [3] [3] = [c_2(g2^#())] [g1^#()] = [1] [1] ? [3] [2] = [c_3(h1^#())] [g1^#()] = [1] [1] ? [3] [3] = [c_4(h2^#())] [g2^#()] = [1] [1] ? [2] [3] = [c_5(h1^#())] [g2^#()] = [1] [1] ? [2] [2] = [c_6(h2^#())] [h1^#()] = [1] [1] > [0] [1] = [c_9()] [h2^#()] = [1] [1] > [0] [1] = [c_10()] [f2^#()] = [2] [1] ? [3] [3] = [c_7(g1^#())] [f2^#()] = [2] [1] ? [2] [2] = [c_8(g2^#())] [e1^#(x1, x1, x, y, z)] = [1 1] x + [2 2] y + [1 1] z + [4 4] x1 + [2] [2 2] [1 1] [1 2] [4 3] [1] ? [1 1] x + [1 1] y + [1 1] z + [2 2] x1 + [3] [1 2] [2 2] [2 2] [2 2] [3] = [c_11(e5^#(x1, x, y, z))] [e5^#(i(), x, y, z)] = [1 1] x + [1 1] y + [1 1] z + [6] [1 2] [2 2] [2 2] [6] > [1] [1] = [c_14()] [e2^#(x, x, y, z, z)] = [1 2] x + [2 2] z + [0] [1 2] [2 2] [0] ? [1] [0] = [c_12()] [e2^#(i(), x, y, z, i())] = [7] [7] > [2] [1] = [c_13()] [e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)] = [1 2] x + [2 1] y + [2 1] z + [2 2] x1 + [2 2] x2 + [4 4] x3 + [3 4] x4 + [1] [2 1] [2 1] [1 1] [4 3] [3 3] [3 3] [3 4] [2] ? [1 1] x + [1 1] y + [1 1] z + [2 2] x1 + [1 2] x2 + [3 4] x3 + [3 2] x4 + [2] [2 2] [2 2] [2 2] [2 1] [2 2] [3 2] [2 3] [2] = [c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))] [e3^#(x, y, x, y, y, z, y, z, x, y, z)] = [3 4] x + [8 7] y + [5 5] z + [1] [6 4] [8 7] [4 5] [2] > [0] [1] = [c_16()] [e4^#(x, x, x, x, x, x, x, x, x, x, x)] = [12 13] x + [0] [15 14] [0] ? [2] [0] = [c_17()] [e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z)] = [1 1] x + [1 1] y + [1 1] z + [6 6] x1 + [7] [2 2] [2 2] [2 2] [6 4] [7] > [1 1] x + [1 1] y + [1 1] z + [2 2] x1 + [3] [1 2] [2 2] [2 2] [2 2] [3] = [c_18(e5^#(x1, x, y, z))] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f1^#() -> c_1(g1^#()) , f1^#() -> c_2(g2^#()) , g1^#() -> c_3(h1^#()) , g1^#() -> c_4(h2^#()) , g2^#() -> c_5(h1^#()) , g2^#() -> c_6(h2^#()) , f2^#() -> c_7(g1^#()) , f2^#() -> c_8(g2^#()) , e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , e2^#(x, x, y, z, z) -> c_12() , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) , e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() } Weak DPs: { h1^#() -> c_9() , h2^#() -> c_10() , e5^#(i(), x, y, z) -> c_14() , e2^#(i(), x, y, z, i()) -> c_13() , e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {3,4,5,6,9,10,12} by applications of Pre({3,4,5,6,9,10,12}) = {1,2,7,8,11}. Here rules are labeled as follows: DPs: { 1: f1^#() -> c_1(g1^#()) , 2: f1^#() -> c_2(g2^#()) , 3: g1^#() -> c_3(h1^#()) , 4: g1^#() -> c_4(h2^#()) , 5: g2^#() -> c_5(h1^#()) , 6: g2^#() -> c_6(h2^#()) , 7: f2^#() -> c_7(g1^#()) , 8: f2^#() -> c_8(g2^#()) , 9: e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , 10: e2^#(x, x, y, z, z) -> c_12() , 11: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) , 12: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() , 13: h1^#() -> c_9() , 14: h2^#() -> c_10() , 15: e5^#(i(), x, y, z) -> c_14() , 16: e2^#(i(), x, y, z, i()) -> c_13() , 17: e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , 18: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f1^#() -> c_1(g1^#()) , f1^#() -> c_2(g2^#()) , f2^#() -> c_7(g1^#()) , f2^#() -> c_8(g2^#()) , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) } Weak DPs: { g1^#() -> c_3(h1^#()) , g1^#() -> c_4(h2^#()) , g2^#() -> c_5(h1^#()) , g2^#() -> c_6(h2^#()) , h1^#() -> c_9() , h2^#() -> c_10() , e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , e5^#(i(), x, y, z) -> c_14() , e2^#(x, x, y, z, z) -> c_12() , e2^#(i(), x, y, z, i()) -> c_13() , e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {1,2,3,4,5} by applications of Pre({1,2,3,4,5}) = {}. Here rules are labeled as follows: DPs: { 1: f1^#() -> c_1(g1^#()) , 2: f1^#() -> c_2(g2^#()) , 3: f2^#() -> c_7(g1^#()) , 4: f2^#() -> c_8(g2^#()) , 5: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) , 6: g1^#() -> c_3(h1^#()) , 7: g1^#() -> c_4(h2^#()) , 8: g2^#() -> c_5(h1^#()) , 9: g2^#() -> c_6(h2^#()) , 10: h1^#() -> c_9() , 11: h2^#() -> c_10() , 12: e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , 13: e5^#(i(), x, y, z) -> c_14() , 14: e2^#(x, x, y, z, z) -> c_12() , 15: e2^#(i(), x, y, z, i()) -> c_13() , 16: e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , 17: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() , 18: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { f1^#() -> c_1(g1^#()) , f1^#() -> c_2(g2^#()) , g1^#() -> c_3(h1^#()) , g1^#() -> c_4(h2^#()) , g2^#() -> c_5(h1^#()) , g2^#() -> c_6(h2^#()) , h1^#() -> c_9() , h2^#() -> c_10() , f2^#() -> c_7(g1^#()) , f2^#() -> c_8(g2^#()) , e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , e5^#(i(), x, y, z) -> c_14() , e2^#(x, x, y, z, z) -> c_12() , e2^#(i(), x, y, z, i()) -> c_13() , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) , e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { f1^#() -> c_1(g1^#()) , f1^#() -> c_2(g2^#()) , g1^#() -> c_3(h1^#()) , g1^#() -> c_4(h2^#()) , g2^#() -> c_5(h1^#()) , g2^#() -> c_6(h2^#()) , h1^#() -> c_9() , h2^#() -> c_10() , f2^#() -> c_7(g1^#()) , f2^#() -> c_8(g2^#()) , e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z)) , e5^#(i(), x, y, z) -> c_14() , e2^#(x, x, y, z, z) -> c_12() , e2^#(i(), x, y, z, i()) -> c_13() , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) , e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() , e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17() , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_18(e5^#(x1, x, y, z)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(1))