MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { *(@x, @y) -> #mult(@x, @y) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@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)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { dyade#1(nil(), @l2) -> nil() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {1, 2}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [dyade](x1, x2) = [2] [dyade#1](x1, x2) = [2] [::](x1, x2) = [1] x1 + [1] x2 + [0] [mult](x1, x2) = [0] [nil] = [0] [mult#1](x1, x2) = [0] [#0] = [0] [#add](x1, x2) = [1] x2 + [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#succ](x1) = [1] x1 + [0] [#natmult](x1, x2) = [0] [#natadd](x1, x2) = [1] x2 + [0] This order satisfies following ordering constraints [*(@x, @y)] = [0] >= [0] = [#mult(@x, @y)] [#mult(#0(), #0())] = [0] >= [0] = [#0()] [#mult(#0(), #neg(@y))] = [0] >= [0] = [#0()] [#mult(#0(), #pos(@y))] = [0] >= [0] = [#0()] [#mult(#neg(@x), #0())] = [0] >= [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [0] >= [0] = [#pos(#natmult(@x, @y))] [#mult(#neg(@x), #pos(@y))] = [0] >= [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [0] >= [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [0] >= [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #pos(@y))] = [0] >= [0] = [#pos(#natmult(@x, @y))] [dyade(@l1, @l2)] = [2] >= [2] = [dyade#1(@l1, @l2)] [dyade#1(::(@x, @xs), @l2)] = [2] >= [2] = [::(mult(@x, @l2), dyade(@xs, @l2))] [dyade#1(nil(), @l2)] = [2] > [0] = [nil()] [mult(@n, @l)] = [0] >= [0] = [mult#1(@l, @n)] [mult#1(::(@x, @xs), @n)] = [0] >= [0] = [::(*(@n, @x), mult(@n, @xs))] [mult#1(nil(), @n)] = [0] >= [0] = [nil()] [#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))] [#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))] [#pred(#0())] = [0] >= [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [1] @x + [0] >= [1] @x + [0] = [#neg(#s(#s(@x)))] [#pred(#pos(#s(#0())))] = [0] >= [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [1] @x + [0] >= [1] @x + [0] = [#pos(#s(@x))] [#succ(#0())] = [0] >= [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] >= [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [1] @x + [0] >= [1] @x + [0] = [#neg(#s(@x))] [#succ(#pos(#s(@x)))] = [1] @x + [0] >= [1] @x + [0] = [#pos(#s(#s(@x)))] [#natmult(#0(), @y)] = [0] >= [0] = [#0()] [#natmult(#s(@x), @y)] = [0] >= [0] = [#natadd(@y, #natmult(@x, @y))] [#natadd(#0(), @y)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#natadd(#s(@x), @y)] = [1] @y + [0] >= [1] @y + [0] = [#s(#natadd(@x, @y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { *(@x, @y) -> #mult(@x, @y) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade#1(nil(), @l2) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { dyade(@l1, @l2) -> dyade#1(@l1, @l2) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {1, 2}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [*](x1, x2) = [0] [0] [#mult](x1, x2) = [0] [0] [dyade](x1, x2) = [2 2] x1 + [2 2] x2 + [2] [0 2] [0 0] [0] [dyade#1](x1, x2) = [2 2] x1 + [2 2] x2 + [0] [0 2] [0 0] [0] [::](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 1] [1] [mult](x1, x2) = [0 0] x2 + [0] [1 1] [0] [nil] = [0] [1] [mult#1](x1, x2) = [0 0] x1 + [0] [1 1] [0] [#0] = [0] [0] [#add](x1, x2) = [1 0] x2 + [0] [2 2] [0] [#s](x1) = [1 0] x1 + [0] [0 0] [0] [#neg](x1) = [1 2] x1 + [0] [0 0] [0] [#pred](x1) = [1 0] x1 + [0] [1 0] [0] [#pos](x1) = [1 1] x1 + [0] [0 0] [0] [#succ](x1) = [1 0] x1 + [0] [0 0] [0] [#natmult](x1, x2) = [0] [0] [#natadd](x1, x2) = [2 0] x2 + [0] [0 2] [0] This order satisfies following ordering constraints [*(@x, @y)] = [0] [0] >= [0] [0] = [#mult(@x, @y)] [#mult(#0(), #0())] = [0] [0] >= [0] [0] = [#0()] [#mult(#0(), #neg(@y))] = [0] [0] >= [0] [0] = [#0()] [#mult(#0(), #pos(@y))] = [0] [0] >= [0] [0] = [#0()] [#mult(#neg(@x), #0())] = [0] [0] >= [0] [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [0] [0] >= [0] [0] = [#pos(#natmult(@x, @y))] [#mult(#neg(@x), #pos(@y))] = [0] [0] >= [0] [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [0] [0] >= [0] [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [0] [0] >= [0] [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #pos(@y))] = [0] [0] >= [0] [0] = [#pos(#natmult(@x, @y))] [dyade(@l1, @l2)] = [2 2] @l1 + [2 2] @l2 + [2] [0 2] [0 0] [0] > [2 2] @l1 + [2 2] @l2 + [0] [0 2] [0 0] [0] = [dyade#1(@l1, @l2)] [dyade#1(::(@x, @xs), @l2)] = [2 2] @l2 + [2 0] @x + [2 2] @xs + [2] [0 0] [0 0] [0 2] [2] >= [2 2] @l2 + [2 2] @xs + [2] [0 0] [0 2] [1] = [::(mult(@x, @l2), dyade(@xs, @l2))] [dyade#1(nil(), @l2)] = [2 2] @l2 + [2] [0 0] [2] > [0] [1] = [nil()] [mult(@n, @l)] = [0 0] @l + [0] [1 1] [0] >= [0 0] @l + [0] [1 1] [0] = [mult#1(@l, @n)] [mult#1(::(@x, @xs), @n)] = [0 0] @x + [0 0] @xs + [0] [1 0] [1 1] [1] >= [0 0] @xs + [0] [1 1] [1] = [::(*(@n, @x), mult(@n, @xs))] [mult#1(nil(), @n)] = [0] [1] >= [0] [1] = [nil()] [#add(#0(), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [0 1] [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [1 0] [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [1 0] [0] = [#pred(#add(#pos(#s(@x)), @y))] [#add(#pos(#s(#0())), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [0 0] [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [0 0] [0] = [#succ(#add(#pos(#s(@x)), @y))] [#pred(#0())] = [0] [0] >= [0] [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [1 0] @x + [0] [1 0] [0] >= [1 0] @x + [0] [0 0] [0] = [#neg(#s(#s(@x)))] [#pred(#pos(#s(#0())))] = [0] [0] >= [0] [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [1 0] @x + [0] [1 0] [0] >= [1 0] @x + [0] [0 0] [0] = [#pos(#s(@x))] [#succ(#0())] = [0] [0] >= [0] [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] [0] >= [0] [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [1 0] @x + [0] [0 0] [0] >= [1 0] @x + [0] [0 0] [0] = [#neg(#s(@x))] [#succ(#pos(#s(@x)))] = [1 0] @x + [0] [0 0] [0] >= [1 0] @x + [0] [0 0] [0] = [#pos(#s(#s(@x)))] [#natmult(#0(), @y)] = [0] [0] >= [0] [0] = [#0()] [#natmult(#s(@x), @y)] = [0] [0] >= [0] [0] = [#natadd(@y, #natmult(@x, @y))] [#natadd(#0(), @y)] = [2 0] @y + [0] [0 2] [0] >= [1 0] @y + [0] [0 1] [0] = [@y] [#natadd(#s(@x), @y)] = [2 0] @y + [0] [0 2] [0] >= [2 0] @y + [0] [0 0] [0] = [#s(#natadd(@x, @y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { *(@x, @y) -> #mult(@x, @y) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(nil(), @l2) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , mult#1(nil(), @n) -> nil() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {1, 2}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [*](x1, x2) = [0] [2] [#mult](x1, x2) = [0] [0] [dyade](x1, x2) = [1 2] x1 + [0 1] x2 + [2] [0 2] [0 1] [0] [dyade#1](x1, x2) = [1 2] x1 + [0 1] x2 + [2] [0 2] [0 1] [0] [::](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [1 0] [0 1] [2] [mult](x1, x2) = [0 0] x2 + [2] [1 1] [0] [nil] = [0] [0] [mult#1](x1, x2) = [0 0] x1 + [2] [1 1] [0] [#0] = [0] [0] [#add](x1, x2) = [1 0] x2 + [0] [2 2] [0] [#s](x1) = [1 0] x1 + [0] [0 0] [0] [#neg](x1) = [1 0] x1 + [0] [0 0] [0] [#pred](x1) = [1 0] x1 + [0] [1 0] [0] [#pos](x1) = [1 0] x1 + [0] [0 0] [0] [#succ](x1) = [1 0] x1 + [0] [0 0] [0] [#natmult](x1, x2) = [0] [0] [#natadd](x1, x2) = [2 0] x2 + [0] [0 2] [0] This order satisfies following ordering constraints [*(@x, @y)] = [0] [2] >= [0] [0] = [#mult(@x, @y)] [#mult(#0(), #0())] = [0] [0] >= [0] [0] = [#0()] [#mult(#0(), #neg(@y))] = [0] [0] >= [0] [0] = [#0()] [#mult(#0(), #pos(@y))] = [0] [0] >= [0] [0] = [#0()] [#mult(#neg(@x), #0())] = [0] [0] >= [0] [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [0] [0] >= [0] [0] = [#pos(#natmult(@x, @y))] [#mult(#neg(@x), #pos(@y))] = [0] [0] >= [0] [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [0] [0] >= [0] [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [0] [0] >= [0] [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #pos(@y))] = [0] [0] >= [0] [0] = [#pos(#natmult(@x, @y))] [dyade(@l1, @l2)] = [1 2] @l1 + [0 1] @l2 + [2] [0 2] [0 1] [0] >= [1 2] @l1 + [0 1] @l2 + [2] [0 2] [0 1] [0] = [dyade#1(@l1, @l2)] [dyade#1(::(@x, @xs), @l2)] = [0 1] @l2 + [3 0] @x + [1 2] @xs + [6] [0 1] [2 0] [0 2] [4] > [0 1] @l2 + [1 2] @xs + [4] [0 1] [0 2] [4] = [::(mult(@x, @l2), dyade(@xs, @l2))] [dyade#1(nil(), @l2)] = [0 1] @l2 + [2] [0 1] [0] > [0] [0] = [nil()] [mult(@n, @l)] = [0 0] @l + [2] [1 1] [0] >= [0 0] @l + [2] [1 1] [0] = [mult#1(@l, @n)] [mult#1(::(@x, @xs), @n)] = [0 0] @x + [0 0] @xs + [2] [2 0] [1 1] [2] >= [0 0] @xs + [2] [1 1] [2] = [::(*(@n, @x), mult(@n, @xs))] [mult#1(nil(), @n)] = [2] [0] > [0] [0] = [nil()] [#add(#0(), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [0 1] [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [1 0] [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [1 0] [0] = [#pred(#add(#pos(#s(@x)), @y))] [#add(#pos(#s(#0())), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [0 0] [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [1 0] @y + [0] [2 2] [0] >= [1 0] @y + [0] [0 0] [0] = [#succ(#add(#pos(#s(@x)), @y))] [#pred(#0())] = [0] [0] >= [0] [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [1 0] @x + [0] [1 0] [0] >= [1 0] @x + [0] [0 0] [0] = [#neg(#s(#s(@x)))] [#pred(#pos(#s(#0())))] = [0] [0] >= [0] [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [1 0] @x + [0] [1 0] [0] >= [1 0] @x + [0] [0 0] [0] = [#pos(#s(@x))] [#succ(#0())] = [0] [0] >= [0] [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] [0] >= [0] [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [1 0] @x + [0] [0 0] [0] >= [1 0] @x + [0] [0 0] [0] = [#neg(#s(@x))] [#succ(#pos(#s(@x)))] = [1 0] @x + [0] [0 0] [0] >= [1 0] @x + [0] [0 0] [0] = [#pos(#s(#s(@x)))] [#natmult(#0(), @y)] = [0] [0] >= [0] [0] = [#0()] [#natmult(#s(@x), @y)] = [0] [0] >= [0] [0] = [#natadd(@y, #natmult(@x, @y))] [#natadd(#0(), @y)] = [2 0] @y + [0] [0 2] [0] >= [1 0] @y + [0] [0 1] [0] = [@y] [#natadd(#s(@x), @y)] = [2 0] @y + [0] [0 2] [0] >= [2 0] @y + [0] [0 0] [0] = [#s(#natadd(@x, @y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { *(@x, @y) -> #mult(@x, @y) , mult(@n, @l) -> mult#1(@l, @n) , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult#1(nil(), @n) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'Small Polynomial Path Order (PS,4-bounded)' 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^3)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,4-bounded)' as induced by the safe mapping safe(*) = {}, safe(#mult) = {}, safe(dyade) = {}, safe(dyade#1) = {}, safe(::) = {1, 2}, safe(mult) = {}, safe(nil) = {}, safe(mult#1) = {}, safe(#0) = {}, safe(#add) = {2}, safe(#s) = {1}, safe(#neg) = {1}, safe(#pred) = {1}, safe(#pos) = {1}, safe(#succ) = {1}, safe(#natmult) = {}, safe(#natadd) = {2} and precedence dyade#1 > mult, mult#1 > *, #add > #pred, #add > #succ, #natmult > #natadd, * ~ #mult, #mult ~ #natmult, dyade ~ dyade#1, mult ~ mult#1 . Following symbols are considered recursive: {#mult, dyade, dyade#1, mult, mult#1, #add, #natmult, #natadd} The recursion depth is 3. For your convenience, here are the satisfied ordering constraints: *(@x, @y;) >= #mult(@x, @y;) #mult(#0(), #0();) > #0() #mult(#0(), #neg(; @y);) > #0() #mult(#0(), #pos(; @y);) > #0() #mult(#neg(; @x), #0();) > #0() #mult(#neg(; @x), #neg(; @y);) > #pos(; #natmult(@x, @y;)) #mult(#neg(; @x), #pos(; @y);) > #neg(; #natmult(@x, @y;)) #mult(#pos(; @x), #0();) > #0() #mult(#pos(; @x), #neg(; @y);) > #neg(; #natmult(@x, @y;)) #mult(#pos(; @x), #pos(; @y);) > #pos(; #natmult(@x, @y;)) dyade(@l1, @l2;) >= dyade#1(@l1, @l2;) dyade#1(::(; @x, @xs), @l2;) > ::(; mult(@x, @l2;), dyade(@xs, @l2;)) dyade#1(nil(), @l2;) > nil() mult(@n, @l;) >= mult#1(@l, @n;) mult#1(::(; @x, @xs), @n;) > ::(; *(@n, @x;), mult(@n, @xs;)) mult#1(nil(), @n;) > nil() #add(#0(); @y) > @y #add(#neg(; #s(; #0())); @y) > #pred(; @y) #add(#neg(; #s(; #s(; @x))); @y) > #pred(; #add(#pos(; #s(; @x)); @y)) #add(#pos(; #s(; #0())); @y) > #succ(; @y) #add(#pos(; #s(; #s(; @x))); @y) > #succ(; #add(#pos(; #s(; @x)); @y)) #pred(; #0()) > #neg(; #s(; #0())) #pred(; #neg(; #s(; @x))) > #neg(; #s(; #s(; @x))) #pred(; #pos(; #s(; #0()))) > #0() #pred(; #pos(; #s(; #s(; @x)))) > #pos(; #s(; @x)) #succ(; #0()) > #pos(; #s(; #0())) #succ(; #neg(; #s(; #0()))) > #0() #succ(; #neg(; #s(; #s(; @x)))) > #neg(; #s(; @x)) #succ(; #pos(; #s(; @x))) > #pos(; #s(; #s(; @x))) #natmult(#0(), @y;) > #0() #natmult(#s(; @x), @y;) > #natadd(@y; #natmult(@x, @y;)) #natadd(#0(); @y) > @y #natadd(#s(; @x); @y) > #s(; #natadd(@x; @y)) We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { *(@x, @y) -> #mult(@x, @y) , mult(@n, @l) -> mult#1(@l, @n) } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'Small Polynomial Path Order (PS,4-bounded)' to orient following rules strictly. Trs: { *(@x, @y) -> #mult(@x, @y) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^4)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,4-bounded)' as induced by the safe mapping safe(*) = {}, safe(#mult) = {}, safe(dyade) = {}, safe(dyade#1) = {}, safe(::) = {1, 2}, safe(mult) = {}, safe(nil) = {}, safe(mult#1) = {}, safe(#0) = {}, safe(#add) = {2}, safe(#s) = {1}, safe(#neg) = {1}, safe(#pred) = {1}, safe(#pos) = {1}, safe(#succ) = {1}, safe(#natmult) = {}, safe(#natadd) = {2} and precedence * > #mult, dyade#1 > mult, mult#1 > *, #add > #pred, #add > #succ, #natmult > #natadd, #mult ~ #natmult, dyade ~ dyade#1, mult ~ mult#1 . Following symbols are considered recursive: {#mult, dyade, dyade#1, mult, mult#1, #add, #natmult, #natadd} The recursion depth is 4. For your convenience, here are the satisfied ordering constraints: *(@x, @y;) > #mult(@x, @y;) #mult(#0(), #0();) > #0() #mult(#0(), #neg(; @y);) > #0() #mult(#0(), #pos(; @y);) > #0() #mult(#neg(; @x), #0();) > #0() #mult(#neg(; @x), #neg(; @y);) > #pos(; #natmult(@x, @y;)) #mult(#neg(; @x), #pos(; @y);) > #neg(; #natmult(@x, @y;)) #mult(#pos(; @x), #0();) > #0() #mult(#pos(; @x), #neg(; @y);) > #neg(; #natmult(@x, @y;)) #mult(#pos(; @x), #pos(; @y);) > #pos(; #natmult(@x, @y;)) dyade(@l1, @l2;) >= dyade#1(@l1, @l2;) dyade#1(::(; @x, @xs), @l2;) > ::(; mult(@x, @l2;), dyade(@xs, @l2;)) dyade#1(nil(), @l2;) > nil() mult(@n, @l;) >= mult#1(@l, @n;) mult#1(::(; @x, @xs), @n;) > ::(; *(@n, @x;), mult(@n, @xs;)) mult#1(nil(), @n;) > nil() #add(#0(); @y) > @y #add(#neg(; #s(; #0())); @y) > #pred(; @y) #add(#neg(; #s(; #s(; @x))); @y) > #pred(; #add(#pos(; #s(; @x)); @y)) #add(#pos(; #s(; #0())); @y) > #succ(; @y) #add(#pos(; #s(; #s(; @x))); @y) > #succ(; #add(#pos(; #s(; @x)); @y)) #pred(; #0()) > #neg(; #s(; #0())) #pred(; #neg(; #s(; @x))) > #neg(; #s(; #s(; @x))) #pred(; #pos(; #s(; #0()))) > #0() #pred(; #pos(; #s(; #s(; @x)))) > #pos(; #s(; @x)) #succ(; #0()) > #pos(; #s(; #0())) #succ(; #neg(; #s(; #0()))) > #0() #succ(; #neg(; #s(; #s(; @x)))) > #neg(; #s(; @x)) #succ(; #pos(; #s(; @x))) > #pos(; #s(; #s(; @x))) #natmult(#0(), @y;) > #0() #natmult(#s(; @x), @y;) > #natadd(@y; #natmult(@x, @y;)) #natadd(#0(); @y) > @y #natadd(#s(; @x); @y) > #s(; #natadd(@x; @y)) We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { mult(@n, @l) -> mult#1(@l, @n) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , dyade(@l1, @l2) -> dyade#1(@l1, @l2) , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) , dyade#1(nil(), @l2) -> nil() , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) , mult#1(nil(), @n) -> nil() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'trivial' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Sequentially' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..