YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , *(@x, @y) -> #mult(@x, @y) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , dyade(@l1, @l2) -> dyade#1(@l1, @l2) } Weak Trs: { #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#0(), #pos(@y)) -> #0() , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(::) = {1, 2}, Uargs(#succ) = {1}, Uargs(#pos) = {1}, Uargs(#add) = {2}, Uargs(#neg) = {1}, Uargs(#pred) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [#natmult](x1, x2) = [0] [mult](x1, x2) = [1] x1 + [7] [mult#1](x1, x2) = [1] x2 + [6] [::](x1, x2) = [1] x1 + [1] x2 + [1] [#mult](x1, x2) = [7] [#succ](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#add](x1, x2) = [1] x2 + [0] [#0] = [0] [*](x1, x2) = [7] [#neg](x1) = [1] x1 + [0] [dyade#1](x1, x2) = [1] x1 + [1] x2 + [5] [#pred](x1) = [1] x1 + [0] [#s](x1) = [0] [dyade](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] The following symbols are considered usable {#natmult, mult, mult#1, #mult, #succ, #add, *, dyade#1, #pred, dyade} The order satisfies the following ordering constraints: [#natmult(#0(), @y)] = [0] >= [0] = [#0()] [#natmult(#s(@x), @y)] = [0] >= [0] = [#add(#pos(@y), #natmult(@x, @y))] [mult(@n, @l)] = [1] @n + [7] > [1] @n + [6] = [mult#1(@l, @n)] [mult#1(::(@x, @xs), @n)] = [1] @n + [6] ? [1] @n + [15] = [::(*(@n, @x), mult(@n, @xs))] [mult#1(nil(), @n)] = [1] @n + [6] ? [7] = [nil()] [#mult(#pos(@x), #pos(@y))] = [7] > [0] = [#pos(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [7] > [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [7] > [0] = [#neg(#natmult(@x, @y))] [#mult(#0(), #pos(@y))] = [7] > [0] = [#0()] [#mult(#0(), #0())] = [7] > [0] = [#0()] [#mult(#0(), #neg(@y))] = [7] > [0] = [#0()] [#mult(#neg(@x), #pos(@y))] = [7] > [0] = [#neg(#natmult(@x, @y))] [#mult(#neg(@x), #0())] = [7] > [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [7] > [0] = [#pos(#natmult(@x, @y))] [#succ(#pos(#s(@x)))] = [0] >= [0] = [#pos(#s(#s(@x)))] [#succ(#0())] = [0] >= [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] >= [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [0] >= [0] = [#neg(#s(@x))] [#add(#pos(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [#add(#0(), @y)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [1] @y + [0] >= [1] @y + [0] = [#pred(#add(#pos(#s(@x)), @y))] [*(@x, @y)] = [7] >= [7] = [#mult(@x, @y)] [dyade#1(::(@x, @xs), @l2)] = [1] @x + [1] @l2 + [1] @xs + [6] ? [1] @x + [1] @l2 + [1] @xs + [15] = [::(mult(@x, @l2), dyade(@xs, @l2))] [dyade#1(nil(), @l2)] = [1] @l2 + [12] > [7] = [nil()] [#pred(#pos(#s(#0())))] = [0] >= [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [0] >= [0] = [#pos(#s(@x))] [#pred(#0())] = [0] >= [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [0] >= [0] = [#neg(#s(#s(@x)))] [dyade(@l1, @l2)] = [1] @l1 + [1] @l2 + [7] > [1] @l1 + [1] @l2 + [5] = [dyade#1(@l1, @l2)] 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(n^2)). Strict Trs: { mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , *(@x, @y) -> #mult(@x, @y) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) } Weak Trs: { #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) , mult(@n, @l) -> mult#1(@l, @n) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#0(), #pos(@y)) -> #0() , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , dyade#1(nil(), @l2) -> nil() , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(::) = {1, 2}, Uargs(#succ) = {1}, Uargs(#pos) = {1}, Uargs(#add) = {2}, Uargs(#neg) = {1}, Uargs(#pred) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [#natmult](x1, x2) = [0] [mult](x1, x2) = [2] [mult#1](x1, x2) = [2] [::](x1, x2) = [1] x1 + [1] x2 + [0] [#mult](x1, x2) = [4] [#succ](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#add](x1, x2) = [1] x2 + [0] [#0] = [0] [*](x1, x2) = [0] [#neg](x1) = [1] x1 + [0] [dyade#1](x1, x2) = [1] x1 + [1] x2 + [1] [#pred](x1) = [1] x1 + [0] [#s](x1) = [0] [dyade](x1, x2) = [1] x1 + [1] x2 + [6] [nil] = [1] The following symbols are considered usable {#natmult, mult, mult#1, #mult, #succ, #add, *, dyade#1, #pred, dyade} The order satisfies the following ordering constraints: [#natmult(#0(), @y)] = [0] >= [0] = [#0()] [#natmult(#s(@x), @y)] = [0] >= [0] = [#add(#pos(@y), #natmult(@x, @y))] [mult(@n, @l)] = [2] >= [2] = [mult#1(@l, @n)] [mult#1(::(@x, @xs), @n)] = [2] >= [2] = [::(*(@n, @x), mult(@n, @xs))] [mult#1(nil(), @n)] = [2] > [1] = [nil()] [#mult(#pos(@x), #pos(@y))] = [4] > [0] = [#pos(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [4] > [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [4] > [0] = [#neg(#natmult(@x, @y))] [#mult(#0(), #pos(@y))] = [4] > [0] = [#0()] [#mult(#0(), #0())] = [4] > [0] = [#0()] [#mult(#0(), #neg(@y))] = [4] > [0] = [#0()] [#mult(#neg(@x), #pos(@y))] = [4] > [0] = [#neg(#natmult(@x, @y))] [#mult(#neg(@x), #0())] = [4] > [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [4] > [0] = [#pos(#natmult(@x, @y))] [#succ(#pos(#s(@x)))] = [0] >= [0] = [#pos(#s(#s(@x)))] [#succ(#0())] = [0] >= [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] >= [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [0] >= [0] = [#neg(#s(@x))] [#add(#pos(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [#add(#0(), @y)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [1] @y + [0] >= [1] @y + [0] = [#pred(#add(#pos(#s(@x)), @y))] [*(@x, @y)] = [0] ? [4] = [#mult(@x, @y)] [dyade#1(::(@x, @xs), @l2)] = [1] @x + [1] @l2 + [1] @xs + [1] ? [1] @l2 + [1] @xs + [8] = [::(mult(@x, @l2), dyade(@xs, @l2))] [dyade#1(nil(), @l2)] = [1] @l2 + [2] > [1] = [nil()] [#pred(#pos(#s(#0())))] = [0] >= [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [0] >= [0] = [#pos(#s(@x))] [#pred(#0())] = [0] >= [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [0] >= [0] = [#neg(#s(#s(@x)))] [dyade(@l1, @l2)] = [1] @l1 + [1] @l2 + [6] > [1] @l1 + [1] @l2 + [1] = [dyade#1(@l1, @l2)] 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(n^2)). Strict Trs: { mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , *(@x, @y) -> #mult(@x, @y) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) } Weak Trs: { #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) , mult(@n, @l) -> mult#1(@l, @n) , mult#1(nil(), @n) -> nil() , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#0(), #pos(@y)) -> #0() , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , dyade#1(nil(), @l2) -> nil() , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(::) = {1, 2}, Uargs(#succ) = {1}, Uargs(#pos) = {1}, Uargs(#add) = {2}, Uargs(#neg) = {1}, Uargs(#pred) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [#natmult](x1, x2) = [0] [mult](x1, x2) = [3] [mult#1](x1, x2) = [3] [::](x1, x2) = [1] x1 + [1] x2 + [0] [#mult](x1, x2) = [4] [#succ](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#add](x1, x2) = [1] x2 + [0] [#0] = [0] [*](x1, x2) = [6] [#neg](x1) = [1] x1 + [0] [dyade#1](x1, x2) = [1] x1 + [1] [#pred](x1) = [1] x1 + [0] [#s](x1) = [0] [dyade](x1, x2) = [1] x1 + [5] [nil] = [3] The following symbols are considered usable {#natmult, mult, mult#1, #mult, #succ, #add, *, dyade#1, #pred, dyade} The order satisfies the following ordering constraints: [#natmult(#0(), @y)] = [0] >= [0] = [#0()] [#natmult(#s(@x), @y)] = [0] >= [0] = [#add(#pos(@y), #natmult(@x, @y))] [mult(@n, @l)] = [3] >= [3] = [mult#1(@l, @n)] [mult#1(::(@x, @xs), @n)] = [3] ? [9] = [::(*(@n, @x), mult(@n, @xs))] [mult#1(nil(), @n)] = [3] >= [3] = [nil()] [#mult(#pos(@x), #pos(@y))] = [4] > [0] = [#pos(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [4] > [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [4] > [0] = [#neg(#natmult(@x, @y))] [#mult(#0(), #pos(@y))] = [4] > [0] = [#0()] [#mult(#0(), #0())] = [4] > [0] = [#0()] [#mult(#0(), #neg(@y))] = [4] > [0] = [#0()] [#mult(#neg(@x), #pos(@y))] = [4] > [0] = [#neg(#natmult(@x, @y))] [#mult(#neg(@x), #0())] = [4] > [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [4] > [0] = [#pos(#natmult(@x, @y))] [#succ(#pos(#s(@x)))] = [0] >= [0] = [#pos(#s(#s(@x)))] [#succ(#0())] = [0] >= [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] >= [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [0] >= [0] = [#neg(#s(@x))] [#add(#pos(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [#add(#0(), @y)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [1] @y + [0] >= [1] @y + [0] = [#pred(#add(#pos(#s(@x)), @y))] [*(@x, @y)] = [6] > [4] = [#mult(@x, @y)] [dyade#1(::(@x, @xs), @l2)] = [1] @x + [1] @xs + [1] ? [1] @xs + [8] = [::(mult(@x, @l2), dyade(@xs, @l2))] [dyade#1(nil(), @l2)] = [4] > [3] = [nil()] [#pred(#pos(#s(#0())))] = [0] >= [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [0] >= [0] = [#pos(#s(@x))] [#pred(#0())] = [0] >= [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [0] >= [0] = [#neg(#s(#s(@x)))] [dyade(@l1, @l2)] = [1] @l1 + [5] > [1] @l1 + [1] = [dyade#1(@l1, @l2)] 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(n^2)). Strict Trs: { mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) } Weak Trs: { #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) , mult(@n, @l) -> mult#1(@l, @n) , mult#1(nil(), @n) -> nil() , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#0(), #pos(@y)) -> #0() , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , *(@x, @y) -> #mult(@x, @y) , dyade#1(nil(), @l2) -> nil() , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(::) = {1, 2}, Uargs(#succ) = {1}, Uargs(#pos) = {1}, Uargs(#add) = {2}, Uargs(#neg) = {1}, Uargs(#pred) = {1} TcT has computed the following constructor-restricted polynomial interpretation. [#natmult](x1, x2) = 0 [mult](x1, x2) = x1 + 3*x1*x2 + 2*x1^2 + x2 [mult#1](x1, x2) = x1 + 3*x1*x2 + x2 + 2*x2^2 [::](x1, x2) = 1 + x1 + x2 [#mult](x1, x2) = 0 [#succ](x1) = x1 [#pos](x1) = x1 [#add](x1, x2) = x2 [#0]() = 0 [*](x1, x2) = 3*x1*x2 + x2 [#neg](x1) = x1 [dyade#1](x1, x2) = 3 + 3*x1*x2 + 2*x1^2 + 3*x2^2 [#pred](x1) = x1 [#s](x1) = 0 [dyade](x1, x2) = 3 + 3*x1 + 3*x1*x2 + 2*x1^2 + 3*x2^2 [nil]() = 0 The following symbols are considered usable {#natmult, mult, mult#1, #mult, #succ, #add, *, dyade#1, #pred, dyade} This order satisfies the following ordering constraints. [#natmult(#0(), @y)] = >= = [#0()] [#natmult(#s(@x), @y)] = >= = [#add(#pos(@y), #natmult(@x, @y))] [mult(@n, @l)] = @n + 3*@n*@l + 2*@n^2 + @l >= @l + 3*@l*@n + @n + 2*@n^2 = [mult#1(@l, @n)] [mult#1(::(@x, @xs), @n)] = 1 + @x + @xs + 4*@n + 3*@x*@n + 3*@xs*@n + 2*@n^2 >= 1 + 3*@n*@x + @x + @n + 3*@n*@xs + 2*@n^2 + @xs = [::(*(@n, @x), mult(@n, @xs))] [mult#1(nil(), @n)] = @n + 2*@n^2 >= = [nil()] [#mult(#pos(@x), #pos(@y))] = >= = [#pos(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = >= = [#0()] [#mult(#pos(@x), #neg(@y))] = >= = [#neg(#natmult(@x, @y))] [#mult(#0(), #pos(@y))] = >= = [#0()] [#mult(#0(), #0())] = >= = [#0()] [#mult(#0(), #neg(@y))] = >= = [#0()] [#mult(#neg(@x), #pos(@y))] = >= = [#neg(#natmult(@x, @y))] [#mult(#neg(@x), #0())] = >= = [#0()] [#mult(#neg(@x), #neg(@y))] = >= = [#pos(#natmult(@x, @y))] [#succ(#pos(#s(@x)))] = >= = [#pos(#s(#s(@x)))] [#succ(#0())] = >= = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = >= = [#0()] [#succ(#neg(#s(#s(@x))))] = >= = [#neg(#s(@x))] [#add(#pos(#s(#0())), @y)] = @y >= @y = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = @y >= @y = [#succ(#add(#pos(#s(@x)), @y))] [#add(#0(), @y)] = @y >= @y = [@y] [#add(#neg(#s(#0())), @y)] = @y >= @y = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = @y >= @y = [#pred(#add(#pos(#s(@x)), @y))] [*(@x, @y)] = 3*@x*@y + @y >= = [#mult(@x, @y)] [dyade#1(::(@x, @xs), @l2)] = 5 + 3*@l2 + 3*@x*@l2 + 3*@xs*@l2 + 4*@x + 4*@xs + 2*@x^2 + 2*@x*@xs + 2*@xs*@x + 2*@xs^2 + 3*@l2^2 > 4 + @x + 3*@x*@l2 + 2*@x^2 + @l2 + 3*@xs + 3*@xs*@l2 + 2*@xs^2 + 3*@l2^2 = [::(mult(@x, @l2), dyade(@xs, @l2))] [dyade#1(nil(), @l2)] = 3 + 3*@l2^2 > = [nil()] [#pred(#pos(#s(#0())))] = >= = [#0()] [#pred(#pos(#s(#s(@x))))] = >= = [#pos(#s(@x))] [#pred(#0())] = >= = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = >= = [#neg(#s(#s(@x)))] [dyade(@l1, @l2)] = 3 + 3*@l1 + 3*@l1*@l2 + 2*@l1^2 + 3*@l2^2 >= 3 + 3*@l1*@l2 + 2*@l1^2 + 3*@l2^2 = [dyade#1(@l1, @l2)] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) } Weak Trs: { #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) , mult(@n, @l) -> mult#1(@l, @n) , mult#1(nil(), @n) -> nil() , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#0(), #pos(@y)) -> #0() , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , *(@x, @y) -> #mult(@x, @y) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(::) = {1, 2}, Uargs(#succ) = {1}, Uargs(#pos) = {1}, Uargs(#add) = {2}, Uargs(#neg) = {1}, Uargs(#pred) = {1} TcT has computed the following constructor-restricted polynomial interpretation. [#natmult](x1, x2) = 0 [mult](x1, x2) = x1^2 + 2*x2 [mult#1](x1, x2) = 2*x1 + x2^2 [::](x1, x2) = 2 + x1 + x2 [#mult](x1, x2) = 0 [#succ](x1) = x1 [#pos](x1) = x1 [#add](x1, x2) = x2 [#0]() = 0 [*](x1, x2) = x2 [#neg](x1) = x1 [dyade#1](x1, x2) = 2*x1*x2 + x1^2 + x2 + 3*x2^2 [#pred](x1) = x1 [#s](x1) = 0 [dyade](x1, x2) = 3*x1 + 2*x1*x2 + x1^2 + 2*x2 + 3*x2^2 [nil]() = 0 The following symbols are considered usable {#natmult, mult, mult#1, #mult, #succ, #add, *, dyade#1, #pred, dyade} This order satisfies the following ordering constraints. [#natmult(#0(), @y)] = >= = [#0()] [#natmult(#s(@x), @y)] = >= = [#add(#pos(@y), #natmult(@x, @y))] [mult(@n, @l)] = @n^2 + 2*@l >= 2*@l + @n^2 = [mult#1(@l, @n)] [mult#1(::(@x, @xs), @n)] = 4 + 2*@x + 2*@xs + @n^2 > 2 + @x + @n^2 + 2*@xs = [::(*(@n, @x), mult(@n, @xs))] [mult#1(nil(), @n)] = @n^2 >= = [nil()] [#mult(#pos(@x), #pos(@y))] = >= = [#pos(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = >= = [#0()] [#mult(#pos(@x), #neg(@y))] = >= = [#neg(#natmult(@x, @y))] [#mult(#0(), #pos(@y))] = >= = [#0()] [#mult(#0(), #0())] = >= = [#0()] [#mult(#0(), #neg(@y))] = >= = [#0()] [#mult(#neg(@x), #pos(@y))] = >= = [#neg(#natmult(@x, @y))] [#mult(#neg(@x), #0())] = >= = [#0()] [#mult(#neg(@x), #neg(@y))] = >= = [#pos(#natmult(@x, @y))] [#succ(#pos(#s(@x)))] = >= = [#pos(#s(#s(@x)))] [#succ(#0())] = >= = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = >= = [#0()] [#succ(#neg(#s(#s(@x))))] = >= = [#neg(#s(@x))] [#add(#pos(#s(#0())), @y)] = @y >= @y = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = @y >= @y = [#succ(#add(#pos(#s(@x)), @y))] [#add(#0(), @y)] = @y >= @y = [@y] [#add(#neg(#s(#0())), @y)] = @y >= @y = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = @y >= @y = [#pred(#add(#pos(#s(@x)), @y))] [*(@x, @y)] = @y >= = [#mult(@x, @y)] [dyade#1(::(@x, @xs), @l2)] = 5*@l2 + 2*@x*@l2 + 2*@xs*@l2 + 4 + 4*@x + 4*@xs + @x^2 + @x*@xs + @xs*@x + @xs^2 + 3*@l2^2 > 2 + @x^2 + 4*@l2 + 3*@xs + 2*@xs*@l2 + @xs^2 + 3*@l2^2 = [::(mult(@x, @l2), dyade(@xs, @l2))] [dyade#1(nil(), @l2)] = @l2 + 3*@l2^2 >= = [nil()] [#pred(#pos(#s(#0())))] = >= = [#0()] [#pred(#pos(#s(#s(@x))))] = >= = [#pos(#s(@x))] [#pred(#0())] = >= = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = >= = [#neg(#s(#s(@x)))] [dyade(@l1, @l2)] = 3*@l1 + 2*@l1*@l2 + @l1^2 + 2*@l2 + 3*@l2^2 >= 2*@l1*@l2 + @l1^2 + @l2 + 3*@l2^2 = [dyade#1(@l1, @l2)] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#0(), #pos(@y)) -> #0() , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , *(@x, @y) -> #mult(@x, @y) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))