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