YES(O(1),O(1)) 114.28/47.02 YES(O(1),O(1)) 114.28/47.02 114.28/47.02 We are left with following problem, upon which TcT provides the 114.28/47.02 certificate YES(O(1),O(1)). 114.28/47.02 114.28/47.02 Strict Trs: 114.28/47.02 { f1(x, a()) -> g2(x, x) 114.28/47.02 , f1(a(), x) -> g1(x, x) 114.28/47.02 , g1(x, a()) -> h2(x) 114.28/47.02 , g1(a(), x) -> h1(x) 114.28/47.02 , g2(x, a()) -> h2(x) 114.28/47.02 , g2(a(), x) -> h1(x) 114.28/47.02 , f2(x, a()) -> g2(x, x) 114.28/47.02 , f2(a(), x) -> g1(x, x) 114.28/47.02 , h1(a()) -> i() 114.28/47.02 , h2(a()) -> i() 114.28/47.02 , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z) 114.28/47.02 , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w) 114.28/47.02 , e2(x, x, y, z, z, a()) -> e6(x, y, z) 114.28/47.02 , e2(f1(w, w), x, y, z, f2(w, w), w) -> 114.28/47.02 e3(x, y, x, y, y, z, y, z, x, y, z, w) 114.28/47.02 , e2(i(), x, y, z, i(), a()) -> e6(x, y, z) 114.28/47.02 , e5(i(), x, y, z) -> e6(x, y, z) 114.28/47.02 , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.02 e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) 114.28/47.02 , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z) 114.28/47.02 , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x) 114.28/47.02 , e4(g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 x, 114.28/47.02 y, 114.28/47.02 z, 114.28/47.02 w) 114.28/47.02 -> e1(x1, x1, x, y, z, w) 114.28/47.02 , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.02 e5(x1, x, y, z) } 114.28/47.02 Obligation: 114.28/47.02 innermost runtime complexity 114.28/47.02 Answer: 114.28/47.02 YES(O(1),O(1)) 114.28/47.02 114.28/47.02 We add the following weak dependency pairs: 114.28/47.02 114.28/47.02 Strict DPs: 114.28/47.02 { f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.02 , f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.02 , g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.02 , g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.02 , g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.02 , g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.02 , h2^#(a()) -> c_10() 114.28/47.02 , h1^#(a()) -> c_9() 114.28/47.02 , f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.02 , f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.02 , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.02 , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) 114.28/47.02 , e5^#(i(), x, y, z) -> c_16() 114.28/47.02 , e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.02 , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> 114.28/47.02 c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) 114.28/47.02 , e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.02 , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.02 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.02 , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() 114.28/47.02 , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.02 , e4^#(g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 x, 114.28/47.02 y, 114.28/47.02 z, 114.28/47.02 w) 114.28/47.02 -> c_20(e1^#(x1, x1, x, y, z, w)) 114.28/47.02 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.02 c_21(e5^#(x1, x, y, z)) } 114.28/47.02 114.28/47.02 and mark the set of starting terms. 114.28/47.02 114.28/47.02 We are left with following problem, upon which TcT provides the 114.28/47.02 certificate YES(O(1),O(1)). 114.28/47.02 114.28/47.02 Strict DPs: 114.28/47.02 { f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.02 , f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.02 , g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.02 , g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.02 , g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.02 , g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.02 , h2^#(a()) -> c_10() 114.28/47.02 , h1^#(a()) -> c_9() 114.28/47.02 , f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.02 , f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.02 , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.02 , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) 114.28/47.02 , e5^#(i(), x, y, z) -> c_16() 114.28/47.02 , e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.02 , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> 114.28/47.02 c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) 114.28/47.02 , e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.02 , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.02 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.02 , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() 114.28/47.02 , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.02 , e4^#(g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 x, 114.28/47.02 y, 114.28/47.02 z, 114.28/47.02 w) 114.28/47.02 -> c_20(e1^#(x1, x1, x, y, z, w)) 114.28/47.02 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.02 c_21(e5^#(x1, x, y, z)) } 114.28/47.02 Strict Trs: 114.28/47.02 { f1(x, a()) -> g2(x, x) 114.28/47.02 , f1(a(), x) -> g1(x, x) 114.28/47.02 , g1(x, a()) -> h2(x) 114.28/47.02 , g1(a(), x) -> h1(x) 114.28/47.02 , g2(x, a()) -> h2(x) 114.28/47.02 , g2(a(), x) -> h1(x) 114.28/47.02 , f2(x, a()) -> g2(x, x) 114.28/47.02 , f2(a(), x) -> g1(x, x) 114.28/47.02 , h1(a()) -> i() 114.28/47.02 , h2(a()) -> i() 114.28/47.02 , e1(x1, x1, x, y, z, a()) -> e5(x1, x, y, z) 114.28/47.02 , e1(h1(w), h2(w), x, y, z, w) -> e2(x, x, y, z, z, w) 114.28/47.02 , e2(x, x, y, z, z, a()) -> e6(x, y, z) 114.28/47.02 , e2(f1(w, w), x, y, z, f2(w, w), w) -> 114.28/47.02 e3(x, y, x, y, y, z, y, z, x, y, z, w) 114.28/47.02 , e2(i(), x, y, z, i(), a()) -> e6(x, y, z) 114.28/47.02 , e5(i(), x, y, z) -> e6(x, y, z) 114.28/47.02 , e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.02 e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) 114.28/47.02 , e3(x, y, x, y, y, z, y, z, x, y, z, a()) -> e6(x, y, z) 114.28/47.02 , e4(x, x, x, x, x, x, x, x, x, x, x, a()) -> e6(x, x, x) 114.28/47.02 , e4(g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 x, 114.28/47.02 y, 114.28/47.02 z, 114.28/47.02 w) 114.28/47.02 -> e1(x1, x1, x, y, z, w) 114.28/47.02 , e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.02 e5(x1, x, y, z) } 114.28/47.02 Obligation: 114.28/47.02 innermost runtime complexity 114.28/47.02 Answer: 114.28/47.02 YES(O(1),O(1)) 114.28/47.02 114.28/47.02 No rule is usable, rules are removed from the input problem. 114.28/47.02 114.28/47.02 We are left with following problem, upon which TcT provides the 114.28/47.02 certificate YES(O(1),O(1)). 114.28/47.02 114.28/47.02 Strict DPs: 114.28/47.02 { f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.02 , f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.02 , g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.02 , g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.02 , g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.02 , g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.02 , h2^#(a()) -> c_10() 114.28/47.02 , h1^#(a()) -> c_9() 114.28/47.02 , f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.02 , f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.02 , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.02 , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) 114.28/47.02 , e5^#(i(), x, y, z) -> c_16() 114.28/47.02 , e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.02 , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> 114.28/47.02 c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) 114.28/47.02 , e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.02 , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.02 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.02 , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() 114.28/47.02 , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.02 , e4^#(g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 g1(w, w), 114.28/47.02 x1, 114.28/47.02 g2(w, w), 114.28/47.02 x1, 114.28/47.02 x, 114.28/47.02 y, 114.28/47.02 z, 114.28/47.02 w) 114.28/47.02 -> c_20(e1^#(x1, x1, x, y, z, w)) 114.28/47.02 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.02 c_21(e5^#(x1, x, y, z)) } 114.28/47.02 Obligation: 114.28/47.02 innermost runtime complexity 114.28/47.02 Answer: 114.28/47.02 YES(O(1),O(1)) 114.28/47.02 114.28/47.02 The weightgap principle applies (using the following constant 114.28/47.02 growth matrix-interpretation) 114.28/47.02 114.28/47.02 The following argument positions are usable: 114.28/47.02 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 114.28/47.02 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 114.28/47.02 Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_11) = {1}, 114.28/47.02 Uargs(c_12) = {1}, Uargs(c_14) = {1}, Uargs(c_17) = {1}, 114.28/47.02 Uargs(c_20) = {1}, Uargs(c_21) = {1} 114.28/47.02 114.28/47.02 TcT has computed the following constructor-restricted matrix 114.28/47.02 interpretation. 114.28/47.02 114.28/47.02 [f1](x1, x2) = [0] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [a] = [0] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [g1](x1, x2) = [0] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [g2](x1, x2) = [0] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [f2](x1, x2) = [0] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [h1](x1) = [0] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [h2](x1) = [0] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [i] = [0] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [f1^#](x1, x2) = [1 114.28/47.02 2] x1 + [1 1] x2 + [2] 114.28/47.02 [2 114.28/47.02 1] [1 1] [2] 114.28/47.02 114.28/47.02 [c_1](x1) = [1 114.28/47.02 0] x1 + [2] 114.28/47.02 [0 114.28/47.02 1] [0] 114.28/47.02 114.28/47.02 [g2^#](x1, x2) = [1 114.28/47.02 1] x1 + [0 0] x2 + [2] 114.28/47.02 [1 114.28/47.02 2] [1 2] [2] 114.28/47.02 114.28/47.02 [c_2](x1) = [1 114.28/47.02 0] x1 + [2] 114.28/47.02 [0 114.28/47.02 1] [1] 114.28/47.02 114.28/47.02 [g1^#](x1, x2) = [1 114.28/47.02 1] x1 + [0 0] x2 + [2] 114.28/47.02 [1 114.28/47.02 2] [1 2] [2] 114.28/47.02 114.28/47.02 [c_3](x1) = [1 114.28/47.02 0] x1 + [2] 114.28/47.02 [0 114.28/47.02 1] [1] 114.28/47.02 114.28/47.02 [h2^#](x1) = [1 114.28/47.02 1] x1 + [2] 114.28/47.02 [1 114.28/47.02 1] [1] 114.28/47.02 114.28/47.02 [c_4](x1) = [1 114.28/47.02 0] x1 + [0] 114.28/47.02 [0 114.28/47.02 1] [0] 114.28/47.02 114.28/47.02 [h1^#](x1) = [0 114.28/47.02 0] x1 + [1] 114.28/47.02 [1 114.28/47.02 1] [2] 114.28/47.02 114.28/47.02 [c_5](x1) = [1 114.28/47.02 0] x1 + [2] 114.28/47.02 [0 114.28/47.02 1] [1] 114.28/47.02 114.28/47.02 [c_6](x1) = [1 114.28/47.02 0] x1 + [0] 114.28/47.02 [0 114.28/47.02 1] [0] 114.28/47.02 114.28/47.02 [f2^#](x1, x2) = [1 114.28/47.02 1] x1 + [1 2] x2 + [2] 114.28/47.02 [1 114.28/47.02 1] [2 2] [2] 114.28/47.02 114.28/47.02 [c_7](x1) = [1 114.28/47.02 0] x1 + [2] 114.28/47.02 [0 114.28/47.02 1] [0] 114.28/47.02 114.28/47.02 [c_8](x1) = [1 114.28/47.02 0] x1 + [2] 114.28/47.02 [0 114.28/47.02 1] [0] 114.28/47.02 114.28/47.02 [c_9] = [0] 114.28/47.02 [1] 114.28/47.02 114.28/47.02 [c_10] = [1] 114.28/47.02 [1] 114.28/47.02 114.28/47.02 [e1^#](x1, x2, x3, x4, x5, x6) = [0 114.28/47.02 0] x3 + [0 0] x4 + [0 0] x5 + [2] 114.28/47.02 [2 114.28/47.02 2] [2 2] [2 2] [2] 114.28/47.02 114.28/47.02 [c_11](x1) = [1 114.28/47.02 0] x1 + [2] 114.28/47.02 [0 114.28/47.02 1] [1] 114.28/47.02 114.28/47.02 [e5^#](x1, x2, x3, x4) = [0 114.28/47.02 0] x1 + [0 0] x2 + [0 0] x3 + [0 114.28/47.02 0] x4 + [2] 114.28/47.02 [1 114.28/47.02 1] [1 2] [1 1] [1 114.28/47.02 2] [2] 114.28/47.02 114.28/47.02 [c_12](x1) = [1 114.28/47.02 0] x1 + [1] 114.28/47.02 [0 114.28/47.02 1] [2] 114.28/47.02 114.28/47.02 [e2^#](x1, x2, x3, x4, x5, x6) = [0 114.28/47.02 0] x2 + [0 0] x3 + [0 0] x4 + [0] 114.28/47.02 [2 114.28/47.02 2] [1 1] [2 2] [0] 114.28/47.02 114.28/47.02 [c_13] = [1] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [c_14](x1) = [1 114.28/47.02 0] x1 + [1] 114.28/47.02 [0 114.28/47.02 1] [1] 114.28/47.02 114.28/47.02 [e3^#](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = [0 114.28/47.02 0] x1 + [0 0] x2 + [0 0] x3 + [0 114.28/47.02 0] x4 + [0 114.28/47.02 0] x6 + [0 114.28/47.02 0] x7 + [0 114.28/47.02 0] x8 + [0 114.28/47.02 0] x9 + [0 114.28/47.02 0] x10 + [0 114.28/47.02 0] x11 + [0 114.28/47.02 0] x12 + [2] 114.28/47.02 [1 114.28/47.02 2] [2 2] [1 2] [1 114.28/47.02 1] [2 114.28/47.02 2] [2 114.28/47.02 2] [2 114.28/47.02 2] [2 114.28/47.02 2] [1 114.28/47.02 1] [2 114.28/47.02 2] [1 114.28/47.02 2] [2] 114.28/47.02 114.28/47.02 [c_15] = [1] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [c_16] = [1] 114.28/47.02 [1] 114.28/47.02 114.28/47.02 [c_17](x1) = [1 114.28/47.02 0] x1 + [1] 114.28/47.02 [0 114.28/47.02 1] [2] 114.28/47.02 114.28/47.02 [e4^#](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = [0 114.28/47.02 0] x2 + [0 0] x4 + [0 0] x6 + [0 114.28/47.02 0] x8 + [0 114.28/47.02 0] x9 + [0 114.28/47.02 0] x10 + [0 114.28/47.02 0] x11 + [0] 114.28/47.02 [1 114.28/47.02 1] [2 2] [2 2] [2 114.28/47.02 2] [2 114.28/47.02 1] [1 114.28/47.02 1] [2 114.28/47.02 2] [0] 114.28/47.02 114.28/47.02 [c_18] = [1] 114.28/47.02 [1] 114.28/47.02 114.28/47.02 [c_19] = [2] 114.28/47.02 [0] 114.28/47.02 114.28/47.02 [c_20](x1) = [1 114.28/47.02 0] x1 + [1] 114.28/47.02 [0 114.28/47.02 1] [2] 114.28/47.02 114.28/47.02 [c_21](x1) = [1 114.28/47.02 0] x1 + [1] 114.28/47.02 [0 114.28/47.02 1] [2] 114.28/47.02 114.28/47.02 The order satisfies the following ordering constraints: 114.28/47.02 114.28/47.02 [f1^#(x, a())] = [1 2] x + [2] 114.28/47.02 [2 1] [2] 114.28/47.02 ? [1 1] x + [4] 114.28/47.02 [2 4] [2] 114.28/47.02 = [c_1(g2^#(x, x))] 114.28/47.02 114.28/47.02 [f1^#(a(), x)] = [1 1] x + [2] 114.28/47.02 [1 1] [2] 114.28/47.02 ? [1 1] x + [4] 114.28/47.02 [2 4] [3] 114.28/47.02 = [c_2(g1^#(x, x))] 114.28/47.02 114.28/47.02 [g2^#(x, a())] = [1 1] x + [2] 114.28/47.02 [1 2] [2] 114.28/47.02 ? [1 1] x + [4] 114.28/47.02 [1 1] [2] 114.28/47.02 = [c_5(h2^#(x))] 114.28/47.02 114.28/47.02 [g2^#(a(), x)] = [0 0] x + [2] 114.28/47.02 [1 2] [2] 114.28/47.02 > [0 0] x + [1] 114.28/47.02 [1 1] [2] 114.28/47.02 = [c_6(h1^#(x))] 114.28/47.02 114.28/47.02 [g1^#(x, a())] = [1 1] x + [2] 114.28/47.02 [1 2] [2] 114.28/47.02 ? [1 1] x + [4] 114.28/47.02 [1 1] [2] 114.28/47.02 = [c_3(h2^#(x))] 114.28/47.02 114.28/47.02 [g1^#(a(), x)] = [0 0] x + [2] 114.28/47.02 [1 2] [2] 114.28/47.02 > [0 0] x + [1] 114.28/47.02 [1 1] [2] 114.28/47.02 = [c_4(h1^#(x))] 114.28/47.02 114.28/47.02 [h2^#(a())] = [2] 114.28/47.02 [1] 114.28/47.02 > [1] 114.28/47.02 [1] 114.28/47.02 = [c_10()] 114.28/47.02 114.28/47.02 [h1^#(a())] = [1] 114.28/47.02 [2] 114.28/47.02 > [0] 114.28/47.02 [1] 114.28/47.02 = [c_9()] 114.28/47.02 114.28/47.02 [f2^#(x, a())] = [1 1] x + [2] 114.28/47.02 [1 1] [2] 114.28/47.02 ? [1 1] x + [4] 114.28/47.02 [2 4] [2] 114.28/47.02 = [c_7(g2^#(x, x))] 114.28/47.02 114.28/47.02 [f2^#(a(), x)] = [1 2] x + [2] 114.28/47.02 [2 2] [2] 114.28/47.02 ? [1 1] x + [4] 114.28/47.02 [2 4] [2] 114.28/47.02 = [c_8(g1^#(x, x))] 114.28/47.02 114.28/47.02 [e1^#(x1, x1, x, y, z, a())] = [0 0] x + [0 0] y + [0 0] z + [2] 114.28/47.02 [2 2] [2 2] [2 2] [2] 114.28/47.02 ? [0 0] x + [0 0] y + [0 0] z + [0 0] x1 + [4] 114.28/47.02 [1 2] [1 1] [1 2] [1 1] [3] 114.28/47.02 = [c_11(e5^#(x1, x, y, z))] 114.28/47.02 114.28/47.02 [e1^#(h1(w), h2(w), x, y, z, w)] = [0 0] x + [0 0] y + [0 0] z + [2] 114.28/47.02 [2 2] [2 2] [2 2] [2] 114.28/47.02 > [0 0] x + [0 0] y + [0 0] z + [1] 114.28/47.02 [2 2] [1 1] [2 2] [2] 114.28/47.02 = [c_12(e2^#(x, x, y, z, z, w))] 114.28/47.02 114.28/47.02 [e5^#(i(), x, y, z)] = [0 0] x + [0 0] y + [0 0] z + [2] 114.28/47.02 [1 2] [1 1] [1 2] [2] 114.28/47.02 > [1] 114.28/47.02 [1] 114.28/47.02 = [c_16()] 114.28/47.02 114.28/47.02 [e2^#(x, x, y, z, z, a())] = [0 0] x + [0 0] y + [0 0] z + [0] 114.28/47.02 [2 2] [1 1] [2 2] [0] 114.28/47.02 ? [1] 114.28/47.02 [0] 114.28/47.02 = [c_13()] 114.28/47.02 114.28/47.02 [e2^#(f1(w, w), x, y, z, f2(w, w), w)] = [0 0] x + [0 0] y + [0 0] z + [0] 114.28/47.02 [2 2] [1 1] [2 2] [0] 114.28/47.02 ? [0 0] x + [0 0] w + [0 0] y + [0 0] z + [3] 114.28/47.02 [4 6] [1 2] [6 6] [6 6] [3] 114.28/47.02 = [c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w))] 114.28/47.02 114.28/47.02 [e2^#(i(), x, y, z, i(), a())] = [0 0] x + [0 0] y + [0 0] z + [0] 114.28/47.02 [2 2] [1 1] [2 2] [0] 114.28/47.02 ? [1] 114.28/47.02 [0] 114.28/47.02 = [c_15()] 114.28/47.02 114.28/47.02 [e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)] = [0 0] x + [0 0] w + [0 0] y + [0 0] z + [0 0] x1 + [0 0] x2 + [0 114.28/47.02 0] x3 + [0 0] x4 + [2] 114.28/47.02 [2 2] [1 2] [1 1] [2 2] [3 4] [2 3] [2 114.28/47.02 2] [4 4] [2] 114.28/47.02 > [0 0] x + [0 0] y + [0 0] z + [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 114.28/47.02 0] x4 + [1] 114.28/47.02 [2 1] [1 1] [2 2] [1 1] [2 2] [2 2] [2 114.28/47.02 2] [2] 114.28/47.02 = [c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w))] 114.28/47.02 114.28/47.02 [e3^#(x, y, x, y, y, z, y, z, x, y, z, a())] = [0 0] x + [0 0] y + [0 0] z + [2] 114.28/47.02 [4 6] [6 6] [6 6] [2] 114.28/47.02 > [1] 114.28/47.02 [1] 114.28/47.02 = [c_18()] 114.28/47.03 114.28/47.03 [e4^#(x, x, x, x, x, x, x, x, x, x, x, a())] = [ 0 0] x + [0] 114.28/47.03 [12 11] [0] 114.28/47.03 ? [2] 114.28/47.03 [0] 114.28/47.03 = [c_19()] 114.28/47.03 114.28/47.03 [e4^#(g1(w, w), = [0 0] x + [0 0] y + [0 0] z + [0 0] x1 + [0] 114.28/47.03 x1, [2 1] [1 1] [2 2] [7 7] [0] 114.28/47.03 g2(w, w), 114.28/47.03 x1, 114.28/47.03 g1(w, w), 114.28/47.03 x1, 114.28/47.03 g2(w, w), 114.28/47.03 x1, 114.28/47.03 x, 114.28/47.03 y, 114.28/47.03 z, 114.28/47.03 w)] 114.28/47.03 ? [0 0] x + [0 0] y + [0 0] z + [3] 114.28/47.03 [2 2] [2 2] [2 2] [4] 114.28/47.03 = [c_20(e1^#(x1, x1, x, y, z, w))] 114.28/47.03 114.28/47.03 [e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a())] = [0 0] x + [0 0] y + [0 0] z + [0 0] x1 + [0] 114.28/47.03 [2 1] [1 1] [2 2] [7 7] [0] 114.28/47.03 ? [0 0] x + [0 0] y + [0 0] z + [0 0] x1 + [3] 114.28/47.03 [1 2] [1 1] [1 2] [1 1] [4] 114.28/47.03 = [c_21(e5^#(x1, x, y, z))] 114.28/47.03 114.28/47.03 114.28/47.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 114.28/47.03 114.28/47.03 We are left with following problem, upon which TcT provides the 114.28/47.03 certificate YES(O(1),O(1)). 114.28/47.03 114.28/47.03 Strict DPs: 114.28/47.03 { f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.03 , f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.03 , g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.03 , g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.03 , f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.03 , f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.03 , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.03 , e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.03 , e2^#(f1(w, w), x, y, z, f2(w, w), w) -> 114.28/47.03 c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) 114.28/47.03 , e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.03 , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.03 , e4^#(g1(w, w), 114.28/47.03 x1, 114.28/47.03 g2(w, w), 114.28/47.03 x1, 114.28/47.03 g1(w, w), 114.28/47.03 x1, 114.28/47.03 g2(w, w), 114.28/47.03 x1, 114.28/47.03 x, 114.28/47.03 y, 114.28/47.03 z, 114.28/47.03 w) 114.28/47.03 -> c_20(e1^#(x1, x1, x, y, z, w)) 114.28/47.03 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) } 114.28/47.03 Weak DPs: 114.28/47.03 { g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.03 , g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.03 , h2^#(a()) -> c_10() 114.28/47.03 , h1^#(a()) -> c_9() 114.28/47.03 , e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) 114.28/47.03 , e5^#(i(), x, y, z) -> c_16() 114.28/47.03 , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.03 , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() } 114.28/47.03 Obligation: 114.28/47.03 innermost runtime complexity 114.28/47.03 Answer: 114.28/47.03 YES(O(1),O(1)) 114.28/47.03 114.28/47.03 Consider the dependency graph: 114.28/47.03 114.28/47.03 1: f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.03 -->_1 g2^#(a(), x) -> c_6(h1^#(x)) :14 114.28/47.03 -->_1 g2^#(x, a()) -> c_5(h2^#(x)) :3 114.28/47.03 114.28/47.03 2: f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.03 -->_1 g1^#(a(), x) -> c_4(h1^#(x)) :15 114.28/47.03 -->_1 g1^#(x, a()) -> c_3(h2^#(x)) :4 114.28/47.03 114.28/47.03 3: g2^#(x, a()) -> c_5(h2^#(x)) -->_1 h2^#(a()) -> c_10() :16 114.28/47.03 114.28/47.03 4: g1^#(x, a()) -> c_3(h2^#(x)) -->_1 h2^#(a()) -> c_10() :16 114.28/47.03 114.28/47.03 5: f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.03 -->_1 g2^#(a(), x) -> c_6(h1^#(x)) :14 114.28/47.03 -->_1 g2^#(x, a()) -> c_5(h2^#(x)) :3 114.28/47.03 114.28/47.03 6: f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.03 -->_1 g1^#(a(), x) -> c_4(h1^#(x)) :15 114.28/47.03 -->_1 g1^#(x, a()) -> c_3(h2^#(x)) :4 114.28/47.03 114.28/47.03 7: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.03 -->_1 e5^#(i(), x, y, z) -> c_16() :19 114.28/47.03 114.28/47.03 8: e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.03 114.28/47.03 9: e2^#(f1(w, w), x, y, z, f2(w, w), w) -> 114.28/47.03 c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) 114.28/47.03 -->_1 e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) :20 114.28/47.03 -->_1 e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() :21 114.28/47.03 114.28/47.03 10: e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.03 114.28/47.03 11: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.03 114.28/47.03 12: e4^#(g1(w, w), 114.28/47.03 x1, 114.28/47.03 g2(w, w), 114.28/47.03 x1, 114.28/47.03 g1(w, w), 114.28/47.03 x1, 114.28/47.03 g2(w, w), 114.28/47.03 x1, 114.28/47.03 x, 114.28/47.03 y, 114.28/47.03 z, 114.28/47.03 w) 114.28/47.03 -> c_20(e1^#(x1, x1, x, y, z, w)) 114.28/47.03 -->_1 e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) :7 114.28/47.03 114.28/47.03 13: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) 114.28/47.03 -->_1 e5^#(i(), x, y, z) -> c_16() :19 114.28/47.03 114.28/47.03 14: g2^#(a(), x) -> c_6(h1^#(x)) -->_1 h1^#(a()) -> c_9() :17 114.28/47.03 114.28/47.03 15: g1^#(a(), x) -> c_4(h1^#(x)) -->_1 h1^#(a()) -> c_9() :17 114.28/47.03 114.28/47.03 16: h2^#(a()) -> c_10() 114.28/47.03 114.28/47.03 17: h1^#(a()) -> c_9() 114.28/47.03 114.28/47.03 18: e1^#(h1(w), h2(w), x, y, z, w) -> c_12(e2^#(x, x, y, z, z, w)) 114.28/47.03 -->_1 e2^#(i(), x, y, z, i(), a()) -> c_15() :10 114.28/47.03 -->_1 e2^#(f1(w, w), x, y, z, f2(w, w), w) -> 114.28/47.03 c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z, w)) :9 114.28/47.03 -->_1 e2^#(x, x, y, z, z, a()) -> c_13() :8 114.28/47.03 114.28/47.03 19: e5^#(i(), x, y, z) -> c_16() 114.28/47.03 114.28/47.03 20: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.03 -->_1 e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) :13 114.28/47.03 -->_1 e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() :11 114.28/47.03 114.28/47.03 21: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() 114.28/47.03 114.28/47.03 114.28/47.03 Only the nodes {1,14,17,3,16,2,15,4,5,6,7,19,8,10,11,13,20,21} are 114.28/47.03 reachable from nodes 114.28/47.03 {1,2,3,4,5,6,7,8,10,11,13,14,15,16,17,19,20,21} that start 114.28/47.03 derivation from marked basic terms. The nodes not reachable are 114.28/47.03 removed from the problem. 114.28/47.03 114.28/47.03 We are left with following problem, upon which TcT provides the 114.28/47.03 certificate YES(O(1),O(1)). 114.28/47.03 114.28/47.03 Strict DPs: 114.28/47.03 { f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.03 , f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.03 , g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.03 , g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.03 , f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.03 , f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.03 , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.03 , e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.03 , e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.03 , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.03 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) } 114.28/47.03 Weak DPs: 114.28/47.03 { g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.03 , g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.03 , h2^#(a()) -> c_10() 114.28/47.03 , h1^#(a()) -> c_9() 114.28/47.03 , e5^#(i(), x, y, z) -> c_16() 114.28/47.03 , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.03 , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() } 114.28/47.03 Obligation: 114.28/47.03 innermost runtime complexity 114.28/47.03 Answer: 114.28/47.03 YES(O(1),O(1)) 114.28/47.03 114.28/47.03 We estimate the number of application of {3,4,7,8,9} by 114.28/47.03 applications of Pre({3,4,7,8,9}) = {1,2,5,6}. Here rules are 114.28/47.03 labeled as follows: 114.28/47.03 114.28/47.03 DPs: 114.28/47.03 { 1: f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.03 , 2: f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.03 , 3: g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.03 , 4: g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.03 , 5: f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.03 , 6: f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.03 , 7: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.03 , 8: e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.03 , 9: e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.03 , 10: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.03 , 11: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) 114.28/47.03 , 12: g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.03 , 13: g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.03 , 14: h2^#(a()) -> c_10() 114.28/47.03 , 15: h1^#(a()) -> c_9() 114.28/47.03 , 16: e5^#(i(), x, y, z) -> c_16() 114.28/47.03 , 17: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.03 , 18: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() } 114.28/47.03 114.28/47.03 We are left with following problem, upon which TcT provides the 114.28/47.03 certificate YES(O(1),O(1)). 114.28/47.03 114.28/47.03 Strict DPs: 114.28/47.03 { f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.03 , f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.03 , f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.03 , f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.03 , e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.03 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) } 114.28/47.03 Weak DPs: 114.28/47.03 { g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.03 , g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.03 , g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.03 , g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.03 , h2^#(a()) -> c_10() 114.28/47.03 , h1^#(a()) -> c_9() 114.28/47.03 , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.03 , e5^#(i(), x, y, z) -> c_16() 114.28/47.03 , e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.03 , e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.03 , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.03 , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() } 114.28/47.03 Obligation: 114.28/47.03 innermost runtime complexity 114.28/47.03 Answer: 114.28/47.03 YES(O(1),O(1)) 114.28/47.03 114.28/47.03 We estimate the number of application of {1,2,3,4} by applications 114.28/47.03 of Pre({1,2,3,4}) = {}. Here rules are labeled as follows: 114.28/47.03 114.28/47.03 DPs: 114.28/47.03 { 1: f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.03 , 2: f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.03 , 3: f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.03 , 4: f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.03 , 5: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.03 , 6: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) 114.28/47.03 , 7: g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.03 , 8: g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.03 , 9: g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.03 , 10: g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.03 , 11: h2^#(a()) -> c_10() 114.28/47.03 , 12: h1^#(a()) -> c_9() 114.28/47.03 , 13: e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.03 , 14: e5^#(i(), x, y, z) -> c_16() 114.28/47.03 , 15: e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.03 , 16: e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.03 , 17: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.03 , 18: e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() } 114.28/47.03 114.28/47.03 We are left with following problem, upon which TcT provides the 114.28/47.03 certificate YES(O(1),O(1)). 114.28/47.03 114.28/47.03 Strict DPs: 114.28/47.03 { e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.03 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) } 114.28/47.03 Weak DPs: 114.28/47.03 { f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.03 , f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.03 , g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.03 , g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.03 , g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.03 , g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.03 , h2^#(a()) -> c_10() 114.28/47.03 , h1^#(a()) -> c_9() 114.28/47.03 , f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.03 , f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.03 , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.03 , e5^#(i(), x, y, z) -> c_16() 114.28/47.03 , e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.03 , e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.03 , e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.03 , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() } 114.28/47.03 Obligation: 114.28/47.03 innermost runtime complexity 114.28/47.03 Answer: 114.28/47.03 YES(O(1),O(1)) 114.28/47.03 114.28/47.03 The following weak DPs constitute a sub-graph of the DG that is 114.28/47.03 closed under successors. The DPs are removed. 114.28/47.03 114.28/47.03 { f1^#(x, a()) -> c_1(g2^#(x, x)) 114.28/47.03 , f1^#(a(), x) -> c_2(g1^#(x, x)) 114.28/47.03 , g2^#(x, a()) -> c_5(h2^#(x)) 114.28/47.03 , g2^#(a(), x) -> c_6(h1^#(x)) 114.28/47.03 , g1^#(x, a()) -> c_3(h2^#(x)) 114.28/47.03 , g1^#(a(), x) -> c_4(h1^#(x)) 114.28/47.03 , h2^#(a()) -> c_10() 114.28/47.03 , h1^#(a()) -> c_9() 114.28/47.03 , f2^#(x, a()) -> c_7(g2^#(x, x)) 114.28/47.03 , f2^#(a(), x) -> c_8(g1^#(x, x)) 114.28/47.03 , e1^#(x1, x1, x, y, z, a()) -> c_11(e5^#(x1, x, y, z)) 114.28/47.03 , e5^#(i(), x, y, z) -> c_16() 114.28/47.03 , e2^#(x, x, y, z, z, a()) -> c_13() 114.28/47.03 , e2^#(i(), x, y, z, i(), a()) -> c_15() 114.28/47.03 , e3^#(x, y, x, y, y, z, y, z, x, y, z, a()) -> c_18() } 114.28/47.03 114.28/47.03 We are left with following problem, upon which TcT provides the 114.28/47.03 certificate YES(O(1),O(1)). 114.28/47.03 114.28/47.03 Strict DPs: 114.28/47.03 { e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_19() 114.28/47.03 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) } 114.28/47.03 Weak DPs: 114.28/47.03 { e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) } 114.28/47.03 Obligation: 114.28/47.03 innermost runtime complexity 114.28/47.03 Answer: 114.28/47.03 YES(O(1),O(1)) 114.28/47.03 114.28/47.03 Due to missing edges in the dependency-graph, the right-hand sides 114.28/47.03 of following rules could be simplified: 114.28/47.03 114.28/47.03 { e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_21(e5^#(x1, x, y, z)) } 114.28/47.03 114.28/47.03 We are left with following problem, upon which TcT provides the 114.28/47.03 certificate YES(O(1),O(1)). 114.28/47.03 114.28/47.03 Strict DPs: 114.28/47.03 { e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_1() 114.28/47.03 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_2() } 114.28/47.03 Weak DPs: 114.28/47.03 { e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_3(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) } 114.28/47.03 Obligation: 114.28/47.03 innermost runtime complexity 114.28/47.03 Answer: 114.28/47.03 YES(O(1),O(1)) 114.28/47.03 114.28/47.03 Consider the dependency graph 114.28/47.03 114.28/47.03 1: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_1() 114.28/47.03 114.28/47.03 2: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_2() 114.28/47.03 114.28/47.03 3: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_3(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) 114.28/47.03 -->_1 e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> 114.28/47.03 c_2() :2 114.28/47.03 -->_1 e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_1() :1 114.28/47.03 114.28/47.03 114.28/47.03 Following roots of the dependency graph are removed, as the 114.28/47.03 considered set of starting terms is closed under reduction with 114.28/47.03 respect to these rules (modulo compound contexts). 114.28/47.03 114.28/47.03 { e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> 114.28/47.03 c_3(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)) } 114.28/47.03 114.28/47.03 114.28/47.03 We are left with following problem, upon which TcT provides the 114.28/47.03 certificate YES(O(1),O(1)). 114.28/47.03 114.28/47.03 Strict DPs: 114.28/47.03 { e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_1() 114.28/47.03 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_2() } 114.28/47.03 Obligation: 114.28/47.03 innermost runtime complexity 114.28/47.03 Answer: 114.28/47.03 YES(O(1),O(1)) 114.28/47.03 114.28/47.03 Consider the dependency graph 114.28/47.03 114.28/47.03 1: e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_1() 114.28/47.03 114.28/47.03 2: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_2() 114.28/47.03 114.28/47.03 114.28/47.03 Following roots of the dependency graph are removed, as the 114.28/47.03 considered set of starting terms is closed under reduction with 114.28/47.03 respect to these rules (modulo compound contexts). 114.28/47.03 114.28/47.03 { e4^#(x, x, x, x, x, x, x, x, x, x, x, a()) -> c_1() 114.28/47.03 , e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z, a()) -> c_2() } 114.28/47.03 114.28/47.03 114.28/47.03 We are left with following problem, upon which TcT provides the 114.28/47.03 certificate YES(O(1),O(1)). 114.28/47.03 114.28/47.03 Rules: Empty 114.28/47.03 Obligation: 114.28/47.03 innermost runtime complexity 114.28/47.03 Answer: 114.28/47.03 YES(O(1),O(1)) 114.28/47.03 114.28/47.03 Empty rules are trivially bounded 114.28/47.03 114.28/47.03 Hurray, we answered YES(O(1),O(1)) 114.43/47.11 EOF