We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ terms(N) -> cons(recip(sqr(N)))
, sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X)))
, first(0(), X) -> nil()
, first(s(X), cons(Y)) -> cons(Y)
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(X))) -> s(half(X))
, half(dbl(X)) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We add the following dependency tuples:
Strict DPs:
{ terms^#(N) -> c_1(sqr^#(N))
, sqr^#(0()) -> c_2()
, sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, add^#(0(), X) -> c_4()
, add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(0()) -> c_6()
, dbl^#(s(X)) -> c_7(dbl^#(X))
, first^#(0(), X) -> c_8()
, first^#(s(X), cons(Y)) -> c_9()
, half^#(0()) -> c_10()
, half^#(s(0())) -> c_11()
, half^#(s(s(X))) -> c_12(half^#(X))
, half^#(dbl(X)) -> c_13() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ terms^#(N) -> c_1(sqr^#(N))
, sqr^#(0()) -> c_2()
, sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, add^#(0(), X) -> c_4()
, add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(0()) -> c_6()
, dbl^#(s(X)) -> c_7(dbl^#(X))
, first^#(0(), X) -> c_8()
, first^#(s(X), cons(Y)) -> c_9()
, half^#(0()) -> c_10()
, half^#(s(0())) -> c_11()
, half^#(s(s(X))) -> c_12(half^#(X))
, half^#(dbl(X)) -> c_13() }
Weak Trs:
{ terms(N) -> cons(recip(sqr(N)))
, sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X)))
, first(0(), X) -> nil()
, first(s(X), cons(Y)) -> cons(Y)
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(X))) -> s(half(X))
, half(dbl(X)) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We estimate the number of application of {2,4,6,8,9,10,11,13} by
applications of Pre({2,4,6,8,9,10,11,13}) = {1,3,5,7,12}. Here
rules are labeled as follows:
DPs:
{ 1: terms^#(N) -> c_1(sqr^#(N))
, 2: sqr^#(0()) -> c_2()
, 3: sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, 4: add^#(0(), X) -> c_4()
, 5: add^#(s(X), Y) -> c_5(add^#(X, Y))
, 6: dbl^#(0()) -> c_6()
, 7: dbl^#(s(X)) -> c_7(dbl^#(X))
, 8: first^#(0(), X) -> c_8()
, 9: first^#(s(X), cons(Y)) -> c_9()
, 10: half^#(0()) -> c_10()
, 11: half^#(s(0())) -> c_11()
, 12: half^#(s(s(X))) -> c_12(half^#(X))
, 13: half^#(dbl(X)) -> c_13() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ terms^#(N) -> c_1(sqr^#(N))
, sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(s(X)) -> c_7(dbl^#(X))
, half^#(s(s(X))) -> c_12(half^#(X)) }
Weak DPs:
{ sqr^#(0()) -> c_2()
, add^#(0(), X) -> c_4()
, dbl^#(0()) -> c_6()
, first^#(0(), X) -> c_8()
, first^#(s(X), cons(Y)) -> c_9()
, half^#(0()) -> c_10()
, half^#(s(0())) -> c_11()
, half^#(dbl(X)) -> c_13() }
Weak Trs:
{ terms(N) -> cons(recip(sqr(N)))
, sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X)))
, first(0(), X) -> nil()
, first(s(X), cons(Y)) -> cons(Y)
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(X))) -> s(half(X))
, half(dbl(X)) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ sqr^#(0()) -> c_2()
, add^#(0(), X) -> c_4()
, dbl^#(0()) -> c_6()
, first^#(0(), X) -> c_8()
, first^#(s(X), cons(Y)) -> c_9()
, half^#(0()) -> c_10()
, half^#(s(0())) -> c_11()
, half^#(dbl(X)) -> c_13() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ terms^#(N) -> c_1(sqr^#(N))
, sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(s(X)) -> c_7(dbl^#(X))
, half^#(s(s(X))) -> c_12(half^#(X)) }
Weak Trs:
{ terms(N) -> cons(recip(sqr(N)))
, sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X)))
, first(0(), X) -> nil()
, first(s(X), cons(Y)) -> cons(Y)
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(X))) -> s(half(X))
, half(dbl(X)) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
Consider the dependency graph
1: terms^#(N) -> c_1(sqr^#(N))
-->_1 sqr^#(s(X)) ->
c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) :2
2: sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
-->_3 dbl^#(s(X)) -> c_7(dbl^#(X)) :4
-->_1 add^#(s(X), Y) -> c_5(add^#(X, Y)) :3
-->_2 sqr^#(s(X)) ->
c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) :2
3: add^#(s(X), Y) -> c_5(add^#(X, Y))
-->_1 add^#(s(X), Y) -> c_5(add^#(X, Y)) :3
4: dbl^#(s(X)) -> c_7(dbl^#(X))
-->_1 dbl^#(s(X)) -> c_7(dbl^#(X)) :4
5: half^#(s(s(X))) -> c_12(half^#(X))
-->_1 half^#(s(s(X))) -> c_12(half^#(X)) :5
Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).
{ terms^#(N) -> c_1(sqr^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(s(X)) -> c_7(dbl^#(X))
, half^#(s(s(X))) -> c_12(half^#(X)) }
Weak Trs:
{ terms(N) -> cons(recip(sqr(N)))
, sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X)))
, first(0(), X) -> nil()
, first(s(X), cons(Y)) -> cons(Y)
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(X))) -> s(half(X))
, half(dbl(X)) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(s(X)) -> c_7(dbl^#(X))
, half^#(s(s(X))) -> c_12(half^#(X)) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, 4: half^#(s(s(X))) -> c_12(half^#(X)) }
Trs:
{ sqr(0()) -> 0()
, dbl(0()) -> 0() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_3) = {1, 2, 3}, Uargs(c_5) = {1}, Uargs(c_7) = {1},
Uargs(c_12) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[sqr](x1) = [1] x1 + [6]
[0] = [0]
[s](x1) = [1] x1 + [7]
[add](x1, x2) = [7]
[dbl](x1) = [1]
[sqr^#](x1) = [1] x1 + [4]
[c_3](x1, x2, x3) = [3] x1 + [1] x2 + [1] x3 + [0]
[add^#](x1, x2) = [2]
[dbl^#](x1) = [0]
[c_5](x1) = [1] x1 + [0]
[c_7](x1) = [2] x1 + [0]
[half^#](x1) = [1] x1 + [1]
[c_12](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[sqr(0())] = [6]
> [0]
= [0()]
[sqr(s(X))] = [1] X + [13]
? [14]
= [s(add(sqr(X), dbl(X)))]
[add(0(), X)] = [7]
? [1] X + [0]
= [X]
[add(s(X), Y)] = [7]
? [14]
= [s(add(X, Y))]
[dbl(0())] = [1]
> [0]
= [0()]
[dbl(s(X))] = [1]
? [15]
= [s(s(dbl(X)))]
[sqr^#(s(X))] = [1] X + [11]
> [1] X + [10]
= [c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))]
[add^#(s(X), Y)] = [2]
>= [2]
= [c_5(add^#(X, Y))]
[dbl^#(s(X))] = [0]
>= [0]
= [c_7(dbl^#(X))]
[half^#(s(s(X)))] = [1] X + [15]
> [1] X + [1]
= [c_12(half^#(X))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(s(X)) -> c_7(dbl^#(X)) }
Weak DPs:
{ sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X))
, half^#(s(s(X))) -> c_12(half^#(X)) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ half^#(s(s(X))) -> c_12(half^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(s(X)) -> c_7(dbl^#(X)) }
Weak DPs:
{ sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We decompose the input problem according to the dependency graph
into the upper component
{ sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) }
and lower component
{ add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(s(X)) -> c_7(dbl^#(X)) }
Further, following extension rules are added to the lower
component.
{ sqr^#(s(X)) -> sqr^#(X)
, sqr^#(s(X)) -> add^#(sqr(X), dbl(X))
, sqr^#(s(X)) -> dbl^#(X) }
TcT solves the upper component with certificate YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.
DPs:
{ 1: sqr^#(s(X)) ->
c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(sqr) = {}, safe(0) = {}, safe(s) = {1}, safe(add) = {1, 2},
safe(dbl) = {}, safe(sqr^#) = {}, safe(c_3) = {}, safe(add^#) = {},
safe(dbl^#) = {}
and precedence
empty .
Following symbols are considered recursive:
{sqr^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(sqr) = [], pi(0) = [], pi(s) = [1], pi(add) = [1, 2],
pi(dbl) = 1, pi(sqr^#) = [1], pi(c_3) = [1, 2, 3], pi(add^#) = [],
pi(dbl^#) = []
Usable defined function symbols are a subset of:
{sqr^#, add^#, dbl^#}
For your convenience, here are the satisfied ordering constraints:
pi(sqr^#(s(X))) = sqr^#(s(; X);)
> c_3(add^#(), sqr^#(X;), dbl^#();)
= pi(c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)))
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ sqr^#(s(X)) -> c_3(add^#(sqr(X), dbl(X)), sqr^#(X), dbl^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
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
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:
{ add^#(s(X), Y) -> c_5(add^#(X, Y))
, dbl^#(s(X)) -> c_7(dbl^#(X)) }
Weak DPs:
{ sqr^#(s(X)) -> sqr^#(X)
, sqr^#(s(X)) -> add^#(sqr(X), dbl(X))
, sqr^#(s(X)) -> dbl^#(X) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 2: dbl^#(s(X)) -> c_7(dbl^#(X))
, 3: sqr^#(s(X)) -> sqr^#(X)
, 4: sqr^#(s(X)) -> add^#(sqr(X), dbl(X))
, 5: sqr^#(s(X)) -> dbl^#(X) }
Trs: { dbl(0()) -> 0() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_5) = {1}, Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[sqr](x1) = [0]
[0] = [0]
[s](x1) = [1] x1 + [4]
[add](x1, x2) = [4] x2 + [0]
[dbl](x1) = [1]
[sqr^#](x1) = [2] x1 + [0]
[add^#](x1, x2) = [1]
[dbl^#](x1) = [1] x1 + [6]
[c_5](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[sqr(0())] = [0]
>= [0]
= [0()]
[sqr(s(X))] = [0]
? [8]
= [s(add(sqr(X), dbl(X)))]
[add(0(), X)] = [4] X + [0]
>= [1] X + [0]
= [X]
[add(s(X), Y)] = [4] Y + [0]
? [4] Y + [4]
= [s(add(X, Y))]
[dbl(0())] = [1]
> [0]
= [0()]
[dbl(s(X))] = [1]
? [9]
= [s(s(dbl(X)))]
[sqr^#(s(X))] = [2] X + [8]
> [2] X + [0]
= [sqr^#(X)]
[sqr^#(s(X))] = [2] X + [8]
> [1]
= [add^#(sqr(X), dbl(X))]
[sqr^#(s(X))] = [2] X + [8]
> [1] X + [6]
= [dbl^#(X)]
[add^#(s(X), Y)] = [1]
>= [1]
= [c_5(add^#(X, Y))]
[dbl^#(s(X))] = [1] X + [10]
> [1] X + [6]
= [c_7(dbl^#(X))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs: { add^#(s(X), Y) -> c_5(add^#(X, Y)) }
Weak DPs:
{ sqr^#(s(X)) -> sqr^#(X)
, sqr^#(s(X)) -> add^#(sqr(X), dbl(X))
, sqr^#(s(X)) -> dbl^#(X)
, dbl^#(s(X)) -> c_7(dbl^#(X)) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ sqr^#(s(X)) -> dbl^#(X)
, dbl^#(s(X)) -> c_7(dbl^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs: { add^#(s(X), Y) -> c_5(add^#(X, Y)) }
Weak DPs:
{ sqr^#(s(X)) -> sqr^#(X)
, sqr^#(s(X)) -> add^#(sqr(X), dbl(X)) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
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:
{ 1: add^#(s(X), Y) -> c_5(add^#(X, Y))
, 2: sqr^#(s(X)) -> sqr^#(X)
, 3: sqr^#(s(X)) -> add^#(sqr(X), dbl(X)) }
Trs:
{ sqr(0()) -> 0()
, dbl(0()) -> 0() }
Sub-proof:
----------
The following argument positions are considered usable:
Uargs(c_5) = {1}
TcT has computed the following constructor-restricted polynomial
interpretation.
[sqr](x1) = 1 + x1^2
[0]() = 0
[s](x1) = 2 + x1
[add](x1, x2) = x1 + x2
[dbl](x1) = 2 + 2*x1
[sqr^#](x1) = 3 + x1^2
[add^#](x1, x2) = 2 + x1
[dbl^#](x1) = 0
[c_5](x1) = x1
[c_7](x1) = 0
This order satisfies the following ordering constraints.
[sqr(0())] = 1
>
= [0()]
[sqr(s(X))] = 5 + 4*X + X^2
>= 5 + X^2 + 2*X
= [s(add(sqr(X), dbl(X)))]
[add(0(), X)] = X
>= X
= [X]
[add(s(X), Y)] = 2 + X + Y
>= 2 + X + Y
= [s(add(X, Y))]
[dbl(0())] = 2
>
= [0()]
[dbl(s(X))] = 6 + 2*X
>= 6 + 2*X
= [s(s(dbl(X)))]
[sqr^#(s(X))] = 7 + 4*X + X^2
> 3 + X^2
= [sqr^#(X)]
[sqr^#(s(X))] = 7 + 4*X + X^2
> 3 + X^2
= [add^#(sqr(X), dbl(X))]
[add^#(s(X), Y)] = 4 + X
> 2 + X
= [c_5(add^#(X, Y))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ sqr^#(s(X)) -> sqr^#(X)
, sqr^#(s(X)) -> add^#(sqr(X), dbl(X))
, add^#(s(X), Y) -> c_5(add^#(X, Y)) }
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ sqr^#(s(X)) -> sqr^#(X)
, sqr^#(s(X)) -> add^#(sqr(X), dbl(X))
, add^#(s(X), Y) -> c_5(add^#(X, Y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ sqr(0()) -> 0()
, sqr(s(X)) -> s(add(sqr(X), dbl(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, dbl(0()) -> 0()
, dbl(s(X)) -> s(s(dbl(X))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
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^3))