YES(O(1),O(1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict Trs: { f0(S(x), x2, x3, 0(), x5) -> 0() , f0(S(x''), S(x'), x3, S(x), y) -> f1(x', S(x'), x, S(x), S(S(y))) , f0(0(), x2, x3, x4, x5) -> 0() , f1(x1, x2, x3, x4, S(x)) -> f2(x2, x1, x3, x4, x) , f1(x1, x2, x3, x4, 0()) -> 0() , f4(S(x'), S(x'), x3, x4, S(x)) -> f4[Ite][False][Ite][False][Ite](False(), S(x'), S(x'), x3, x4, S(x)) , f4(S(x'), S(x), x3, x4, 0()) -> f4[Ite][False][Ite][False][Ite](True(), S(x'), S(x), x3, x4, 0()) , f4(S(x'), 0(), x3, x4, S(x)) -> f4[Ite][False][Ite][True][Ite](False(), S(x'), 0(), x3, x4, S(x)) , f4(S(x), 0(), x3, x4, 0()) -> f4[Ite][False][Ite][True][Ite](True(), S(x), 0(), x3, x4, 0()) , f4(0(), x2, x3, x4, x5) -> 0() , f2(x1, x2, S(x'), S(x'), S(x)) -> f2[Ite][False][Ite][False][Ite](False(), x1, x2, S(x'), S(x'), S(x)) , f2(x1, x2, S(x'), S(x), 0()) -> f2[Ite][False][Ite][False][Ite](True(), x1, x2, S(x'), S(x), 0()) , f2(x1, x2, S(x'), 0(), S(x)) -> f2[Ite][False][Ite][True][Ite](False(), x1, x2, S(x'), 0(), S(x)) , f2(x1, x2, S(x), 0(), 0()) -> f2[Ite][False][Ite][True][Ite](True(), x1, x2, S(x), 0(), 0()) , f2(x1, x2, 0(), x4, x5) -> 0() , f6(x1, x2, x3, x4, S(x)) -> f0(x1, x2, x4, x3, x) , f6(x1, x2, x3, x4, 0()) -> 0() , f5(x1, x2, x3, x4, S(x)) -> f6(x2, x1, x3, x4, x) , f5(x1, x2, x3, x4, 0()) -> 0() , f3(x1, x2, x3, x4, S(x)) -> f4(x1, x2, x4, x3, x) , f3(x1, x2, x3, x4, 0()) -> 0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We add the following innermost weak dependency pairs: Strict DPs: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 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: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } Strict Trs: { f0(S(x), x2, x3, 0(), x5) -> 0() , f0(S(x''), S(x'), x3, S(x), y) -> f1(x', S(x'), x, S(x), S(S(y))) , f0(0(), x2, x3, x4, x5) -> 0() , f1(x1, x2, x3, x4, S(x)) -> f2(x2, x1, x3, x4, x) , f1(x1, x2, x3, x4, 0()) -> 0() , f4(S(x'), S(x'), x3, x4, S(x)) -> f4[Ite][False][Ite][False][Ite](False(), S(x'), S(x'), x3, x4, S(x)) , f4(S(x'), S(x), x3, x4, 0()) -> f4[Ite][False][Ite][False][Ite](True(), S(x'), S(x), x3, x4, 0()) , f4(S(x'), 0(), x3, x4, S(x)) -> f4[Ite][False][Ite][True][Ite](False(), S(x'), 0(), x3, x4, S(x)) , f4(S(x), 0(), x3, x4, 0()) -> f4[Ite][False][Ite][True][Ite](True(), S(x), 0(), x3, x4, 0()) , f4(0(), x2, x3, x4, x5) -> 0() , f2(x1, x2, S(x'), S(x'), S(x)) -> f2[Ite][False][Ite][False][Ite](False(), x1, x2, S(x'), S(x'), S(x)) , f2(x1, x2, S(x'), S(x), 0()) -> f2[Ite][False][Ite][False][Ite](True(), x1, x2, S(x'), S(x), 0()) , f2(x1, x2, S(x'), 0(), S(x)) -> f2[Ite][False][Ite][True][Ite](False(), x1, x2, S(x'), 0(), S(x)) , f2(x1, x2, S(x), 0(), 0()) -> f2[Ite][False][Ite][True][Ite](True(), x1, x2, S(x), 0(), 0()) , f2(x1, x2, 0(), x4, x5) -> 0() , f6(x1, x2, x3, x4, S(x)) -> f0(x1, x2, x4, x3, x) , f6(x1, x2, x3, x4, 0()) -> 0() , f5(x1, x2, x3, x4, S(x)) -> f6(x2, x1, x3, x4, x) , f5(x1, x2, x3, x4, 0()) -> 0() , f3(x1, x2, x3, x4, S(x)) -> f4(x1, x2, x4, x3, x) , f3(x1, x2, x3, x4, 0()) -> 0() } 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: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 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_2) = {1}, Uargs(c_4) = {1}, Uargs(c_16) = {1}, Uargs(c_18) = {1}, Uargs(c_20) = {1} TcT has computed the following constructor-restricted matrix interpretation. [S](x1) = [0] [0] [0] = [0] [0] [f0^#](x1, x2, x3, x4, x5) = [1 1] x3 + [0 0] x5 + [0] [1 1] [1 1] [0] [c_1] = [1] [0] [c_2](x1) = [1 0] x1 + [1] [0 1] [1] [f1^#](x1, x2, x3, x4, x5) = [0 0] x1 + [0] [2 0] [0] [c_3] = [1] [0] [c_4](x1) = [1 0] x1 + [2] [0 1] [0] [f2^#](x1, x2, x3, x4, x5) = [0 0] x2 + [0] [1 0] [0] [c_5] = [1] [0] [f4^#](x1, x2, x3, x4, x5) = [1 1] x3 + [1 1] x4 + [0] [1 1] [1 1] [0] [c_6] = [2] [0] [c_7] = [1] [0] [c_8] = [1] [0] [c_9] = [1] [0] [c_10] = [1] [0] [c_11] = [1] [0] [c_12] = [1] [0] [c_13] = [1] [0] [c_14] = [1] [0] [c_15] = [1] [0] [f6^#](x1, x2, x3, x4, x5) = [1 2] x1 + [1 1] x2 + [2 2] x3 + [1 1] x4 + [1] [1 2] [2 2] [2 1] [1 1] [0] [c_16](x1) = [1 0] x1 + [0] [0 1] [0] [c_17] = [0] [0] [f5^#](x1, x2, x3, x4, x5) = [2 1] x1 + [1 2] x2 + [2 2] x3 + [1 1] x4 + [0] [2 2] [1 2] [2 2] [1 2] [0] [c_18](x1) = [1 0] x1 + [1] [0 1] [0] [c_19] = [1] [0] [f3^#](x1, x2, x3, x4, x5) = [1 1] x1 + [1 1] x2 + [1 1] x3 + [1 1] x4 + [0] [2 1] [1 1] [1 1] [1 2] [0] [c_20](x1) = [1 0] x1 + [2] [0 1] [0] [c_21] = [1] [0] The following symbols are considered usable {f0^#, f1^#, f2^#, f4^#, f6^#, f5^#, f3^#} The order satisfies the following ordering constraints: [f0^#(S(x), x2, x3, 0(), x5)] = [1 1] x3 + [0 0] x5 + [0] [1 1] [1 1] [0] ? [1] [0] = [c_1()] [f0^#(S(x''), S(x'), x3, S(x), y)] = [1 1] x3 + [0 0] y + [0] [1 1] [1 1] [0] ? [0 0] x' + [1] [2 0] [1] = [c_2(f1^#(x', S(x'), x, S(x), S(S(y))))] [f0^#(0(), x2, x3, x4, x5)] = [1 1] x3 + [0 0] x5 + [0] [1 1] [1 1] [0] ? [1] [0] = [c_3()] [f1^#(x1, x2, x3, x4, S(x))] = [0 0] x1 + [0] [2 0] [0] ? [0 0] x1 + [2] [1 0] [0] = [c_4(f2^#(x2, x1, x3, x4, x))] [f1^#(x1, x2, x3, x4, 0())] = [0 0] x1 + [0] [2 0] [0] ? [1] [0] = [c_5()] [f2^#(x1, x2, S(x'), S(x'), S(x))] = [0 0] x2 + [0] [1 0] [0] ? [1] [0] = [c_11()] [f2^#(x1, x2, S(x'), S(x), 0())] = [0 0] x2 + [0] [1 0] [0] ? [1] [0] = [c_12()] [f2^#(x1, x2, S(x'), 0(), S(x))] = [0 0] x2 + [0] [1 0] [0] ? [1] [0] = [c_13()] [f2^#(x1, x2, S(x), 0(), 0())] = [0 0] x2 + [0] [1 0] [0] ? [1] [0] = [c_14()] [f2^#(x1, x2, 0(), x4, x5)] = [0 0] x2 + [0] [1 0] [0] ? [1] [0] = [c_15()] [f4^#(S(x'), S(x'), x3, x4, S(x))] = [1 1] x3 + [1 1] x4 + [0] [1 1] [1 1] [0] ? [2] [0] = [c_6()] [f4^#(S(x'), S(x), x3, x4, 0())] = [1 1] x3 + [1 1] x4 + [0] [1 1] [1 1] [0] ? [1] [0] = [c_7()] [f4^#(S(x'), 0(), x3, x4, S(x))] = [1 1] x3 + [1 1] x4 + [0] [1 1] [1 1] [0] ? [1] [0] = [c_8()] [f4^#(S(x), 0(), x3, x4, 0())] = [1 1] x3 + [1 1] x4 + [0] [1 1] [1 1] [0] ? [1] [0] = [c_9()] [f4^#(0(), x2, x3, x4, x5)] = [1 1] x3 + [1 1] x4 + [0] [1 1] [1 1] [0] ? [1] [0] = [c_10()] [f6^#(x1, x2, x3, x4, S(x))] = [2 2] x3 + [1 1] x4 + [1 2] x1 + [1 1] x2 + [1] [2 1] [1 1] [1 2] [2 2] [0] ? [0 0] x + [1 1] x4 + [0] [1 1] [1 1] [0] = [c_16(f0^#(x1, x2, x4, x3, x))] [f6^#(x1, x2, x3, x4, 0())] = [2 2] x3 + [1 1] x4 + [1 2] x1 + [1 1] x2 + [1] [2 1] [1 1] [1 2] [2 2] [0] > [0] [0] = [c_17()] [f5^#(x1, x2, x3, x4, S(x))] = [2 2] x3 + [1 1] x4 + [2 1] x1 + [1 2] x2 + [0] [2 2] [1 2] [2 2] [1 2] [0] ? [2 2] x3 + [1 1] x4 + [1 1] x1 + [1 2] x2 + [2] [2 1] [1 1] [2 2] [1 2] [0] = [c_18(f6^#(x2, x1, x3, x4, x))] [f5^#(x1, x2, x3, x4, 0())] = [2 2] x3 + [1 1] x4 + [2 1] x1 + [1 2] x2 + [0] [2 2] [1 2] [2 2] [1 2] [0] ? [1] [0] = [c_19()] [f3^#(x1, x2, x3, x4, S(x))] = [1 1] x3 + [1 1] x4 + [1 1] x1 + [1 1] x2 + [0] [1 1] [1 2] [2 1] [1 1] [0] ? [1 1] x3 + [1 1] x4 + [2] [1 1] [1 1] [0] = [c_20(f4^#(x1, x2, x4, x3, x))] [f3^#(x1, x2, x3, x4, 0())] = [1 1] x3 + [1 1] x4 + [1 1] x1 + [1 1] x2 + [0] [1 1] [1 2] [2 1] [1 1] [0] ? [1] [0] = [c_21()] 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: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } Weak DPs: { f6^#(x1, x2, x3, x4, 0()) -> c_17() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {1,3,5,6,7,8,9,10,11,12,13,14,15,18,20} by applications of Pre({1,3,5,6,7,8,9,10,11,12,13,14,15,18,20}) = {4,16,19}. Here rules are labeled as follows: DPs: { 1: f0^#(S(x), x2, x3, 0(), x5) -> c_1() , 2: f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , 3: f0^#(0(), x2, x3, x4, x5) -> c_3() , 4: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , 5: f1^#(x1, x2, x3, x4, 0()) -> c_5() , 6: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , 7: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , 8: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , 9: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , 10: f2^#(x1, x2, 0(), x4, x5) -> c_15() , 11: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , 12: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , 13: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , 14: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , 15: f4^#(0(), x2, x3, x4, x5) -> c_10() , 16: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , 17: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , 18: f5^#(x1, x2, x3, x4, 0()) -> c_19() , 19: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , 20: f3^#(x1, x2, x3, x4, 0()) -> c_21() , 21: f6^#(x1, x2, x3, x4, 0()) -> c_17() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) } Weak DPs: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, 0()) -> c_21() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {2,5} by applications of Pre({2,5}) = {1}. Here rules are labeled as follows: DPs: { 1: f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , 2: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , 3: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , 4: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , 5: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , 6: f0^#(S(x), x2, x3, 0(), x5) -> c_1() , 7: f0^#(0(), x2, x3, x4, x5) -> c_3() , 8: f1^#(x1, x2, x3, x4, 0()) -> c_5() , 9: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , 10: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , 11: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , 12: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , 13: f2^#(x1, x2, 0(), x4, x5) -> c_15() , 14: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , 15: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , 16: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , 17: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , 18: f4^#(0(), x2, x3, x4, x5) -> c_10() , 19: f6^#(x1, x2, x3, x4, 0()) -> c_17() , 20: f5^#(x1, x2, x3, x4, 0()) -> c_19() , 21: f3^#(x1, x2, x3, x4, 0()) -> c_21() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) } Weak DPs: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {1} by applications of Pre({1}) = {2}. Here rules are labeled as follows: DPs: { 1: f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , 2: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , 3: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , 4: f0^#(S(x), x2, x3, 0(), x5) -> c_1() , 5: f0^#(0(), x2, x3, x4, x5) -> c_3() , 6: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , 7: f1^#(x1, x2, x3, x4, 0()) -> c_5() , 8: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , 9: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , 10: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , 11: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , 12: f2^#(x1, x2, 0(), x4, x5) -> c_15() , 13: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , 14: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , 15: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , 16: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , 17: f4^#(0(), x2, x3, x4, x5) -> c_10() , 18: f6^#(x1, x2, x3, x4, 0()) -> c_17() , 19: f5^#(x1, x2, x3, x4, 0()) -> c_19() , 20: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , 21: f3^#(x1, x2, x3, x4, 0()) -> c_21() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) } Weak DPs: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {1} by applications of Pre({1}) = {2}. Here rules are labeled as follows: DPs: { 1: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , 2: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , 3: f0^#(S(x), x2, x3, 0(), x5) -> c_1() , 4: f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , 5: f0^#(0(), x2, x3, x4, x5) -> c_3() , 6: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , 7: f1^#(x1, x2, x3, x4, 0()) -> c_5() , 8: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , 9: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , 10: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , 11: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , 12: f2^#(x1, x2, 0(), x4, x5) -> c_15() , 13: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , 14: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , 15: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , 16: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , 17: f4^#(0(), x2, x3, x4, x5) -> c_10() , 18: f6^#(x1, x2, x3, x4, 0()) -> c_17() , 19: f5^#(x1, x2, x3, x4, 0()) -> c_19() , 20: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , 21: f3^#(x1, x2, x3, x4, 0()) -> c_21() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) } Weak DPs: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {1} by applications of Pre({1}) = {}. Here rules are labeled as follows: DPs: { 1: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , 2: f0^#(S(x), x2, x3, 0(), x5) -> c_1() , 3: f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , 4: f0^#(0(), x2, x3, x4, x5) -> c_3() , 5: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , 6: f1^#(x1, x2, x3, x4, 0()) -> c_5() , 7: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , 8: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , 9: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , 10: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , 11: f2^#(x1, x2, 0(), x4, x5) -> c_15() , 12: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , 13: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , 14: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , 15: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , 16: f4^#(0(), x2, x3, x4, x5) -> c_10() , 17: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , 18: f6^#(x1, x2, x3, x4, 0()) -> c_17() , 19: f5^#(x1, x2, x3, x4, 0()) -> c_19() , 20: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , 21: f3^#(x1, x2, x3, x4, 0()) -> c_21() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 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. { f0^#(S(x), x2, x3, 0(), x5) -> c_1() , f0^#(S(x''), S(x'), x3, S(x), y) -> c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) , f0^#(0(), x2, x3, x4, x5) -> c_3() , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) , f1^#(x1, x2, x3, x4, 0()) -> c_5() , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() , f2^#(x1, x2, 0(), x4, x5) -> c_15() , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() , f4^#(0(), x2, x3, x4, x5) -> c_10() , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) , f6^#(x1, x2, x3, x4, 0()) -> c_17() , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) , f5^#(x1, x2, x3, x4, 0()) -> c_19() , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 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))