YES(O(1),O(n^4)) 225.47/60.06 YES(O(1),O(n^4)) 225.47/60.06 225.47/60.06 We are left with following problem, upon which TcT provides the 225.47/60.06 certificate YES(O(1),O(n^4)). 225.47/60.06 225.47/60.06 Strict Trs: 225.47/60.06 { +(x, c(y, z)) -> c(y, +(x, z)) 225.47/60.06 , +(0(), 0()) -> 0() 225.47/60.06 , +(0(), 1()) -> 1() 225.47/60.06 , +(0(), 2()) -> 2() 225.47/60.06 , +(0(), 3()) -> 3() 225.47/60.06 , +(0(), 4()) -> 4() 225.47/60.06 , +(0(), 5()) -> 5() 225.47/60.06 , +(0(), 6()) -> 6() 225.47/60.06 , +(0(), 7()) -> 7() 225.47/60.06 , +(0(), 8()) -> 8() 225.47/60.06 , +(0(), 9()) -> 9() 225.47/60.06 , +(1(), 0()) -> 1() 225.47/60.06 , +(1(), 1()) -> 2() 225.47/60.06 , +(1(), 2()) -> 3() 225.47/60.06 , +(1(), 3()) -> 4() 225.47/60.06 , +(1(), 4()) -> 5() 225.47/60.06 , +(1(), 5()) -> 6() 225.47/60.06 , +(1(), 6()) -> 7() 225.47/60.06 , +(1(), 7()) -> 8() 225.47/60.06 , +(1(), 8()) -> 9() 225.47/60.06 , +(1(), 9()) -> c(1(), 0()) 225.47/60.06 , +(2(), 0()) -> 2() 225.47/60.06 , +(2(), 1()) -> 3() 225.47/60.06 , +(2(), 2()) -> 4() 225.47/60.06 , +(2(), 3()) -> 5() 225.47/60.06 , +(2(), 4()) -> 6() 225.47/60.06 , +(2(), 5()) -> 7() 225.47/60.06 , +(2(), 6()) -> 8() 225.47/60.06 , +(2(), 7()) -> 9() 225.47/60.06 , +(2(), 8()) -> c(1(), 0()) 225.47/60.06 , +(2(), 9()) -> c(1(), 1()) 225.47/60.06 , +(3(), 0()) -> 3() 225.47/60.06 , +(3(), 1()) -> 4() 225.47/60.06 , +(3(), 2()) -> 5() 225.47/60.06 , +(3(), 3()) -> 6() 225.47/60.06 , +(3(), 4()) -> 7() 225.47/60.06 , +(3(), 5()) -> 8() 225.47/60.06 , +(3(), 6()) -> 9() 225.47/60.06 , +(3(), 7()) -> c(1(), 0()) 225.47/60.06 , +(3(), 8()) -> c(1(), 1()) 225.47/60.06 , +(3(), 9()) -> c(1(), 2()) 225.47/60.06 , +(4(), 0()) -> 4() 225.47/60.06 , +(4(), 1()) -> 5() 225.47/60.06 , +(4(), 2()) -> 6() 225.47/60.06 , +(4(), 3()) -> 7() 225.47/60.06 , +(4(), 4()) -> 8() 225.47/60.06 , +(4(), 5()) -> 9() 225.47/60.06 , +(4(), 6()) -> c(1(), 0()) 225.47/60.06 , +(4(), 7()) -> c(1(), 1()) 225.47/60.06 , +(4(), 8()) -> c(1(), 2()) 225.47/60.06 , +(4(), 9()) -> c(1(), 3()) 225.47/60.06 , +(5(), 0()) -> 5() 225.47/60.06 , +(5(), 1()) -> 6() 225.47/60.06 , +(5(), 2()) -> 7() 225.47/60.06 , +(5(), 3()) -> 8() 225.47/60.06 , +(5(), 4()) -> 9() 225.47/60.06 , +(5(), 5()) -> c(1(), 0()) 225.47/60.06 , +(5(), 6()) -> c(1(), 1()) 225.47/60.06 , +(5(), 7()) -> c(1(), 2()) 225.47/60.06 , +(5(), 8()) -> c(1(), 3()) 225.47/60.06 , +(5(), 9()) -> c(1(), 4()) 225.47/60.06 , +(6(), 0()) -> 6() 225.47/60.06 , +(6(), 1()) -> 7() 225.47/60.06 , +(6(), 2()) -> 8() 225.47/60.06 , +(6(), 3()) -> 9() 225.47/60.06 , +(6(), 4()) -> c(1(), 0()) 225.47/60.06 , +(6(), 5()) -> c(1(), 1()) 225.47/60.06 , +(6(), 6()) -> c(1(), 2()) 225.47/60.06 , +(6(), 7()) -> c(1(), 3()) 225.47/60.06 , +(6(), 8()) -> c(1(), 4()) 225.47/60.06 , +(6(), 9()) -> c(1(), 5()) 225.47/60.06 , +(7(), 0()) -> 7() 225.47/60.06 , +(7(), 1()) -> 8() 225.47/60.06 , +(7(), 2()) -> 9() 225.47/60.06 , +(7(), 3()) -> c(1(), 0()) 225.47/60.06 , +(7(), 4()) -> c(1(), 1()) 225.47/60.06 , +(7(), 5()) -> c(1(), 2()) 225.47/60.06 , +(7(), 6()) -> c(1(), 3()) 225.47/60.06 , +(7(), 7()) -> c(1(), 4()) 225.47/60.06 , +(7(), 8()) -> c(1(), 5()) 225.47/60.06 , +(7(), 9()) -> c(1(), 6()) 225.47/60.06 , +(8(), 0()) -> 8() 225.47/60.06 , +(8(), 1()) -> 9() 225.47/60.06 , +(8(), 2()) -> c(1(), 0()) 225.47/60.06 , +(8(), 3()) -> c(1(), 1()) 225.47/60.06 , +(8(), 4()) -> c(1(), 2()) 225.47/60.06 , +(8(), 5()) -> c(1(), 3()) 225.47/60.06 , +(8(), 6()) -> c(1(), 4()) 225.47/60.06 , +(8(), 7()) -> c(1(), 5()) 225.47/60.06 , +(8(), 8()) -> c(1(), 6()) 225.47/60.06 , +(8(), 9()) -> c(1(), 7()) 225.47/60.06 , +(9(), 0()) -> 9() 225.47/60.06 , +(9(), 1()) -> c(1(), 0()) 225.47/60.06 , +(9(), 2()) -> c(1(), 1()) 225.47/60.06 , +(9(), 3()) -> c(1(), 2()) 225.47/60.06 , +(9(), 4()) -> c(1(), 3()) 225.47/60.06 , +(9(), 5()) -> c(1(), 4()) 225.47/60.06 , +(9(), 6()) -> c(1(), 5()) 225.47/60.06 , +(9(), 7()) -> c(1(), 6()) 225.47/60.06 , +(9(), 8()) -> c(1(), 7()) 225.47/60.06 , +(9(), 9()) -> c(1(), 8()) 225.47/60.06 , +(c(x, y), z) -> c(x, +(y, z)) 225.47/60.06 , c(x, c(y, z)) -> c(+(x, y), z) 225.47/60.06 , c(0(), x) -> x } 225.47/60.06 Obligation: 225.47/60.06 derivational complexity 225.47/60.06 Answer: 225.47/60.06 YES(O(1),O(n^4)) 225.47/60.06 225.47/60.06 We use the processor 'matrix interpretation of dimension 1' to 225.47/60.06 orient following rules strictly. 225.47/60.06 225.47/60.06 Trs: 225.47/60.06 { +(0(), 0()) -> 0() 225.47/60.06 , +(0(), 1()) -> 1() 225.47/60.06 , +(0(), 2()) -> 2() 225.47/60.06 , +(0(), 3()) -> 3() 225.47/60.06 , +(0(), 4()) -> 4() 225.47/60.06 , +(0(), 5()) -> 5() 225.47/60.06 , +(0(), 6()) -> 6() 225.47/60.06 , +(0(), 7()) -> 7() 225.47/60.06 , +(0(), 8()) -> 8() 225.47/60.06 , +(0(), 9()) -> 9() 225.47/60.06 , +(1(), 0()) -> 1() 225.47/60.06 , +(1(), 1()) -> 2() 225.47/60.06 , +(1(), 2()) -> 3() 225.47/60.06 , +(1(), 3()) -> 4() 225.47/60.06 , +(1(), 4()) -> 5() 225.47/60.06 , +(1(), 5()) -> 6() 225.47/60.06 , +(1(), 6()) -> 7() 225.47/60.06 , +(1(), 7()) -> 8() 225.47/60.06 , +(1(), 8()) -> 9() 225.47/60.06 , +(1(), 9()) -> c(1(), 0()) 225.47/60.06 , +(2(), 0()) -> 2() 225.47/60.06 , +(2(), 1()) -> 3() 225.47/60.06 , +(2(), 2()) -> 4() 225.47/60.06 , +(2(), 3()) -> 5() 225.47/60.06 , +(2(), 4()) -> 6() 225.47/60.06 , +(2(), 5()) -> 7() 225.47/60.06 , +(2(), 6()) -> 8() 225.47/60.06 , +(2(), 7()) -> 9() 225.47/60.06 , +(2(), 8()) -> c(1(), 0()) 225.47/60.06 , +(2(), 9()) -> c(1(), 1()) 225.47/60.06 , +(3(), 0()) -> 3() 225.47/60.06 , +(3(), 1()) -> 4() 225.47/60.06 , +(3(), 2()) -> 5() 225.47/60.06 , +(3(), 3()) -> 6() 225.47/60.06 , +(3(), 4()) -> 7() 225.47/60.06 , +(3(), 5()) -> 8() 225.47/60.06 , +(3(), 6()) -> 9() 225.47/60.06 , +(3(), 7()) -> c(1(), 0()) 225.47/60.06 , +(3(), 8()) -> c(1(), 1()) 225.47/60.06 , +(3(), 9()) -> c(1(), 2()) 225.47/60.06 , +(4(), 0()) -> 4() 225.47/60.06 , +(4(), 1()) -> 5() 225.47/60.06 , +(4(), 2()) -> 6() 225.47/60.06 , +(4(), 3()) -> 7() 225.47/60.06 , +(4(), 4()) -> 8() 225.47/60.06 , +(4(), 5()) -> 9() 225.47/60.06 , +(4(), 6()) -> c(1(), 0()) 225.47/60.06 , +(4(), 7()) -> c(1(), 1()) 225.47/60.06 , +(4(), 8()) -> c(1(), 2()) 225.47/60.06 , +(4(), 9()) -> c(1(), 3()) 225.47/60.06 , +(5(), 0()) -> 5() 225.47/60.06 , +(5(), 1()) -> 6() 225.47/60.06 , +(5(), 2()) -> 7() 225.47/60.06 , +(5(), 3()) -> 8() 225.47/60.06 , +(5(), 4()) -> 9() 225.47/60.06 , +(5(), 5()) -> c(1(), 0()) 225.47/60.06 , +(5(), 6()) -> c(1(), 1()) 225.47/60.06 , +(5(), 7()) -> c(1(), 2()) 225.47/60.06 , +(5(), 8()) -> c(1(), 3()) 225.47/60.06 , +(5(), 9()) -> c(1(), 4()) 225.47/60.06 , +(6(), 0()) -> 6() 225.47/60.06 , +(6(), 1()) -> 7() 225.47/60.06 , +(6(), 2()) -> 8() 225.47/60.06 , +(6(), 3()) -> 9() 225.47/60.06 , +(6(), 4()) -> c(1(), 0()) 225.47/60.06 , +(6(), 5()) -> c(1(), 1()) 225.47/60.06 , +(6(), 6()) -> c(1(), 2()) 225.47/60.06 , +(6(), 7()) -> c(1(), 3()) 225.47/60.06 , +(6(), 8()) -> c(1(), 4()) 225.47/60.06 , +(6(), 9()) -> c(1(), 5()) 225.47/60.06 , +(7(), 0()) -> 7() 225.47/60.06 , +(7(), 1()) -> 8() 225.47/60.06 , +(7(), 2()) -> 9() 225.47/60.06 , +(7(), 3()) -> c(1(), 0()) 225.47/60.06 , +(7(), 4()) -> c(1(), 1()) 225.47/60.06 , +(7(), 5()) -> c(1(), 2()) 225.47/60.06 , +(7(), 6()) -> c(1(), 3()) 225.47/60.06 , +(7(), 7()) -> c(1(), 4()) 225.47/60.06 , +(7(), 8()) -> c(1(), 5()) 225.47/60.06 , +(7(), 9()) -> c(1(), 6()) 225.47/60.06 , +(8(), 0()) -> 8() 225.47/60.06 , +(8(), 1()) -> 9() 225.47/60.06 , +(8(), 2()) -> c(1(), 0()) 225.47/60.06 , +(8(), 3()) -> c(1(), 1()) 225.47/60.06 , +(8(), 4()) -> c(1(), 2()) 225.47/60.06 , +(8(), 5()) -> c(1(), 3()) 225.47/60.06 , +(8(), 6()) -> c(1(), 4()) 225.47/60.06 , +(8(), 7()) -> c(1(), 5()) 225.47/60.06 , +(8(), 8()) -> c(1(), 6()) 225.47/60.06 , +(8(), 9()) -> c(1(), 7()) 225.47/60.06 , +(9(), 0()) -> 9() 225.47/60.06 , +(9(), 1()) -> c(1(), 0()) 225.47/60.06 , +(9(), 2()) -> c(1(), 1()) 225.47/60.06 , +(9(), 3()) -> c(1(), 2()) 225.47/60.06 , +(9(), 4()) -> c(1(), 3()) 225.47/60.06 , +(9(), 5()) -> c(1(), 4()) 225.47/60.06 , +(9(), 6()) -> c(1(), 5()) 225.47/60.06 , +(9(), 7()) -> c(1(), 6()) 225.47/60.06 , +(9(), 8()) -> c(1(), 7()) 225.47/60.06 , +(9(), 9()) -> c(1(), 8()) 225.47/60.06 , c(0(), x) -> x } 225.47/60.06 225.47/60.06 The induced complexity on above rules (modulo remaining rules) is 225.47/60.06 YES(?,O(n^1)) . These rules are removed from the problem. Note that 225.47/60.06 no rule is size-increasing. The overall complexity is obtained by 225.47/60.06 multiplication . 225.47/60.06 225.47/60.06 Sub-proof: 225.47/60.06 ---------- 225.47/60.06 TcT has computed the following triangular matrix interpretation. 225.47/60.06 225.47/60.06 [+](x1, x2) = [1] x1 + [1] x2 + [1] 225.47/60.06 225.47/60.06 [0] = [0] 225.47/60.06 225.47/60.06 [1] = [1] 225.47/60.06 225.47/60.06 [2] = [1] 225.47/60.06 225.47/60.06 [3] = [1] 225.47/60.06 225.47/60.06 [4] = [2] 225.47/60.06 225.47/60.06 [5] = [2] 225.47/60.06 225.47/60.06 [6] = [2] 225.47/60.06 225.47/60.06 [7] = [2] 225.47/60.06 225.47/60.06 [8] = [2] 225.47/60.06 225.47/60.06 [9] = [2] 225.47/60.06 225.47/60.06 [c](x1, x2) = [1] x1 + [1] x2 + [1] 225.47/60.06 225.47/60.06 The order satisfies the following ordering constraints: 225.47/60.06 225.47/60.06 [+(x, c(y, z))] = [1] x + [1] y + [1] z + [2] 225.47/60.06 >= [1] x + [1] y + [1] z + [2] 225.47/60.06 = [c(y, +(x, z))] 225.47/60.06 225.47/60.06 [+(0(), 0())] = [1] 225.47/60.06 > [0] 225.47/60.06 = [0()] 225.47/60.06 225.47/60.06 [+(0(), 1())] = [2] 225.47/60.06 > [1] 225.47/60.06 = [1()] 225.47/60.06 225.47/60.06 [+(0(), 2())] = [2] 225.47/60.06 > [1] 225.47/60.06 = [2()] 225.47/60.06 225.47/60.06 [+(0(), 3())] = [2] 225.47/60.06 > [1] 225.47/60.06 = [3()] 225.47/60.06 225.47/60.06 [+(0(), 4())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [4()] 225.47/60.06 225.47/60.06 [+(0(), 5())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [5()] 225.47/60.06 225.47/60.06 [+(0(), 6())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [6()] 225.47/60.06 225.47/60.06 [+(0(), 7())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [7()] 225.47/60.06 225.47/60.06 [+(0(), 8())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [8()] 225.47/60.06 225.47/60.06 [+(0(), 9())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [9()] 225.47/60.06 225.47/60.06 [+(1(), 0())] = [2] 225.47/60.06 > [1] 225.47/60.06 = [1()] 225.47/60.06 225.47/60.06 [+(1(), 1())] = [3] 225.47/60.06 > [1] 225.47/60.06 = [2()] 225.47/60.06 225.47/60.06 [+(1(), 2())] = [3] 225.47/60.06 > [1] 225.47/60.06 = [3()] 225.47/60.06 225.47/60.06 [+(1(), 3())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [4()] 225.47/60.06 225.47/60.06 [+(1(), 4())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [5()] 225.47/60.06 225.47/60.06 [+(1(), 5())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [6()] 225.47/60.06 225.47/60.06 [+(1(), 6())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [7()] 225.47/60.06 225.47/60.06 [+(1(), 7())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [8()] 225.47/60.06 225.47/60.06 [+(1(), 8())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [9()] 225.47/60.06 225.47/60.06 [+(1(), 9())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [c(1(), 0())] 225.47/60.06 225.47/60.06 [+(2(), 0())] = [2] 225.47/60.06 > [1] 225.47/60.06 = [2()] 225.47/60.06 225.47/60.06 [+(2(), 1())] = [3] 225.47/60.06 > [1] 225.47/60.06 = [3()] 225.47/60.06 225.47/60.06 [+(2(), 2())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [4()] 225.47/60.06 225.47/60.06 [+(2(), 3())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [5()] 225.47/60.06 225.47/60.06 [+(2(), 4())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [6()] 225.47/60.06 225.47/60.06 [+(2(), 5())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [7()] 225.47/60.06 225.47/60.06 [+(2(), 6())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [8()] 225.47/60.06 225.47/60.06 [+(2(), 7())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [9()] 225.47/60.06 225.47/60.06 [+(2(), 8())] = [4] 225.47/60.06 > [2] 225.47/60.06 = [c(1(), 0())] 225.47/60.06 225.47/60.06 [+(2(), 9())] = [4] 225.47/60.06 > [3] 225.47/60.06 = [c(1(), 1())] 225.47/60.06 225.47/60.06 [+(3(), 0())] = [2] 225.47/60.06 > [1] 225.47/60.06 = [3()] 225.47/60.06 225.47/60.06 [+(3(), 1())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [4()] 225.47/60.06 225.47/60.06 [+(3(), 2())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [5()] 225.47/60.06 225.47/60.06 [+(3(), 3())] = [3] 225.47/60.06 > [2] 225.47/60.06 = [6()] 225.47/60.06 225.47/60.06 [+(3(), 4())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [7()] 225.47/60.07 225.47/60.07 [+(3(), 5())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [8()] 225.47/60.07 225.47/60.07 [+(3(), 6())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [9()] 225.47/60.07 225.47/60.07 [+(3(), 7())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [c(1(), 0())] 225.47/60.07 225.47/60.07 [+(3(), 8())] = [4] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 1())] 225.47/60.07 225.47/60.07 [+(3(), 9())] = [4] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 2())] 225.47/60.07 225.47/60.07 [+(4(), 0())] = [3] 225.47/60.07 > [2] 225.47/60.07 = [4()] 225.47/60.07 225.47/60.07 [+(4(), 1())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [5()] 225.47/60.07 225.47/60.07 [+(4(), 2())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [6()] 225.47/60.07 225.47/60.07 [+(4(), 3())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [7()] 225.47/60.07 225.47/60.07 [+(4(), 4())] = [5] 225.47/60.07 > [2] 225.47/60.07 = [8()] 225.47/60.07 225.47/60.07 [+(4(), 5())] = [5] 225.47/60.07 > [2] 225.47/60.07 = [9()] 225.47/60.07 225.47/60.07 [+(4(), 6())] = [5] 225.47/60.07 > [2] 225.47/60.07 = [c(1(), 0())] 225.47/60.07 225.47/60.07 [+(4(), 7())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 1())] 225.47/60.07 225.47/60.07 [+(4(), 8())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 2())] 225.47/60.07 225.47/60.07 [+(4(), 9())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 3())] 225.47/60.07 225.47/60.07 [+(5(), 0())] = [3] 225.47/60.07 > [2] 225.47/60.07 = [5()] 225.47/60.07 225.47/60.07 [+(5(), 1())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [6()] 225.47/60.07 225.47/60.07 [+(5(), 2())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [7()] 225.47/60.07 225.47/60.07 [+(5(), 3())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [8()] 225.47/60.07 225.47/60.07 [+(5(), 4())] = [5] 225.47/60.07 > [2] 225.47/60.07 = [9()] 225.47/60.07 225.47/60.07 [+(5(), 5())] = [5] 225.47/60.07 > [2] 225.47/60.07 = [c(1(), 0())] 225.47/60.07 225.47/60.07 [+(5(), 6())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 1())] 225.47/60.07 225.47/60.07 [+(5(), 7())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 2())] 225.47/60.07 225.47/60.07 [+(5(), 8())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 3())] 225.47/60.07 225.47/60.07 [+(5(), 9())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 4())] 225.47/60.07 225.47/60.07 [+(6(), 0())] = [3] 225.47/60.07 > [2] 225.47/60.07 = [6()] 225.47/60.07 225.47/60.07 [+(6(), 1())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [7()] 225.47/60.07 225.47/60.07 [+(6(), 2())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [8()] 225.47/60.07 225.47/60.07 [+(6(), 3())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [9()] 225.47/60.07 225.47/60.07 [+(6(), 4())] = [5] 225.47/60.07 > [2] 225.47/60.07 = [c(1(), 0())] 225.47/60.07 225.47/60.07 [+(6(), 5())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 1())] 225.47/60.07 225.47/60.07 [+(6(), 6())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 2())] 225.47/60.07 225.47/60.07 [+(6(), 7())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 3())] 225.47/60.07 225.47/60.07 [+(6(), 8())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 4())] 225.47/60.07 225.47/60.07 [+(6(), 9())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 5())] 225.47/60.07 225.47/60.07 [+(7(), 0())] = [3] 225.47/60.07 > [2] 225.47/60.07 = [7()] 225.47/60.07 225.47/60.07 [+(7(), 1())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [8()] 225.47/60.07 225.47/60.07 [+(7(), 2())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [9()] 225.47/60.07 225.47/60.07 [+(7(), 3())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [c(1(), 0())] 225.47/60.07 225.47/60.07 [+(7(), 4())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 1())] 225.47/60.07 225.47/60.07 [+(7(), 5())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 2())] 225.47/60.07 225.47/60.07 [+(7(), 6())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 3())] 225.47/60.07 225.47/60.07 [+(7(), 7())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 4())] 225.47/60.07 225.47/60.07 [+(7(), 8())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 5())] 225.47/60.07 225.47/60.07 [+(7(), 9())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 6())] 225.47/60.07 225.47/60.07 [+(8(), 0())] = [3] 225.47/60.07 > [2] 225.47/60.07 = [8()] 225.47/60.07 225.47/60.07 [+(8(), 1())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [9()] 225.47/60.07 225.47/60.07 [+(8(), 2())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [c(1(), 0())] 225.47/60.07 225.47/60.07 [+(8(), 3())] = [4] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 1())] 225.47/60.07 225.47/60.07 [+(8(), 4())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 2())] 225.47/60.07 225.47/60.07 [+(8(), 5())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 3())] 225.47/60.07 225.47/60.07 [+(8(), 6())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 4())] 225.47/60.07 225.47/60.07 [+(8(), 7())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 5())] 225.47/60.07 225.47/60.07 [+(8(), 8())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 6())] 225.47/60.07 225.47/60.07 [+(8(), 9())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 7())] 225.47/60.07 225.47/60.07 [+(9(), 0())] = [3] 225.47/60.07 > [2] 225.47/60.07 = [9()] 225.47/60.07 225.47/60.07 [+(9(), 1())] = [4] 225.47/60.07 > [2] 225.47/60.07 = [c(1(), 0())] 225.47/60.07 225.47/60.07 [+(9(), 2())] = [4] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 1())] 225.47/60.07 225.47/60.07 [+(9(), 3())] = [4] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 2())] 225.47/60.07 225.47/60.07 [+(9(), 4())] = [5] 225.47/60.07 > [3] 225.47/60.07 = [c(1(), 3())] 225.47/60.07 225.47/60.07 [+(9(), 5())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 4())] 225.47/60.07 225.47/60.07 [+(9(), 6())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 5())] 225.47/60.07 225.47/60.07 [+(9(), 7())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 6())] 225.47/60.07 225.47/60.07 [+(9(), 8())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 7())] 225.47/60.07 225.47/60.07 [+(9(), 9())] = [5] 225.47/60.07 > [4] 225.47/60.07 = [c(1(), 8())] 225.47/60.07 225.47/60.07 [+(c(x, y), z)] = [1] x + [1] y + [1] z + [2] 225.47/60.07 >= [1] x + [1] y + [1] z + [2] 225.47/60.07 = [c(x, +(y, z))] 225.47/60.07 225.47/60.07 [c(x, c(y, z))] = [1] x + [1] y + [1] z + [2] 225.47/60.07 >= [1] x + [1] y + [1] z + [2] 225.47/60.07 = [c(+(x, y), z)] 225.47/60.07 225.47/60.07 [c(0(), x)] = [1] x + [1] 225.47/60.07 > [1] x + [0] 225.47/60.07 = [x] 225.47/60.07 225.47/60.07 225.47/60.07 We return to the main proof. 225.47/60.07 225.47/60.07 We are left with following problem, upon which TcT provides the 225.47/60.07 certificate YES(O(1),O(n^3)). 225.47/60.07 225.47/60.07 Strict Trs: 225.47/60.07 { +(x, c(y, z)) -> c(y, +(x, z)) 225.47/60.07 , +(c(x, y), z) -> c(x, +(y, z)) 225.47/60.07 , c(x, c(y, z)) -> c(+(x, y), z) } 225.47/60.07 Obligation: 225.47/60.07 derivational complexity 225.47/60.07 Answer: 225.47/60.07 YES(O(1),O(n^3)) 225.47/60.07 225.47/60.07 We use the processor 'matrix interpretation of dimension 1' to 225.47/60.07 orient following rules strictly. 225.47/60.07 225.47/60.07 Trs: { c(x, c(y, z)) -> c(+(x, y), z) } 225.47/60.07 225.47/60.07 The induced complexity on above rules (modulo remaining rules) is 225.47/60.07 YES(?,O(n^1)) . These rules are removed from the problem. Note that 225.47/60.07 no rule is size-increasing. The overall complexity is obtained by 225.47/60.07 multiplication . 225.47/60.07 225.47/60.07 Sub-proof: 225.47/60.07 ---------- 225.47/60.07 TcT has computed the following triangular matrix interpretation. 225.47/60.07 225.47/60.07 [+](x1, x2) = [1] x1 + [1] x2 + [0] 225.47/60.07 225.47/60.07 [c](x1, x2) = [1] x1 + [1] x2 + [1] 225.47/60.07 225.47/60.07 The order satisfies the following ordering constraints: 225.47/60.07 225.47/60.07 [+(x, c(y, z))] = [1] x + [1] y + [1] z + [1] 225.47/60.07 >= [1] x + [1] y + [1] z + [1] 225.47/60.07 = [c(y, +(x, z))] 225.47/60.07 225.47/60.07 [+(c(x, y), z)] = [1] x + [1] y + [1] z + [1] 225.47/60.07 >= [1] x + [1] y + [1] z + [1] 225.47/60.07 = [c(x, +(y, z))] 225.47/60.07 225.47/60.07 [c(x, c(y, z))] = [1] x + [1] y + [1] z + [2] 225.47/60.07 > [1] x + [1] y + [1] z + [1] 225.47/60.07 = [c(+(x, y), z)] 225.47/60.07 225.47/60.07 225.47/60.07 We return to the main proof. 225.47/60.07 225.47/60.07 We are left with following problem, upon which TcT provides the 225.47/60.07 certificate YES(?,O(n^2)). 225.47/60.07 225.47/60.07 Strict Trs: 225.47/60.07 { +(x, c(y, z)) -> c(y, +(x, z)) 225.47/60.07 , +(c(x, y), z) -> c(x, +(y, z)) } 225.47/60.07 Obligation: 225.47/60.07 derivational complexity 225.47/60.07 Answer: 225.47/60.07 YES(?,O(n^2)) 225.47/60.07 225.47/60.07 TcT has computed the following triangular matrix interpretation. 225.47/60.07 225.47/60.07 [+](x1, x2) = [1 2] x1 + [1 1] x2 + [0] 225.47/60.07 [0 1] [0 1] [0] 225.47/60.07 225.47/60.07 [c](x1, x2) = [1 5] x1 + [1 0] x2 + [0] 225.47/60.07 [0 1] [0 1] [1] 225.47/60.07 225.47/60.07 The order satisfies the following ordering constraints: 225.47/60.07 225.47/60.07 [+(x, c(y, z))] = [1 2] x + [1 6] y + [1 1] z + [1] 225.47/60.07 [0 1] [0 1] [0 1] [1] 225.47/60.07 > [1 2] x + [1 5] y + [1 1] z + [0] 225.47/60.07 [0 1] [0 1] [0 1] [1] 225.47/60.07 = [c(y, +(x, z))] 225.47/60.07 225.47/60.07 [+(c(x, y), z)] = [1 7] x + [1 2] y + [1 1] z + [2] 225.47/60.07 [0 1] [0 1] [0 1] [1] 225.47/60.07 > [1 5] x + [1 2] y + [1 1] z + [0] 225.47/60.07 [0 1] [0 1] [0 1] [1] 225.47/60.07 = [c(x, +(y, z))] 225.47/60.07 225.47/60.07 225.47/60.07 Hurray, we answered YES(O(1),O(n^4)) 225.61/60.16 EOF