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