YES(O(1),O(1)) 10.42/2.70 YES(O(1),O(1)) 10.42/2.70 10.42/2.70 We are left with following problem, upon which TcT provides the 10.42/2.70 certificate YES(O(1),O(1)). 10.42/2.70 10.42/2.70 Strict Trs: 10.42/2.70 { f0(S(x), x2, x3, 0(), x5) -> 0() 10.42/2.70 , f0(S(x''), S(x'), x3, S(x), y) -> f1(x', S(x'), x, S(x), S(S(y))) 10.42/2.70 , f0(0(), x2, x3, x4, x5) -> 0() 10.42/2.70 , f1(x1, x2, x3, x4, S(x)) -> f2(x2, x1, x3, x4, x) 10.42/2.70 , f1(x1, x2, x3, x4, 0()) -> 0() 10.42/2.70 , f4(S(x'), S(x'), x3, x4, S(x)) -> 10.42/2.70 f4[Ite][False][Ite][False][Ite](False(), 10.42/2.70 S(x'), 10.42/2.70 S(x'), 10.42/2.70 x3, 10.42/2.70 x4, 10.42/2.70 S(x)) 10.42/2.70 , f4(S(x'), S(x), x3, x4, 0()) -> 10.42/2.70 f4[Ite][False][Ite][False][Ite](True(), S(x'), S(x), x3, x4, 0()) 10.42/2.70 , f4(S(x'), 0(), x3, x4, S(x)) -> 10.42/2.70 f4[Ite][False][Ite][True][Ite](False(), S(x'), 0(), x3, x4, S(x)) 10.42/2.70 , f4(S(x), 0(), x3, x4, 0()) -> 10.42/2.70 f4[Ite][False][Ite][True][Ite](True(), S(x), 0(), x3, x4, 0()) 10.42/2.70 , f4(0(), x2, x3, x4, x5) -> 0() 10.42/2.70 , f2(x1, x2, S(x'), S(x'), S(x)) -> 10.42/2.70 f2[Ite][False][Ite][False][Ite](False(), 10.42/2.70 x1, 10.42/2.70 x2, 10.42/2.70 S(x'), 10.42/2.70 S(x'), 10.42/2.70 S(x)) 10.42/2.70 , f2(x1, x2, S(x'), S(x), 0()) -> 10.42/2.70 f2[Ite][False][Ite][False][Ite](True(), x1, x2, S(x'), S(x), 0()) 10.42/2.70 , f2(x1, x2, S(x'), 0(), S(x)) -> 10.42/2.70 f2[Ite][False][Ite][True][Ite](False(), x1, x2, S(x'), 0(), S(x)) 10.42/2.70 , f2(x1, x2, S(x), 0(), 0()) -> 10.42/2.70 f2[Ite][False][Ite][True][Ite](True(), x1, x2, S(x), 0(), 0()) 10.42/2.70 , f2(x1, x2, 0(), x4, x5) -> 0() 10.42/2.70 , f6(x1, x2, x3, x4, S(x)) -> f0(x1, x2, x4, x3, x) 10.42/2.70 , f6(x1, x2, x3, x4, 0()) -> 0() 10.42/2.70 , f5(x1, x2, x3, x4, S(x)) -> f6(x2, x1, x3, x4, x) 10.42/2.70 , f5(x1, x2, x3, x4, 0()) -> 0() 10.42/2.70 , f3(x1, x2, x3, x4, S(x)) -> f4(x1, x2, x4, x3, x) 10.42/2.70 , f3(x1, x2, x3, x4, 0()) -> 0() } 10.42/2.70 Obligation: 10.42/2.70 innermost runtime complexity 10.42/2.70 Answer: 10.42/2.70 YES(O(1),O(1)) 10.42/2.70 10.42/2.70 We add the following weak dependency pairs: 10.42/2.70 10.42/2.70 Strict DPs: 10.42/2.70 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.70 , f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.70 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.70 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.70 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.70 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.70 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.70 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.70 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.70 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.70 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.70 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.70 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.70 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.70 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.70 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.70 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.70 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.70 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.70 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.70 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.70 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.70 10.42/2.70 and mark the set of starting terms. 10.42/2.70 10.42/2.70 We are left with following problem, upon which TcT provides the 10.42/2.70 certificate YES(O(1),O(1)). 10.42/2.70 10.42/2.70 Strict DPs: 10.42/2.70 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.70 , f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.70 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.70 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.70 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.70 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.70 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.70 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.70 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.70 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.70 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.70 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.70 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.70 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.70 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.70 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.70 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.70 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.70 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.70 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.70 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.70 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.70 Strict Trs: 10.42/2.70 { f0(S(x), x2, x3, 0(), x5) -> 0() 10.42/2.70 , f0(S(x''), S(x'), x3, S(x), y) -> f1(x', S(x'), x, S(x), S(S(y))) 10.42/2.70 , f0(0(), x2, x3, x4, x5) -> 0() 10.42/2.70 , f1(x1, x2, x3, x4, S(x)) -> f2(x2, x1, x3, x4, x) 10.42/2.70 , f1(x1, x2, x3, x4, 0()) -> 0() 10.42/2.70 , f4(S(x'), S(x'), x3, x4, S(x)) -> 10.42/2.70 f4[Ite][False][Ite][False][Ite](False(), 10.42/2.70 S(x'), 10.42/2.70 S(x'), 10.42/2.70 x3, 10.42/2.70 x4, 10.42/2.70 S(x)) 10.42/2.70 , f4(S(x'), S(x), x3, x4, 0()) -> 10.42/2.70 f4[Ite][False][Ite][False][Ite](True(), S(x'), S(x), x3, x4, 0()) 10.42/2.70 , f4(S(x'), 0(), x3, x4, S(x)) -> 10.42/2.70 f4[Ite][False][Ite][True][Ite](False(), S(x'), 0(), x3, x4, S(x)) 10.42/2.70 , f4(S(x), 0(), x3, x4, 0()) -> 10.42/2.70 f4[Ite][False][Ite][True][Ite](True(), S(x), 0(), x3, x4, 0()) 10.42/2.70 , f4(0(), x2, x3, x4, x5) -> 0() 10.42/2.70 , f2(x1, x2, S(x'), S(x'), S(x)) -> 10.42/2.70 f2[Ite][False][Ite][False][Ite](False(), 10.42/2.70 x1, 10.42/2.70 x2, 10.42/2.70 S(x'), 10.42/2.70 S(x'), 10.42/2.70 S(x)) 10.42/2.70 , f2(x1, x2, S(x'), S(x), 0()) -> 10.42/2.70 f2[Ite][False][Ite][False][Ite](True(), x1, x2, S(x'), S(x), 0()) 10.42/2.70 , f2(x1, x2, S(x'), 0(), S(x)) -> 10.42/2.70 f2[Ite][False][Ite][True][Ite](False(), x1, x2, S(x'), 0(), S(x)) 10.42/2.70 , f2(x1, x2, S(x), 0(), 0()) -> 10.42/2.70 f2[Ite][False][Ite][True][Ite](True(), x1, x2, S(x), 0(), 0()) 10.42/2.70 , f2(x1, x2, 0(), x4, x5) -> 0() 10.42/2.70 , f6(x1, x2, x3, x4, S(x)) -> f0(x1, x2, x4, x3, x) 10.42/2.70 , f6(x1, x2, x3, x4, 0()) -> 0() 10.42/2.70 , f5(x1, x2, x3, x4, S(x)) -> f6(x2, x1, x3, x4, x) 10.42/2.70 , f5(x1, x2, x3, x4, 0()) -> 0() 10.42/2.70 , f3(x1, x2, x3, x4, S(x)) -> f4(x1, x2, x4, x3, x) 10.42/2.70 , f3(x1, x2, x3, x4, 0()) -> 0() } 10.42/2.70 Obligation: 10.42/2.70 innermost runtime complexity 10.42/2.70 Answer: 10.42/2.70 YES(O(1),O(1)) 10.42/2.70 10.42/2.70 No rule is usable, rules are removed from the input problem. 10.42/2.70 10.42/2.70 We are left with following problem, upon which TcT provides the 10.42/2.70 certificate YES(O(1),O(1)). 10.42/2.70 10.42/2.70 Strict DPs: 10.42/2.70 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.70 , f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.70 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.70 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.70 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.70 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.70 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.70 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.70 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.70 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.70 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.70 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.70 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.70 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.70 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.70 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.70 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.70 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.70 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.70 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.70 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.70 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.70 Obligation: 10.42/2.70 innermost runtime complexity 10.42/2.70 Answer: 10.42/2.70 YES(O(1),O(1)) 10.42/2.70 10.42/2.70 The weightgap principle applies (using the following constant 10.42/2.70 growth matrix-interpretation) 10.42/2.70 10.42/2.70 The following argument positions are usable: 10.42/2.70 Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_16) = {1}, 10.42/2.70 Uargs(c_18) = {1}, Uargs(c_20) = {1} 10.42/2.70 10.42/2.70 TcT has computed the following constructor-restricted matrix 10.42/2.70 interpretation. 10.42/2.70 10.42/2.70 [S](x1) = [0] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [0] = [0] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [f0^#](x1, x2, x3, x4, x5) = [1 1] x3 + [0 0] x5 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 10.42/2.70 [c_1] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_2](x1) = [1 0] x1 + [1] 10.42/2.70 [0 1] [1] 10.42/2.70 10.42/2.70 [f1^#](x1, x2, x3, x4, x5) = [0 0] x1 + [0] 10.42/2.70 [2 0] [0] 10.42/2.70 10.42/2.70 [c_3] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_4](x1) = [1 0] x1 + [2] 10.42/2.70 [0 1] [0] 10.42/2.70 10.42/2.70 [f2^#](x1, x2, x3, x4, x5) = [0 0] x2 + [0] 10.42/2.70 [1 0] [0] 10.42/2.70 10.42/2.70 [c_5] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [f4^#](x1, x2, x3, x4, x5) = [1 1] x3 + [1 1] x4 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 10.42/2.70 [c_6] = [2] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_7] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_8] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_9] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_10] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_11] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_12] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_13] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_14] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [c_15] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [f6^#](x1, x2, x3, x4, x5) = [1 2] x1 + [1 1] x2 + [2 2] x3 + [1 10.42/2.70 1] x4 + [1] 10.42/2.70 [1 2] [2 2] [2 1] [1 10.42/2.70 1] [0] 10.42/2.70 10.42/2.70 [c_16](x1) = [1 0] x1 + [0] 10.42/2.70 [0 1] [0] 10.42/2.70 10.42/2.70 [c_17] = [0] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [f5^#](x1, x2, x3, x4, x5) = [2 1] x1 + [1 2] x2 + [2 2] x3 + [1 10.42/2.70 1] x4 + [0] 10.42/2.70 [2 2] [1 2] [2 2] [1 10.42/2.70 2] [0] 10.42/2.70 10.42/2.70 [c_18](x1) = [1 0] x1 + [1] 10.42/2.70 [0 1] [0] 10.42/2.70 10.42/2.70 [c_19] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 [f3^#](x1, x2, x3, x4, x5) = [1 1] x1 + [1 1] x2 + [1 1] x3 + [1 10.42/2.70 1] x4 + [0] 10.42/2.70 [2 1] [1 1] [1 1] [1 10.42/2.70 2] [0] 10.42/2.70 10.42/2.70 [c_20](x1) = [1 0] x1 + [2] 10.42/2.70 [0 1] [0] 10.42/2.70 10.42/2.70 [c_21] = [1] 10.42/2.70 [0] 10.42/2.70 10.42/2.70 The order satisfies the following ordering constraints: 10.42/2.70 10.42/2.70 [f0^#(S(x), x2, x3, 0(), x5)] = [1 1] x3 + [0 0] x5 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_1()] 10.42/2.70 10.42/2.70 [f0^#(S(x''), S(x'), x3, S(x), y)] = [1 1] x3 + [0 0] y + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 ? [0 0] x' + [1] 10.42/2.70 [2 0] [1] 10.42/2.70 = [c_2(f1^#(x', S(x'), x, S(x), S(S(y))))] 10.42/2.70 10.42/2.70 [f0^#(0(), x2, x3, x4, x5)] = [1 1] x3 + [0 0] x5 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_3()] 10.42/2.70 10.42/2.70 [f1^#(x1, x2, x3, x4, S(x))] = [0 0] x1 + [0] 10.42/2.70 [2 0] [0] 10.42/2.70 ? [0 0] x1 + [2] 10.42/2.70 [1 0] [0] 10.42/2.70 = [c_4(f2^#(x2, x1, x3, x4, x))] 10.42/2.70 10.42/2.70 [f1^#(x1, x2, x3, x4, 0())] = [0 0] x1 + [0] 10.42/2.70 [2 0] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_5()] 10.42/2.70 10.42/2.70 [f2^#(x1, x2, S(x'), S(x'), S(x))] = [0 0] x2 + [0] 10.42/2.70 [1 0] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_11()] 10.42/2.70 10.42/2.70 [f2^#(x1, x2, S(x'), S(x), 0())] = [0 0] x2 + [0] 10.42/2.70 [1 0] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_12()] 10.42/2.70 10.42/2.70 [f2^#(x1, x2, S(x'), 0(), S(x))] = [0 0] x2 + [0] 10.42/2.70 [1 0] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_13()] 10.42/2.70 10.42/2.70 [f2^#(x1, x2, S(x), 0(), 0())] = [0 0] x2 + [0] 10.42/2.70 [1 0] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_14()] 10.42/2.70 10.42/2.70 [f2^#(x1, x2, 0(), x4, x5)] = [0 0] x2 + [0] 10.42/2.70 [1 0] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_15()] 10.42/2.70 10.42/2.70 [f4^#(S(x'), S(x'), x3, x4, S(x))] = [1 1] x3 + [1 1] x4 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 ? [2] 10.42/2.70 [0] 10.42/2.70 = [c_6()] 10.42/2.70 10.42/2.70 [f4^#(S(x'), S(x), x3, x4, 0())] = [1 1] x3 + [1 1] x4 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_7()] 10.42/2.70 10.42/2.70 [f4^#(S(x'), 0(), x3, x4, S(x))] = [1 1] x3 + [1 1] x4 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_8()] 10.42/2.70 10.42/2.70 [f4^#(S(x), 0(), x3, x4, 0())] = [1 1] x3 + [1 1] x4 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_9()] 10.42/2.70 10.42/2.70 [f4^#(0(), x2, x3, x4, x5)] = [1 1] x3 + [1 1] x4 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 ? [1] 10.42/2.70 [0] 10.42/2.70 = [c_10()] 10.42/2.70 10.42/2.70 [f6^#(x1, x2, x3, x4, S(x))] = [2 2] x3 + [1 1] x4 + [1 2] x1 + [1 1] x2 + [1] 10.42/2.70 [2 1] [1 1] [1 2] [2 2] [0] 10.42/2.70 ? [0 0] x + [1 1] x4 + [0] 10.42/2.70 [1 1] [1 1] [0] 10.42/2.70 = [c_16(f0^#(x1, x2, x4, x3, x))] 10.42/2.70 10.42/2.70 [f6^#(x1, x2, x3, x4, 0())] = [2 2] x3 + [1 1] x4 + [1 2] x1 + [1 1] x2 + [1] 10.42/2.70 [2 1] [1 1] [1 2] [2 2] [0] 10.42/2.70 > [0] 10.42/2.70 [0] 10.42/2.70 = [c_17()] 10.42/2.70 10.42/2.70 [f5^#(x1, x2, x3, x4, S(x))] = [2 2] x3 + [1 1] x4 + [2 1] x1 + [1 2] x2 + [0] 10.42/2.70 [2 2] [1 2] [2 2] [1 2] [0] 10.42/2.70 ? [2 2] x3 + [1 1] x4 + [1 1] x1 + [1 2] x2 + [2] 10.42/2.70 [2 1] [1 1] [2 2] [1 2] [0] 10.42/2.70 = [c_18(f6^#(x2, x1, x3, x4, x))] 10.42/2.71 10.42/2.71 [f5^#(x1, x2, x3, x4, 0())] = [2 2] x3 + [1 1] x4 + [2 1] x1 + [1 2] x2 + [0] 10.42/2.71 [2 2] [1 2] [2 2] [1 2] [0] 10.42/2.71 ? [1] 10.42/2.71 [0] 10.42/2.71 = [c_19()] 10.42/2.71 10.42/2.71 [f3^#(x1, x2, x3, x4, S(x))] = [1 1] x3 + [1 1] x4 + [1 1] x1 + [1 1] x2 + [0] 10.42/2.71 [1 1] [1 2] [2 1] [1 1] [0] 10.42/2.71 ? [1 1] x3 + [1 1] x4 + [2] 10.42/2.71 [1 1] [1 1] [0] 10.42/2.71 = [c_20(f4^#(x1, x2, x4, x3, x))] 10.42/2.71 10.42/2.71 [f3^#(x1, x2, x3, x4, 0())] = [1 1] x3 + [1 1] x4 + [1 1] x1 + [1 1] x2 + [0] 10.42/2.71 [1 1] [1 2] [2 1] [1 1] [0] 10.42/2.71 ? [1] 10.42/2.71 [0] 10.42/2.71 = [c_21()] 10.42/2.71 10.42/2.71 10.42/2.71 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 10.42/2.71 10.42/2.71 We are left with following problem, upon which TcT provides the 10.42/2.71 certificate YES(O(1),O(1)). 10.42/2.71 10.42/2.71 Strict DPs: 10.42/2.71 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 Weak DPs: { f6^#(x1, x2, x3, x4, 0()) -> c_17() } 10.42/2.71 Obligation: 10.42/2.71 innermost runtime complexity 10.42/2.71 Answer: 10.42/2.71 YES(O(1),O(1)) 10.42/2.71 10.42/2.71 We estimate the number of application of 10.42/2.71 {1,3,5,6,7,8,9,10,11,12,13,14,15,18,20} by applications of 10.42/2.71 Pre({1,3,5,6,7,8,9,10,11,12,13,14,15,18,20}) = {4,16,19}. Here 10.42/2.71 rules are labeled as follows: 10.42/2.71 10.42/2.71 DPs: 10.42/2.71 { 1: f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , 2: f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , 3: f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , 4: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , 5: f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , 6: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , 7: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , 8: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , 9: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , 10: f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , 11: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , 12: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , 13: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , 14: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , 15: f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , 16: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , 17: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , 18: f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , 19: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , 20: f3^#(x1, x2, x3, x4, 0()) -> c_21() 10.42/2.71 , 21: f6^#(x1, x2, x3, x4, 0()) -> c_17() } 10.42/2.71 10.42/2.71 We are left with following problem, upon which TcT provides the 10.42/2.71 certificate YES(O(1),O(1)). 10.42/2.71 10.42/2.71 Strict DPs: 10.42/2.71 { f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) } 10.42/2.71 Weak DPs: 10.42/2.71 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 Obligation: 10.42/2.71 innermost runtime complexity 10.42/2.71 Answer: 10.42/2.71 YES(O(1),O(1)) 10.42/2.71 10.42/2.71 We estimate the number of application of {2,5} by applications of 10.42/2.71 Pre({2,5}) = {1}. Here rules are labeled as follows: 10.42/2.71 10.42/2.71 DPs: 10.42/2.71 { 1: f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , 2: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , 3: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , 4: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , 5: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , 6: f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , 7: f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , 8: f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , 9: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , 10: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , 11: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , 12: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , 13: f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , 14: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , 15: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , 16: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , 17: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , 18: f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , 19: f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , 20: f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , 21: f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 10.42/2.71 We are left with following problem, upon which TcT provides the 10.42/2.71 certificate YES(O(1),O(1)). 10.42/2.71 10.42/2.71 Strict DPs: 10.42/2.71 { f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) } 10.42/2.71 Weak DPs: 10.42/2.71 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 Obligation: 10.42/2.71 innermost runtime complexity 10.42/2.71 Answer: 10.42/2.71 YES(O(1),O(1)) 10.42/2.71 10.42/2.71 We estimate the number of application of {1} by applications of 10.42/2.71 Pre({1}) = {2}. Here rules are labeled as follows: 10.42/2.71 10.42/2.71 DPs: 10.42/2.71 { 1: f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , 2: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , 3: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , 4: f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , 5: f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , 6: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , 7: f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , 8: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , 9: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , 10: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , 11: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , 12: f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , 13: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , 14: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , 15: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , 16: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , 17: f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , 18: f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , 19: f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , 20: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , 21: f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 10.42/2.71 We are left with following problem, upon which TcT provides the 10.42/2.71 certificate YES(O(1),O(1)). 10.42/2.71 10.42/2.71 Strict DPs: 10.42/2.71 { f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) } 10.42/2.71 Weak DPs: 10.42/2.71 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 Obligation: 10.42/2.71 innermost runtime complexity 10.42/2.71 Answer: 10.42/2.71 YES(O(1),O(1)) 10.42/2.71 10.42/2.71 We estimate the number of application of {1} by applications of 10.42/2.71 Pre({1}) = {2}. Here rules are labeled as follows: 10.42/2.71 10.42/2.71 DPs: 10.42/2.71 { 1: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , 2: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , 3: f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , 4: f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , 5: f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , 6: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , 7: f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , 8: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , 9: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , 10: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , 11: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , 12: f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , 13: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , 14: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , 15: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , 16: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , 17: f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , 18: f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , 19: f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , 20: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , 21: f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 10.42/2.71 We are left with following problem, upon which TcT provides the 10.42/2.71 certificate YES(O(1),O(1)). 10.42/2.71 10.42/2.71 Strict DPs: 10.42/2.71 { f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) } 10.42/2.71 Weak DPs: 10.42/2.71 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 Obligation: 10.42/2.71 innermost runtime complexity 10.42/2.71 Answer: 10.42/2.71 YES(O(1),O(1)) 10.42/2.71 10.42/2.71 We estimate the number of application of {1} by applications of 10.42/2.71 Pre({1}) = {}. Here rules are labeled as follows: 10.42/2.71 10.42/2.71 DPs: 10.42/2.71 { 1: f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , 2: f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , 3: f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , 4: f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , 5: f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , 6: f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , 7: f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , 8: f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , 9: f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , 10: f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , 11: f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , 12: f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , 13: f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , 14: f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , 15: f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , 16: f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , 17: f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , 18: f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , 19: f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , 20: f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , 21: f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 10.42/2.71 We are left with following problem, upon which TcT provides the 10.42/2.71 certificate YES(O(1),O(1)). 10.42/2.71 10.42/2.71 Weak DPs: 10.42/2.71 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 Obligation: 10.42/2.71 innermost runtime complexity 10.42/2.71 Answer: 10.42/2.71 YES(O(1),O(1)) 10.42/2.71 10.42/2.71 The following weak DPs constitute a sub-graph of the DG that is 10.42/2.71 closed under successors. The DPs are removed. 10.42/2.71 10.42/2.71 { f0^#(S(x), x2, x3, 0(), x5) -> c_1() 10.42/2.71 , f0^#(S(x''), S(x'), x3, S(x), y) -> 10.42/2.71 c_2(f1^#(x', S(x'), x, S(x), S(S(y)))) 10.42/2.71 , f0^#(0(), x2, x3, x4, x5) -> c_3() 10.42/2.71 , f1^#(x1, x2, x3, x4, S(x)) -> c_4(f2^#(x2, x1, x3, x4, x)) 10.42/2.71 , f1^#(x1, x2, x3, x4, 0()) -> c_5() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x'), S(x)) -> c_11() 10.42/2.71 , f2^#(x1, x2, S(x'), S(x), 0()) -> c_12() 10.42/2.71 , f2^#(x1, x2, S(x'), 0(), S(x)) -> c_13() 10.42/2.71 , f2^#(x1, x2, S(x), 0(), 0()) -> c_14() 10.42/2.71 , f2^#(x1, x2, 0(), x4, x5) -> c_15() 10.42/2.71 , f4^#(S(x'), S(x'), x3, x4, S(x)) -> c_6() 10.42/2.71 , f4^#(S(x'), S(x), x3, x4, 0()) -> c_7() 10.42/2.71 , f4^#(S(x'), 0(), x3, x4, S(x)) -> c_8() 10.42/2.71 , f4^#(S(x), 0(), x3, x4, 0()) -> c_9() 10.42/2.71 , f4^#(0(), x2, x3, x4, x5) -> c_10() 10.42/2.71 , f6^#(x1, x2, x3, x4, S(x)) -> c_16(f0^#(x1, x2, x4, x3, x)) 10.42/2.71 , f6^#(x1, x2, x3, x4, 0()) -> c_17() 10.42/2.71 , f5^#(x1, x2, x3, x4, S(x)) -> c_18(f6^#(x2, x1, x3, x4, x)) 10.42/2.71 , f5^#(x1, x2, x3, x4, 0()) -> c_19() 10.42/2.71 , f3^#(x1, x2, x3, x4, S(x)) -> c_20(f4^#(x1, x2, x4, x3, x)) 10.42/2.71 , f3^#(x1, x2, x3, x4, 0()) -> c_21() } 10.42/2.71 10.42/2.71 We are left with following problem, upon which TcT provides the 10.42/2.71 certificate YES(O(1),O(1)). 10.42/2.71 10.42/2.71 Rules: Empty 10.42/2.71 Obligation: 10.42/2.71 innermost runtime complexity 10.42/2.71 Answer: 10.42/2.71 YES(O(1),O(1)) 10.42/2.71 10.42/2.71 Empty rules are trivially bounded 10.42/2.71 10.42/2.71 Hurray, we answered YES(O(1),O(1)) 10.42/2.72 EOF