tct
| Execution Time (secs) | 3.885 |
| Answer | YES(O(1),O(n^2)) |
| Input | dyade.raml |
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:
{ *(@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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add following dependency pairs
Strict DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, dyade#1^#(nil(), @l2) -> c_4()
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
, mult#1^#(nil(), @n) -> c_7() }
Weak DPs:
{ #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
and replace the set of basic marked basic terms accordingly.
We apply the transformation 'usablerules' on the sub-problem:
Strict DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, dyade#1^#(nil(), @l2) -> c_4()
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
, mult#1^#(nil(), @n) -> c_7() }
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 DPs:
{ #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
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) -> #add(#pos(@y), #natmult(@x, @y)) }
StartTerms: basic terms
Strategy: innermost
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
We apply the transformation 'compose (addition)' on the
sub-problem:
Strict DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, dyade#1^#(nil(), @l2) -> c_4()
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
, mult#1^#(nil(), @n) -> c_7() }
Weak DPs:
{ #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
StartTerms: basic terms
Strategy: innermost
We use the processor 'weightgap of dimension 2, maximal degree 1,
cbits 3' to orient following rules strictly.
DPs: { mult#1^#(nil(), @n) -> c_7() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)). These rulesare moved into the corresponding weak
component(s).
Sub-proof:
----------
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(::) = {}, Uargs(#add) = {2}, Uargs(#s) = {},
Uargs(#neg) = {}, Uargs(#pred) = {1}, Uargs(#pos) = {},
Uargs(#succ) = {1}, Uargs(#natmult) = {}, Uargs(*^#) = {},
Uargs(#mult^#) = {}, Uargs(dyade^#) = {}, Uargs(dyade#1^#) = {},
Uargs(c_3) = {1, 2}, Uargs(mult^#) = {}, Uargs(mult#1^#) = {},
Uargs(c_6) = {1, 2}, Uargs(#natmult^#) = {}, Uargs(#add^#) = {2},
Uargs(#pred^#) = {1}, Uargs(#succ^#) = {1}
TcT has computed following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 1
non-zero entries.
[::](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[nil] = [0]
[1]
[#0] = [0]
[0]
[#add](x1, x2) = [1 0] x2 + [0]
[0 2] [0]
[#s](x1) = [0]
[0]
[#neg](x1) = [0]
[0]
[#pred](x1) = [1 0] x1 + [0]
[0 0] [0]
[#pos](x1) = [0]
[0]
[#succ](x1) = [1 0] x1 + [0]
[0 0] [0]
[#natmult](x1, x2) = [0]
[0]
[*^#](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[2 2] [2 2] [0]
[#mult^#](x1, x2) = [2]
[0]
[dyade^#](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[2 2] [1 1] [0]
[dyade#1^#](x1, x2) = [0]
[0]
[c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
[mult^#](x1, x2) = [0 0] x2 + [0]
[1 1] [1]
[c_4] = [0]
[0]
[mult#1^#](x1, x2) = [1]
[0]
[c_6](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [2]
[c_7] = [0]
[0]
[c_8] = [0]
[0]
[c_9] = [0]
[0]
[c_10] = [0]
[0]
[c_11] = [0]
[0]
[#natmult^#](x1, x2) = [2]
[0]
[c_14] = [0]
[0]
[#add^#](x1, x2) = [2 0] x2 + [0]
[0 0] [0]
[c_17] = [0]
[0]
[#pred^#](x1) = [2 0] x1 + [0]
[0 0] [0]
[#succ^#](x1) = [2 0] x1 + [0]
[0 0] [0]
[c_22] = [0]
[0]
[c_23] = [0]
[0]
[c_24] = [0]
[0]
[c_25] = [0]
[0]
[c_26] = [0]
[0]
[c_27] = [0]
[0]
[c_28] = [0]
[0]
[c_29] = [0]
[0]
[c_30] = [0]
[0]
This order satisfies following ordering constraints
[#add(#0(), @y)] = [1 0] @y + [0]
[0 2] [0]
>= [1 0] @y + [0]
[0 1] [0]
= [@y]
[#add(#neg(#s(#0())), @y)] = [1 0] @y + [0]
[0 2] [0]
>= [1 0] @y + [0]
[0 0] [0]
= [#pred(@y)]
[#add(#neg(#s(#s(@x))), @y)] = [1 0] @y + [0]
[0 2] [0]
>= [1 0] @y + [0]
[0 0] [0]
= [#pred(#add(#pos(#s(@x)), @y))]
[#add(#pos(#s(#0())), @y)] = [1 0] @y + [0]
[0 2] [0]
>= [1 0] @y + [0]
[0 0] [0]
= [#succ(@y)]
[#add(#pos(#s(#s(@x))), @y)] = [1 0] @y + [0]
[0 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)))] = [0]
[0]
>= [0]
[0]
= [#neg(#s(#s(@x)))]
[#pred(#pos(#s(#0())))] = [0]
[0]
>= [0]
[0]
= [#0()]
[#pred(#pos(#s(#s(@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))))] = [0]
[0]
>= [0]
[0]
= [#neg(#s(@x))]
[#succ(#pos(#s(@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]
= [#add(#pos(@y), #natmult(@x, @y))]
[*^#(@x, @y)] = [0 0] @x + [0 0] @y + [0]
[2 2] [2 2] [0]
? [2]
[0]
= [#mult^#(@x, @y)]
[#mult^#(#0(), #0())] = [2]
[0]
> [0]
[0]
= [c_8()]
[#mult^#(#0(), #neg(@y))] = [2]
[0]
> [0]
[0]
= [c_9()]
[#mult^#(#0(), #pos(@y))] = [2]
[0]
> [0]
[0]
= [c_10()]
[#mult^#(#neg(@x), #0())] = [2]
[0]
> [0]
[0]
= [c_11()]
[#mult^#(#neg(@x), #neg(@y))] = [2]
[0]
>= [2]
[0]
= [#natmult^#(@x, @y)]
[#mult^#(#neg(@x), #pos(@y))] = [2]
[0]
>= [2]
[0]
= [#natmult^#(@x, @y)]
[#mult^#(#pos(@x), #0())] = [2]
[0]
> [0]
[0]
= [c_14()]
[#mult^#(#pos(@x), #neg(@y))] = [2]
[0]
>= [2]
[0]
= [#natmult^#(@x, @y)]
[#mult^#(#pos(@x), #pos(@y))] = [2]
[0]
>= [2]
[0]
= [#natmult^#(@x, @y)]
[dyade^#(@l1, @l2)] = [0 0] @l1 + [0 0] @l2 + [0]
[2 2] [1 1] [0]
>= [0]
[0]
= [dyade#1^#(@l1, @l2)]
[dyade#1^#(::(@x, @xs), @l2)] = [0]
[0]
? [0 0] @l2 + [0 0] @xs + [0]
[2 2] [2 2] [1]
= [c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))]
[dyade#1^#(nil(), @l2)] = [0]
[0]
>= [0]
[0]
= [c_4()]
[mult^#(@n, @l)] = [0 0] @l + [0]
[1 1] [1]
? [1]
[0]
= [mult#1^#(@l, @n)]
[mult#1^#(::(@x, @xs), @n)] = [1]
[0]
? [0 0] @n + [0 0] @x + [0 0] @xs + [0]
[2 2] [2 2] [1 1] [3]
= [c_6(*^#(@n, @x), mult^#(@n, @xs))]
[mult#1^#(nil(), @n)] = [1]
[0]
> [0]
[0]
= [c_7()]
[#natmult^#(#0(), @y)] = [2]
[0]
> [0]
[0]
= [c_30()]
[#natmult^#(#s(@x), @y)] = [2]
[0]
> [0]
[0]
= [#add^#(#pos(@y), #natmult(@x, @y))]
[#add^#(#0(), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [0]
[0]
= [c_17()]
[#add^#(#neg(#s(#0())), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [2 0] @y + [0]
[0 0] [0]
= [#pred^#(@y)]
[#add^#(#neg(#s(#s(@x))), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [2 0] @y + [0]
[0 0] [0]
= [#pred^#(#add(#pos(#s(@x)), @y))]
[#add^#(#pos(#s(#0())), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [2 0] @y + [0]
[0 0] [0]
= [#succ^#(@y)]
[#add^#(#pos(#s(#s(@x))), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [2 0] @y + [0]
[0 0] [0]
= [#succ^#(#add(#pos(#s(@x)), @y))]
[#pred^#(#0())] = [0]
[0]
>= [0]
[0]
= [c_22()]
[#pred^#(#neg(#s(@x)))] = [0]
[0]
>= [0]
[0]
= [c_23()]
[#pred^#(#pos(#s(#0())))] = [0]
[0]
>= [0]
[0]
= [c_24()]
[#pred^#(#pos(#s(#s(@x))))] = [0]
[0]
>= [0]
[0]
= [c_25()]
[#succ^#(#0())] = [0]
[0]
>= [0]
[0]
= [c_26()]
[#succ^#(#neg(#s(#0())))] = [0]
[0]
>= [0]
[0]
= [c_27()]
[#succ^#(#neg(#s(#s(@x))))] = [0]
[0]
>= [0]
[0]
= [c_28()]
[#succ^#(#pos(#s(@x)))] = [0]
[0]
>= [0]
[0]
= [c_29()]
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 DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, dyade#1^#(nil(), @l2) -> c_4()
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) }
Weak DPs:
{ #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, mult#1^#(nil(), @n) -> c_7()
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: *^#(@x, @y) -> #mult^#(@x, @y)
-->_1 #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y) :15
-->_1 #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y) :14
-->_1 #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y) :12
-->_1 #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y) :11
-->_1 #mult^#(#pos(@x), #0()) -> c_14() :13
-->_1 #mult^#(#neg(@x), #0()) -> c_11() :10
-->_1 #mult^#(#0(), #pos(@y)) -> c_10() :9
-->_1 #mult^#(#0(), #neg(@y)) -> c_9() :8
-->_1 #mult^#(#0(), #0()) -> c_8() :7
2: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) :3
-->_1 dyade#1^#(nil(), @l2) -> c_4() :4
3: dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :5
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :2
4: dyade#1^#(nil(), @l2) -> c_4()
5: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) ->
c_6(*^#(@n, @x), mult^#(@n, @xs)) :6
-->_1 mult#1^#(nil(), @n) -> c_7() :16
6: mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
-->_2 mult^#(@n, @l) -> mult#1^#(@l, @n) :5
-->_1 *^#(@x, @y) -> #mult^#(@x, @y) :1
7: #mult^#(#0(), #0()) -> c_8()
8: #mult^#(#0(), #neg(@y)) -> c_9()
9: #mult^#(#0(), #pos(@y)) -> c_10()
10: #mult^#(#neg(@x), #0()) -> c_11()
11: #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
-->_1 #natmult^#(#s(@x), @y) ->
#add^#(#pos(@y), #natmult(@x, @y)) :18
-->_1 #natmult^#(#0(), @y) -> c_30() :17
12: #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
-->_1 #natmult^#(#s(@x), @y) ->
#add^#(#pos(@y), #natmult(@x, @y)) :18
-->_1 #natmult^#(#0(), @y) -> c_30() :17
13: #mult^#(#pos(@x), #0()) -> c_14()
14: #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
-->_1 #natmult^#(#s(@x), @y) ->
#add^#(#pos(@y), #natmult(@x, @y)) :18
-->_1 #natmult^#(#0(), @y) -> c_30() :17
15: #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
-->_1 #natmult^#(#s(@x), @y) ->
#add^#(#pos(@y), #natmult(@x, @y)) :18
-->_1 #natmult^#(#0(), @y) -> c_30() :17
16: mult#1^#(nil(), @n) -> c_7()
17: #natmult^#(#0(), @y) -> c_30()
18: #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
-->_1 #add^#(#pos(#s(#s(@x))), @y) ->
#succ^#(#add(#pos(#s(@x)), @y)) :23
-->_1 #add^#(#pos(#s(#0())), @y) -> #succ^#(@y) :22
19: #add^#(#0(), @y) -> c_17()
20: #add^#(#neg(#s(#0())), @y) -> #pred^#(@y)
-->_1 #pred^#(#pos(#s(#s(@x)))) -> c_25() :27
-->_1 #pred^#(#pos(#s(#0()))) -> c_24() :26
-->_1 #pred^#(#neg(#s(@x))) -> c_23() :25
-->_1 #pred^#(#0()) -> c_22() :24
21: #add^#(#neg(#s(#s(@x))), @y) -> #pred^#(#add(#pos(#s(@x)), @y))
-->_1 #pred^#(#pos(#s(#s(@x)))) -> c_25() :27
-->_1 #pred^#(#pos(#s(#0()))) -> c_24() :26
-->_1 #pred^#(#neg(#s(@x))) -> c_23() :25
-->_1 #pred^#(#0()) -> c_22() :24
22: #add^#(#pos(#s(#0())), @y) -> #succ^#(@y)
-->_1 #succ^#(#pos(#s(@x))) -> c_29() :31
-->_1 #succ^#(#neg(#s(#s(@x)))) -> c_28() :30
-->_1 #succ^#(#neg(#s(#0()))) -> c_27() :29
-->_1 #succ^#(#0()) -> c_26() :28
23: #add^#(#pos(#s(#s(@x))), @y) -> #succ^#(#add(#pos(#s(@x)), @y))
-->_1 #succ^#(#pos(#s(@x))) -> c_29() :31
-->_1 #succ^#(#neg(#s(#s(@x)))) -> c_28() :30
-->_1 #succ^#(#neg(#s(#0()))) -> c_27() :29
-->_1 #succ^#(#0()) -> c_26() :28
24: #pred^#(#0()) -> c_22()
25: #pred^#(#neg(#s(@x))) -> c_23()
26: #pred^#(#pos(#s(#0()))) -> c_24()
27: #pred^#(#pos(#s(#s(@x)))) -> c_25()
28: #succ^#(#0()) -> c_26()
29: #succ^#(#neg(#s(#0()))) -> c_27()
30: #succ^#(#neg(#s(#s(@x)))) -> c_28()
31: #succ^#(#pos(#s(@x))) -> c_29()
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {2} to the strict component.
- We remove {1} and add Pre({1}) = {6} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) }
Weak DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, dyade#1^#(nil(), @l2) -> c_4()
, mult#1^#(nil(), @n) -> c_7()
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the the dependency graph
->8:{1,2}
|
|->10:{3,4}
| |
| |->12:{5} Weak SCC
| | |
| | |->13:{6} Weak SCC
| | |
| | |->14:{7} Weak SCC
| | |
| | |->15:{8} Weak SCC
| | |
| | |->16:{9} Weak SCC
| | |
| | |->18:{10} Weak SCC
| | | |
| | | |->22:{17} Weak SCC
| | | |
| | | `->23:{18} Weak SCC
| | | |
| | | |->24:{22} Weak SCC
| | | | |
| | | | |->26:{28} Weak SCC
| | | | |
| | | | |->27:{29} Weak SCC
| | | | |
| | | | |->28:{30} Weak SCC
| | | | |
| | | | `->29:{31} Weak SCC
| | | |
| | | `->25:{23} Weak SCC
| | | |
| | | |->26:{28} Weak SCC
| | | |
| | | |->27:{29} Weak SCC
| | | |
| | | |->28:{30} Weak SCC
| | | |
| | | `->29:{31} Weak SCC
| | |
| | |->19:{11} Weak SCC
| | | |
| | | |->22:{17} Weak SCC
| | | |
| | | `->23:{18} Weak SCC
| | | |
| | | |->24:{22} Weak SCC
| | | | |
| | | | |->26:{28} Weak SCC
| | | | |
| | | | |->27:{29} Weak SCC
| | | | |
| | | | |->28:{30} Weak SCC
| | | | |
| | | | `->29:{31} Weak SCC
| | | |
| | | `->25:{23} Weak SCC
| | | |
| | | |->26:{28} Weak SCC
| | | |
| | | |->27:{29} Weak SCC
| | | |
| | | |->28:{30} Weak SCC
| | | |
| | | `->29:{31} Weak SCC
| | |
| | |->17:{12} Weak SCC
| | |
| | |->20:{13} Weak SCC
| | | |
| | | |->22:{17} Weak SCC
| | | |
| | | `->23:{18} Weak SCC
| | | |
| | | |->24:{22} Weak SCC
| | | | |
| | | | |->26:{28} Weak SCC
| | | | |
| | | | |->27:{29} Weak SCC
| | | | |
| | | | |->28:{30} Weak SCC
| | | | |
| | | | `->29:{31} Weak SCC
| | | |
| | | `->25:{23} Weak SCC
| | | |
| | | |->26:{28} Weak SCC
| | | |
| | | |->27:{29} Weak SCC
| | | |
| | | |->28:{30} Weak SCC
| | | |
| | | `->29:{31} Weak SCC
| | |
| | `->21:{14} Weak SCC
| | |
| | |->22:{17} Weak SCC
| | |
| | `->23:{18} Weak SCC
| | |
| | |->24:{22} Weak SCC
| | | |
| | | |->26:{28} Weak SCC
| | | |
| | | |->27:{29} Weak SCC
| | | |
| | | |->28:{30} Weak SCC
| | | |
| | | `->29:{31} Weak SCC
| | |
| | `->25:{23} Weak SCC
| | |
| | |->26:{28} Weak SCC
| | |
| | |->27:{29} Weak SCC
| | |
| | |->28:{30} Weak SCC
| | |
| | `->29:{31} Weak SCC
| |
| `->11:{16} Weak SCC
|
`->9:{15} Weak SCC
->7:{19} Weak SCC
->2:{20} Weak SCC
|
|->3:{24} Weak SCC
|
|->4:{25} Weak SCC
|
|->5:{26} Weak SCC
|
`->6:{27} Weak SCC
->1:{21} Weak SCC
|
|->3:{24} Weak SCC
|
|->4:{25} Weak SCC
|
|->5:{26} Weak SCC
|
`->6:{27} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, 2: dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, 3: mult^#(@n, @l) -> mult#1^#(@l, @n)
, 4: mult#1^#(::(@x, @xs), @n) ->
c_6(*^#(@n, @x), mult^#(@n, @xs)) }
Weak DPs:
{ 5: *^#(@x, @y) -> #mult^#(@x, @y)
, 6: #mult^#(#0(), #0()) -> c_8()
, 7: #mult^#(#0(), #neg(@y)) -> c_9()
, 8: #mult^#(#0(), #pos(@y)) -> c_10()
, 9: #mult^#(#neg(@x), #0()) -> c_11()
, 10: #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, 11: #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, 12: #mult^#(#pos(@x), #0()) -> c_14()
, 13: #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, 14: #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, 15: dyade#1^#(nil(), @l2) -> c_4()
, 16: mult#1^#(nil(), @n) -> c_7()
, 17: #natmult^#(#0(), @y) -> c_30()
, 18: #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, 19: #add^#(#0(), @y) -> c_17()
, 20: #add^#(#neg(#s(#0())), @y) -> #pred^#(@y)
, 21: #add^#(#neg(#s(#s(@x))), @y) ->
#pred^#(#add(#pos(#s(@x)), @y))
, 22: #add^#(#pos(#s(#0())), @y) -> #succ^#(@y)
, 23: #add^#(#pos(#s(#s(@x))), @y) ->
#succ^#(#add(#pos(#s(@x)), @y))
, 24: #pred^#(#0()) -> c_22()
, 25: #pred^#(#neg(#s(@x))) -> c_23()
, 26: #pred^#(#pos(#s(#0()))) -> c_24()
, 27: #pred^#(#pos(#s(#s(@x)))) -> c_25()
, 28: #succ^#(#0()) -> c_26()
, 29: #succ^#(#neg(#s(#0()))) -> c_27()
, 30: #succ^#(#neg(#s(#s(@x)))) -> c_28()
, 31: #succ^#(#pos(#s(@x))) -> c_29() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 21: #add^#(#neg(#s(#s(@x))), @y) ->
#pred^#(#add(#pos(#s(@x)), @y))
, 20: #add^#(#neg(#s(#0())), @y) -> #pred^#(@y)
, 24: #pred^#(#0()) -> c_22()
, 25: #pred^#(#neg(#s(@x))) -> c_23()
, 26: #pred^#(#pos(#s(#0()))) -> c_24()
, 27: #pred^#(#pos(#s(#s(@x)))) -> c_25()
, 19: #add^#(#0(), @y) -> c_17()
, 15: dyade#1^#(nil(), @l2) -> c_4()
, 16: mult#1^#(nil(), @n) -> c_7()
, 5: *^#(@x, @y) -> #mult^#(@x, @y)
, 6: #mult^#(#0(), #0()) -> c_8()
, 7: #mult^#(#0(), #neg(@y)) -> c_9()
, 8: #mult^#(#0(), #pos(@y)) -> c_10()
, 9: #mult^#(#neg(@x), #0()) -> c_11()
, 12: #mult^#(#pos(@x), #0()) -> c_14()
, 10: #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, 11: #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, 13: #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, 14: #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, 17: #natmult^#(#0(), @y) -> c_30()
, 18: #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, 22: #add^#(#pos(#s(#0())), @y) -> #succ^#(@y)
, 23: #add^#(#pos(#s(#s(@x))), @y) ->
#succ^#(#add(#pos(#s(@x)), @y))
, 28: #succ^#(#0()) -> c_26()
, 29: #succ^#(#neg(#s(#0()))) -> c_27()
, 30: #succ^#(#neg(#s(#s(@x)))) -> c_28()
, 31: #succ^#(#pos(#s(@x))) -> c_29() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the following dependency-graph
1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) :2
2: dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :1
3: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) ->
c_6(*^#(@n, @x), mult^#(@n, @xs)) :4
4: mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
-->_2 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2)) :2
2: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :1
3: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) :4
4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs)
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {3} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n) }
Weak DPs: { mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2)) :2
2: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :1
3: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) :4
4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs)
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, mult^#(@n, @l) -> mult#1^#(@l, @n) }
Weak DPs:
{ dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
No rule is usable.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, mult^#(@n, @l) -> mult#1^#(@l, @n) }
Weak DPs:
{ dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
DPs:
{ 2: mult^#(@n, @l) -> mult#1^#(@l, @n)
, 3: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, 4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(::) = {}, Uargs(#s) = {}, Uargs(#neg) = {}, Uargs(#pos) = {},
Uargs(*^#) = {}, Uargs(#mult^#) = {}, Uargs(dyade^#) = {},
Uargs(dyade#1^#) = {}, Uargs(mult^#) = {}, Uargs(mult#1^#) = {},
Uargs(#natmult^#) = {}, Uargs(#add^#) = {}, Uargs(#pred^#) = {},
Uargs(#succ^#) = {}, Uargs(c_1) = {1, 2}
TcT has computed following constructor-restricted polynomial
interpretation.
[::](x1, x2) = 3 + x2
[nil]() = 0
[#0]() = 0
[#s](x1) = 0
[#neg](x1) = 0
[#pos](x1) = 0
[*^#](x1, x2) = 0
[#mult^#](x1, x2) = 0
[dyade^#](x1, x2) = x1 + x1*x2 + x1^2
[dyade#1^#](x1, x2) = x1 + x1*x2 + x1^2
[mult^#](x1, x2) = 1 + x2
[mult#1^#](x1, x2) = x1
[#natmult^#](x1, x2) = 0
[#add^#](x1, x2) = 0
[#pred^#](x1) = 0
[#succ^#](x1) = 0
[c_1](x1, x2) = 2 + 3*x1 + x2
This order satisfies following ordering constraints
[dyade^#(@l1, @l2)] = @l1 + @l1*@l2 + @l1^2
>= @l1 + @l1*@l2 + @l1^2
= [dyade#1^#(@l1, @l2)]
[dyade#1^#(::(@x, @xs), @l2)] = 12 + 7*@xs + 3*@l2 + @xs*@l2 + @xs^2
> 5 + 3*@l2 + @xs + @xs*@l2 + @xs^2
= [c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))]
[mult^#(@n, @l)] = 1 + @l
> @l
= [mult#1^#(@l, @n)]
[mult#1^#(::(@x, @xs), @n)] = 3 + @xs
> 1 + @xs
= [mult^#(@n, @xs)]
Processor 'custom shape polynomial interpretation' induces the
complexity certificate YES(?,O(n^2)) on application of rules
{2,3,4}. Here rules are labeled according to the (estimated)
dependency graph
1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2)) :3
2: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) :4
3: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :2
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :1
4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs)
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :2
- The rules {2,3,4} have known complexity. These cover all
predecessors of {1}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4} is given by YES(?,O(n^2)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1,2} Weak SCC
|
`->2:{3,4} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, 2: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, 3: mult^#(@n, @l) -> mult#1^#(@l, @n)
, 4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, 2: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, 3: mult^#(@n, @l) -> mult#1^#(@l, @n)
, 4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
We apply the transformation 'usablerules' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))
tct-popstar
| Execution Time (secs) | 3.116 |
| Answer | YES(O(1),O(n^2)) |
| Input | dyade.raml |
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:
{ *(@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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add following dependency pairs
Strict DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, dyade#1^#(nil(), @l2) -> c_4()
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
, mult#1^#(nil(), @n) -> c_7() }
Weak DPs:
{ #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
and replace the set of basic marked basic terms accordingly.
We apply the transformation 'usablerules' on the sub-problem:
Strict DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, dyade#1^#(nil(), @l2) -> c_4()
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
, mult#1^#(nil(), @n) -> c_7() }
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 DPs:
{ #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
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) -> #add(#pos(@y), #natmult(@x, @y)) }
StartTerms: basic terms
Strategy: innermost
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
We apply the transformation 'compose (addition)' on the
sub-problem:
Strict DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, dyade#1^#(nil(), @l2) -> c_4()
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
, mult#1^#(nil(), @n) -> c_7() }
Weak DPs:
{ #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
StartTerms: basic terms
Strategy: innermost
We use the processor 'weightgap of dimension 2, maximal degree 1,
cbits 3' to orient following rules strictly.
DPs: { mult#1^#(nil(), @n) -> c_7() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)). These rulesare moved into the corresponding weak
component(s).
Sub-proof:
----------
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(::) = {}, Uargs(#add) = {2}, Uargs(#s) = {},
Uargs(#neg) = {}, Uargs(#pred) = {1}, Uargs(#pos) = {},
Uargs(#succ) = {1}, Uargs(#natmult) = {}, Uargs(*^#) = {},
Uargs(#mult^#) = {}, Uargs(dyade^#) = {}, Uargs(dyade#1^#) = {},
Uargs(c_3) = {1, 2}, Uargs(mult^#) = {}, Uargs(mult#1^#) = {},
Uargs(c_6) = {1, 2}, Uargs(#natmult^#) = {}, Uargs(#add^#) = {2},
Uargs(#pred^#) = {1}, Uargs(#succ^#) = {1}
TcT has computed following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 1
non-zero entries.
[::](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[nil] = [0]
[1]
[#0] = [0]
[0]
[#add](x1, x2) = [1 0] x2 + [0]
[0 2] [0]
[#s](x1) = [0]
[0]
[#neg](x1) = [0]
[0]
[#pred](x1) = [1 0] x1 + [0]
[0 0] [0]
[#pos](x1) = [0]
[0]
[#succ](x1) = [1 0] x1 + [0]
[0 0] [0]
[#natmult](x1, x2) = [0]
[0]
[*^#](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[2 2] [2 2] [0]
[#mult^#](x1, x2) = [2]
[0]
[dyade^#](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[2 2] [1 1] [0]
[dyade#1^#](x1, x2) = [0]
[0]
[c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
[mult^#](x1, x2) = [0 0] x2 + [0]
[1 1] [1]
[c_4] = [0]
[0]
[mult#1^#](x1, x2) = [1]
[0]
[c_6](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [2]
[c_7] = [0]
[0]
[c_8] = [0]
[0]
[c_9] = [0]
[0]
[c_10] = [0]
[0]
[c_11] = [0]
[0]
[#natmult^#](x1, x2) = [2]
[0]
[c_14] = [0]
[0]
[#add^#](x1, x2) = [2 0] x2 + [0]
[0 0] [0]
[c_17] = [0]
[0]
[#pred^#](x1) = [2 0] x1 + [0]
[0 0] [0]
[#succ^#](x1) = [2 0] x1 + [0]
[0 0] [0]
[c_22] = [0]
[0]
[c_23] = [0]
[0]
[c_24] = [0]
[0]
[c_25] = [0]
[0]
[c_26] = [0]
[0]
[c_27] = [0]
[0]
[c_28] = [0]
[0]
[c_29] = [0]
[0]
[c_30] = [0]
[0]
This order satisfies following ordering constraints
[#add(#0(), @y)] = [1 0] @y + [0]
[0 2] [0]
>= [1 0] @y + [0]
[0 1] [0]
= [@y]
[#add(#neg(#s(#0())), @y)] = [1 0] @y + [0]
[0 2] [0]
>= [1 0] @y + [0]
[0 0] [0]
= [#pred(@y)]
[#add(#neg(#s(#s(@x))), @y)] = [1 0] @y + [0]
[0 2] [0]
>= [1 0] @y + [0]
[0 0] [0]
= [#pred(#add(#pos(#s(@x)), @y))]
[#add(#pos(#s(#0())), @y)] = [1 0] @y + [0]
[0 2] [0]
>= [1 0] @y + [0]
[0 0] [0]
= [#succ(@y)]
[#add(#pos(#s(#s(@x))), @y)] = [1 0] @y + [0]
[0 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)))] = [0]
[0]
>= [0]
[0]
= [#neg(#s(#s(@x)))]
[#pred(#pos(#s(#0())))] = [0]
[0]
>= [0]
[0]
= [#0()]
[#pred(#pos(#s(#s(@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))))] = [0]
[0]
>= [0]
[0]
= [#neg(#s(@x))]
[#succ(#pos(#s(@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]
= [#add(#pos(@y), #natmult(@x, @y))]
[*^#(@x, @y)] = [0 0] @x + [0 0] @y + [0]
[2 2] [2 2] [0]
? [2]
[0]
= [#mult^#(@x, @y)]
[#mult^#(#0(), #0())] = [2]
[0]
> [0]
[0]
= [c_8()]
[#mult^#(#0(), #neg(@y))] = [2]
[0]
> [0]
[0]
= [c_9()]
[#mult^#(#0(), #pos(@y))] = [2]
[0]
> [0]
[0]
= [c_10()]
[#mult^#(#neg(@x), #0())] = [2]
[0]
> [0]
[0]
= [c_11()]
[#mult^#(#neg(@x), #neg(@y))] = [2]
[0]
>= [2]
[0]
= [#natmult^#(@x, @y)]
[#mult^#(#neg(@x), #pos(@y))] = [2]
[0]
>= [2]
[0]
= [#natmult^#(@x, @y)]
[#mult^#(#pos(@x), #0())] = [2]
[0]
> [0]
[0]
= [c_14()]
[#mult^#(#pos(@x), #neg(@y))] = [2]
[0]
>= [2]
[0]
= [#natmult^#(@x, @y)]
[#mult^#(#pos(@x), #pos(@y))] = [2]
[0]
>= [2]
[0]
= [#natmult^#(@x, @y)]
[dyade^#(@l1, @l2)] = [0 0] @l1 + [0 0] @l2 + [0]
[2 2] [1 1] [0]
>= [0]
[0]
= [dyade#1^#(@l1, @l2)]
[dyade#1^#(::(@x, @xs), @l2)] = [0]
[0]
? [0 0] @l2 + [0 0] @xs + [0]
[2 2] [2 2] [1]
= [c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))]
[dyade#1^#(nil(), @l2)] = [0]
[0]
>= [0]
[0]
= [c_4()]
[mult^#(@n, @l)] = [0 0] @l + [0]
[1 1] [1]
? [1]
[0]
= [mult#1^#(@l, @n)]
[mult#1^#(::(@x, @xs), @n)] = [1]
[0]
? [0 0] @n + [0 0] @x + [0 0] @xs + [0]
[2 2] [2 2] [1 1] [3]
= [c_6(*^#(@n, @x), mult^#(@n, @xs))]
[mult#1^#(nil(), @n)] = [1]
[0]
> [0]
[0]
= [c_7()]
[#natmult^#(#0(), @y)] = [2]
[0]
> [0]
[0]
= [c_30()]
[#natmult^#(#s(@x), @y)] = [2]
[0]
> [0]
[0]
= [#add^#(#pos(@y), #natmult(@x, @y))]
[#add^#(#0(), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [0]
[0]
= [c_17()]
[#add^#(#neg(#s(#0())), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [2 0] @y + [0]
[0 0] [0]
= [#pred^#(@y)]
[#add^#(#neg(#s(#s(@x))), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [2 0] @y + [0]
[0 0] [0]
= [#pred^#(#add(#pos(#s(@x)), @y))]
[#add^#(#pos(#s(#0())), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [2 0] @y + [0]
[0 0] [0]
= [#succ^#(@y)]
[#add^#(#pos(#s(#s(@x))), @y)] = [2 0] @y + [0]
[0 0] [0]
>= [2 0] @y + [0]
[0 0] [0]
= [#succ^#(#add(#pos(#s(@x)), @y))]
[#pred^#(#0())] = [0]
[0]
>= [0]
[0]
= [c_22()]
[#pred^#(#neg(#s(@x)))] = [0]
[0]
>= [0]
[0]
= [c_23()]
[#pred^#(#pos(#s(#0())))] = [0]
[0]
>= [0]
[0]
= [c_24()]
[#pred^#(#pos(#s(#s(@x))))] = [0]
[0]
>= [0]
[0]
= [c_25()]
[#succ^#(#0())] = [0]
[0]
>= [0]
[0]
= [c_26()]
[#succ^#(#neg(#s(#0())))] = [0]
[0]
>= [0]
[0]
= [c_27()]
[#succ^#(#neg(#s(#s(@x))))] = [0]
[0]
>= [0]
[0]
= [c_28()]
[#succ^#(#pos(#s(@x)))] = [0]
[0]
>= [0]
[0]
= [c_29()]
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 DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, dyade#1^#(nil(), @l2) -> c_4()
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) }
Weak DPs:
{ #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, mult#1^#(nil(), @n) -> c_7()
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: *^#(@x, @y) -> #mult^#(@x, @y)
-->_1 #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y) :15
-->_1 #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y) :14
-->_1 #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y) :12
-->_1 #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y) :11
-->_1 #mult^#(#pos(@x), #0()) -> c_14() :13
-->_1 #mult^#(#neg(@x), #0()) -> c_11() :10
-->_1 #mult^#(#0(), #pos(@y)) -> c_10() :9
-->_1 #mult^#(#0(), #neg(@y)) -> c_9() :8
-->_1 #mult^#(#0(), #0()) -> c_8() :7
2: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) :3
-->_1 dyade#1^#(nil(), @l2) -> c_4() :4
3: dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :5
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :2
4: dyade#1^#(nil(), @l2) -> c_4()
5: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) ->
c_6(*^#(@n, @x), mult^#(@n, @xs)) :6
-->_1 mult#1^#(nil(), @n) -> c_7() :16
6: mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
-->_2 mult^#(@n, @l) -> mult#1^#(@l, @n) :5
-->_1 *^#(@x, @y) -> #mult^#(@x, @y) :1
7: #mult^#(#0(), #0()) -> c_8()
8: #mult^#(#0(), #neg(@y)) -> c_9()
9: #mult^#(#0(), #pos(@y)) -> c_10()
10: #mult^#(#neg(@x), #0()) -> c_11()
11: #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
-->_1 #natmult^#(#s(@x), @y) ->
#add^#(#pos(@y), #natmult(@x, @y)) :18
-->_1 #natmult^#(#0(), @y) -> c_30() :17
12: #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
-->_1 #natmult^#(#s(@x), @y) ->
#add^#(#pos(@y), #natmult(@x, @y)) :18
-->_1 #natmult^#(#0(), @y) -> c_30() :17
13: #mult^#(#pos(@x), #0()) -> c_14()
14: #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
-->_1 #natmult^#(#s(@x), @y) ->
#add^#(#pos(@y), #natmult(@x, @y)) :18
-->_1 #natmult^#(#0(), @y) -> c_30() :17
15: #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
-->_1 #natmult^#(#s(@x), @y) ->
#add^#(#pos(@y), #natmult(@x, @y)) :18
-->_1 #natmult^#(#0(), @y) -> c_30() :17
16: mult#1^#(nil(), @n) -> c_7()
17: #natmult^#(#0(), @y) -> c_30()
18: #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
-->_1 #add^#(#pos(#s(#s(@x))), @y) ->
#succ^#(#add(#pos(#s(@x)), @y)) :23
-->_1 #add^#(#pos(#s(#0())), @y) -> #succ^#(@y) :22
19: #add^#(#0(), @y) -> c_17()
20: #add^#(#neg(#s(#0())), @y) -> #pred^#(@y)
-->_1 #pred^#(#pos(#s(#s(@x)))) -> c_25() :27
-->_1 #pred^#(#pos(#s(#0()))) -> c_24() :26
-->_1 #pred^#(#neg(#s(@x))) -> c_23() :25
-->_1 #pred^#(#0()) -> c_22() :24
21: #add^#(#neg(#s(#s(@x))), @y) -> #pred^#(#add(#pos(#s(@x)), @y))
-->_1 #pred^#(#pos(#s(#s(@x)))) -> c_25() :27
-->_1 #pred^#(#pos(#s(#0()))) -> c_24() :26
-->_1 #pred^#(#neg(#s(@x))) -> c_23() :25
-->_1 #pred^#(#0()) -> c_22() :24
22: #add^#(#pos(#s(#0())), @y) -> #succ^#(@y)
-->_1 #succ^#(#pos(#s(@x))) -> c_29() :31
-->_1 #succ^#(#neg(#s(#s(@x)))) -> c_28() :30
-->_1 #succ^#(#neg(#s(#0()))) -> c_27() :29
-->_1 #succ^#(#0()) -> c_26() :28
23: #add^#(#pos(#s(#s(@x))), @y) -> #succ^#(#add(#pos(#s(@x)), @y))
-->_1 #succ^#(#pos(#s(@x))) -> c_29() :31
-->_1 #succ^#(#neg(#s(#s(@x)))) -> c_28() :30
-->_1 #succ^#(#neg(#s(#0()))) -> c_27() :29
-->_1 #succ^#(#0()) -> c_26() :28
24: #pred^#(#0()) -> c_22()
25: #pred^#(#neg(#s(@x))) -> c_23()
26: #pred^#(#pos(#s(#0()))) -> c_24()
27: #pred^#(#pos(#s(#s(@x)))) -> c_25()
28: #succ^#(#0()) -> c_26()
29: #succ^#(#neg(#s(#0()))) -> c_27()
30: #succ^#(#neg(#s(#s(@x)))) -> c_28()
31: #succ^#(#pos(#s(@x))) -> c_29()
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {2} to the strict component.
- We remove {1} and add Pre({1}) = {6} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) }
Weak DPs:
{ *^#(@x, @y) -> #mult^#(@x, @y)
, #mult^#(#0(), #0()) -> c_8()
, #mult^#(#0(), #neg(@y)) -> c_9()
, #mult^#(#0(), #pos(@y)) -> c_10()
, #mult^#(#neg(@x), #0()) -> c_11()
, #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #0()) -> c_14()
, #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, dyade#1^#(nil(), @l2) -> c_4()
, mult#1^#(nil(), @n) -> c_7()
, #natmult^#(#0(), @y) -> c_30()
, #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, #add^#(#0(), @y) -> c_17()
, #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()) -> c_22()
, #pred^#(#neg(#s(@x))) -> c_23()
, #pred^#(#pos(#s(#0()))) -> c_24()
, #pred^#(#pos(#s(#s(@x)))) -> c_25()
, #succ^#(#0()) -> c_26()
, #succ^#(#neg(#s(#0()))) -> c_27()
, #succ^#(#neg(#s(#s(@x)))) -> c_28()
, #succ^#(#pos(#s(@x))) -> c_29() }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the the dependency graph
->8:{1,2}
|
|->10:{3,4}
| |
| |->12:{5} Weak SCC
| | |
| | |->13:{6} Weak SCC
| | |
| | |->14:{7} Weak SCC
| | |
| | |->15:{8} Weak SCC
| | |
| | |->16:{9} Weak SCC
| | |
| | |->18:{10} Weak SCC
| | | |
| | | |->22:{17} Weak SCC
| | | |
| | | `->23:{18} Weak SCC
| | | |
| | | |->24:{22} Weak SCC
| | | | |
| | | | |->26:{28} Weak SCC
| | | | |
| | | | |->27:{29} Weak SCC
| | | | |
| | | | |->28:{30} Weak SCC
| | | | |
| | | | `->29:{31} Weak SCC
| | | |
| | | `->25:{23} Weak SCC
| | | |
| | | |->26:{28} Weak SCC
| | | |
| | | |->27:{29} Weak SCC
| | | |
| | | |->28:{30} Weak SCC
| | | |
| | | `->29:{31} Weak SCC
| | |
| | |->19:{11} Weak SCC
| | | |
| | | |->22:{17} Weak SCC
| | | |
| | | `->23:{18} Weak SCC
| | | |
| | | |->24:{22} Weak SCC
| | | | |
| | | | |->26:{28} Weak SCC
| | | | |
| | | | |->27:{29} Weak SCC
| | | | |
| | | | |->28:{30} Weak SCC
| | | | |
| | | | `->29:{31} Weak SCC
| | | |
| | | `->25:{23} Weak SCC
| | | |
| | | |->26:{28} Weak SCC
| | | |
| | | |->27:{29} Weak SCC
| | | |
| | | |->28:{30} Weak SCC
| | | |
| | | `->29:{31} Weak SCC
| | |
| | |->17:{12} Weak SCC
| | |
| | |->20:{13} Weak SCC
| | | |
| | | |->22:{17} Weak SCC
| | | |
| | | `->23:{18} Weak SCC
| | | |
| | | |->24:{22} Weak SCC
| | | | |
| | | | |->26:{28} Weak SCC
| | | | |
| | | | |->27:{29} Weak SCC
| | | | |
| | | | |->28:{30} Weak SCC
| | | | |
| | | | `->29:{31} Weak SCC
| | | |
| | | `->25:{23} Weak SCC
| | | |
| | | |->26:{28} Weak SCC
| | | |
| | | |->27:{29} Weak SCC
| | | |
| | | |->28:{30} Weak SCC
| | | |
| | | `->29:{31} Weak SCC
| | |
| | `->21:{14} Weak SCC
| | |
| | |->22:{17} Weak SCC
| | |
| | `->23:{18} Weak SCC
| | |
| | |->24:{22} Weak SCC
| | | |
| | | |->26:{28} Weak SCC
| | | |
| | | |->27:{29} Weak SCC
| | | |
| | | |->28:{30} Weak SCC
| | | |
| | | `->29:{31} Weak SCC
| | |
| | `->25:{23} Weak SCC
| | |
| | |->26:{28} Weak SCC
| | |
| | |->27:{29} Weak SCC
| | |
| | |->28:{30} Weak SCC
| | |
| | `->29:{31} Weak SCC
| |
| `->11:{16} Weak SCC
|
`->9:{15} Weak SCC
->7:{19} Weak SCC
->2:{20} Weak SCC
|
|->3:{24} Weak SCC
|
|->4:{25} Weak SCC
|
|->5:{26} Weak SCC
|
`->6:{27} Weak SCC
->1:{21} Weak SCC
|
|->3:{24} Weak SCC
|
|->4:{25} Weak SCC
|
|->5:{26} Weak SCC
|
`->6:{27} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, 2: dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, 3: mult^#(@n, @l) -> mult#1^#(@l, @n)
, 4: mult#1^#(::(@x, @xs), @n) ->
c_6(*^#(@n, @x), mult^#(@n, @xs)) }
Weak DPs:
{ 5: *^#(@x, @y) -> #mult^#(@x, @y)
, 6: #mult^#(#0(), #0()) -> c_8()
, 7: #mult^#(#0(), #neg(@y)) -> c_9()
, 8: #mult^#(#0(), #pos(@y)) -> c_10()
, 9: #mult^#(#neg(@x), #0()) -> c_11()
, 10: #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, 11: #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, 12: #mult^#(#pos(@x), #0()) -> c_14()
, 13: #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, 14: #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, 15: dyade#1^#(nil(), @l2) -> c_4()
, 16: mult#1^#(nil(), @n) -> c_7()
, 17: #natmult^#(#0(), @y) -> c_30()
, 18: #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, 19: #add^#(#0(), @y) -> c_17()
, 20: #add^#(#neg(#s(#0())), @y) -> #pred^#(@y)
, 21: #add^#(#neg(#s(#s(@x))), @y) ->
#pred^#(#add(#pos(#s(@x)), @y))
, 22: #add^#(#pos(#s(#0())), @y) -> #succ^#(@y)
, 23: #add^#(#pos(#s(#s(@x))), @y) ->
#succ^#(#add(#pos(#s(@x)), @y))
, 24: #pred^#(#0()) -> c_22()
, 25: #pred^#(#neg(#s(@x))) -> c_23()
, 26: #pred^#(#pos(#s(#0()))) -> c_24()
, 27: #pred^#(#pos(#s(#s(@x)))) -> c_25()
, 28: #succ^#(#0()) -> c_26()
, 29: #succ^#(#neg(#s(#0()))) -> c_27()
, 30: #succ^#(#neg(#s(#s(@x)))) -> c_28()
, 31: #succ^#(#pos(#s(@x))) -> c_29() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 21: #add^#(#neg(#s(#s(@x))), @y) ->
#pred^#(#add(#pos(#s(@x)), @y))
, 20: #add^#(#neg(#s(#0())), @y) -> #pred^#(@y)
, 24: #pred^#(#0()) -> c_22()
, 25: #pred^#(#neg(#s(@x))) -> c_23()
, 26: #pred^#(#pos(#s(#0()))) -> c_24()
, 27: #pred^#(#pos(#s(#s(@x)))) -> c_25()
, 19: #add^#(#0(), @y) -> c_17()
, 15: dyade#1^#(nil(), @l2) -> c_4()
, 16: mult#1^#(nil(), @n) -> c_7()
, 5: *^#(@x, @y) -> #mult^#(@x, @y)
, 6: #mult^#(#0(), #0()) -> c_8()
, 7: #mult^#(#0(), #neg(@y)) -> c_9()
, 8: #mult^#(#0(), #pos(@y)) -> c_10()
, 9: #mult^#(#neg(@x), #0()) -> c_11()
, 12: #mult^#(#pos(@x), #0()) -> c_14()
, 10: #mult^#(#neg(@x), #neg(@y)) -> #natmult^#(@x, @y)
, 11: #mult^#(#neg(@x), #pos(@y)) -> #natmult^#(@x, @y)
, 13: #mult^#(#pos(@x), #neg(@y)) -> #natmult^#(@x, @y)
, 14: #mult^#(#pos(@x), #pos(@y)) -> #natmult^#(@x, @y)
, 17: #natmult^#(#0(), @y) -> c_30()
, 18: #natmult^#(#s(@x), @y) -> #add^#(#pos(@y), #natmult(@x, @y))
, 22: #add^#(#pos(#s(#0())), @y) -> #succ^#(@y)
, 23: #add^#(#pos(#s(#s(@x))), @y) ->
#succ^#(#add(#pos(#s(@x)), @y))
, 28: #succ^#(#0()) -> c_26()
, 29: #succ^#(#neg(#s(#0()))) -> c_27()
, 30: #succ^#(#neg(#s(#s(@x)))) -> c_28()
, 31: #succ^#(#pos(#s(@x))) -> c_29() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the following dependency-graph
1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) :2
2: dyade#1^#(::(@x, @xs), @l2) ->
c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :1
3: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) ->
c_6(*^#(@n, @x), mult^#(@n, @xs)) :4
4: mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs))
-->_2 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ mult#1^#(::(@x, @xs), @n) -> c_6(*^#(@n, @x), mult^#(@n, @xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2)) :2
2: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :1
3: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) :4
4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs)
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {4} and add Pre({4}) = {3} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n) }
Weak DPs: { mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2)) :2
2: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :1
3: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) :4
4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs)
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :3
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, mult^#(@n, @l) -> mult#1^#(@l, @n) }
Weak DPs:
{ dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Weak Trs:
{ #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) -> #add(#pos(@y), #natmult(@x, @y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
No rule is usable.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, mult^#(@n, @l) -> mult#1^#(@l, @n) }
Weak DPs:
{ dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'Small Polynomial Path Order (PS,2-bounded)'
to orient following rules strictly.
DPs:
{ 3: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, 4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,2-bounded)' as induced by the safe mapping
safe(::) = {1, 2}, safe(nil) = {}, safe(#0) = {}, safe(#s) = {1},
safe(#neg) = {1}, safe(#pos) = {1}, safe(*^#) = {},
safe(#mult^#) = {}, safe(dyade^#) = {}, safe(dyade#1^#) = {},
safe(mult^#) = {2}, safe(mult#1^#) = {1}, safe(#natmult^#) = {},
safe(#add^#) = {}, safe(#pred^#) = {}, safe(#succ^#) = {},
safe(c_1) = {}
and precedence
dyade#1^# > mult^#, dyade^# ~ dyade#1^#, mult^# ~ mult#1^# .
Following symbols are considered recursive:
{dyade^#, dyade#1^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(::) = [2], pi(nil) = [], pi(#0) = [], pi(#s) = [],
pi(#neg) = [], pi(#pos) = [], pi(*^#) = [], pi(#mult^#) = [],
pi(dyade^#) = [1, 2], pi(dyade#1^#) = [1, 2], pi(mult^#) = 2,
pi(mult#1^#) = 1, pi(#natmult^#) = [], pi(#add^#) = [],
pi(#pred^#) = [], pi(#succ^#) = [], pi(c_1) = [1, 2]
Usable defined function symbols are a subset of:
{}
For your convenience, here are the satisfied ordering constraints:
pi(dyade^#(@l1, @l2)) = dyade^#(@l1, @l2;)
>= dyade#1^#(@l1, @l2;)
= pi(dyade#1^#(@l1, @l2))
pi(dyade#1^#(::(@x, @xs), @l2)) = dyade#1^#(::(; @xs), @l2;)
> c_1(@l2, dyade^#(@xs, @l2;);)
= pi(c_1(mult^#(@x, @l2), dyade^#(@xs, @l2)))
pi(mult^#(@n, @l)) = @l
>= @l
= pi(mult#1^#(@l, @n))
pi(mult#1^#(::(@x, @xs), @n)) = ::(; @xs)
> @xs
= pi(mult^#(@n, @xs))
Processor 'Small Polynomial Path Order (PS,2-bounded)' induces the
complexity certificate YES(?,O(n^2)) on application of rules {3,4}.
Here rules are labeled according to the (estimated) dependency
graph
1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
-->_1 dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2)) :3
2: mult^#(@n, @l) -> mult#1^#(@l, @n)
-->_1 mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) :4
3: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :2
-->_2 dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2) :1
4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs)
-->_1 mult^#(@n, @l) -> mult#1^#(@l, @n) :2
- The rules {3,4} have known complexity. These cover all
predecessors of {1,2}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4} is given by YES(?,O(n^2)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, mult^#(@n, @l) -> mult#1^#(@l, @n)
, mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1,2} Weak SCC
|
`->2:{3,4} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, 2: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, 3: mult^#(@n, @l) -> mult#1^#(@l, @n)
, 4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: dyade^#(@l1, @l2) -> dyade#1^#(@l1, @l2)
, 2: dyade#1^#(::(@x, @xs), @l2) ->
c_1(mult^#(@x, @l2), dyade^#(@xs, @l2))
, 3: mult^#(@n, @l) -> mult#1^#(@l, @n)
, 4: mult#1^#(::(@x, @xs), @n) -> mult^#(@n, @xs) }
We apply the transformation 'usablerules' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))