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))