We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ map(Cons(x, xs)) -> Cons(f(x), map(xs))
, map(Nil()) -> Nil()
, f(x) -> *(x, x)
, +Full(S(x), y) -> +Full(x, S(y))
, +Full(0(), y) -> y
, goal(xs) -> map(xs) }
Weak Trs:
{ *(x, S(S(y))) -> +(x, *(x, S(y)))
, *(x, S(0())) -> x
, *(x, 0()) -> 0()
, *(0(), y) -> 0() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(f^#(x), map^#(xs))
, map^#(Nil()) -> c_2()
, f^#(x) -> c_3(*^#(x, x))
, +Full^#(S(x), y) -> c_4(+Full^#(x, S(y)))
, +Full^#(0(), y) -> c_5()
, goal^#(xs) -> c_6(map^#(xs)) }
Weak DPs:
{ *^#(x, S(S(y))) -> c_7(*^#(x, S(y)))
, *^#(x, S(0())) -> c_8()
, *^#(x, 0()) -> c_9()
, *^#(0(), y) -> c_10() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(f^#(x), map^#(xs))
, map^#(Nil()) -> c_2()
, f^#(x) -> c_3(*^#(x, x))
, +Full^#(S(x), y) -> c_4(+Full^#(x, S(y)))
, +Full^#(0(), y) -> c_5()
, goal^#(xs) -> c_6(map^#(xs)) }
Strict Trs:
{ map(Cons(x, xs)) -> Cons(f(x), map(xs))
, map(Nil()) -> Nil()
, f(x) -> *(x, x)
, +Full(S(x), y) -> +Full(x, S(y))
, +Full(0(), y) -> y
, goal(xs) -> map(xs) }
Weak DPs:
{ *^#(x, S(S(y))) -> c_7(*^#(x, S(y)))
, *^#(x, S(0())) -> c_8()
, *^#(x, 0()) -> c_9()
, *^#(0(), y) -> c_10() }
Weak Trs:
{ *(x, S(S(y))) -> +(x, *(x, S(y)))
, *(x, S(0())) -> x
, *(x, 0()) -> 0()
, *(0(), y) -> 0() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^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(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(f^#(x), map^#(xs))
, map^#(Nil()) -> c_2()
, f^#(x) -> c_3(*^#(x, x))
, +Full^#(S(x), y) -> c_4(+Full^#(x, S(y)))
, +Full^#(0(), y) -> c_5()
, goal^#(xs) -> c_6(map^#(xs)) }
Weak DPs:
{ *^#(x, S(S(y))) -> c_7(*^#(x, S(y)))
, *^#(x, S(0())) -> c_8()
, *^#(x, 0()) -> c_9()
, *^#(0(), y) -> c_10() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(c_1) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_4) = {1},
Uargs(c_6) = {1}, Uargs(c_7) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[S](x1) = [0]
[0]
[Cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
[Nil] = [0]
[0]
[0] = [0]
[0]
[map^#](x1) = [2 2] x1 + [0]
[0 0] [0]
[c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 1] [0 1] [2]
[f^#](x1) = [0]
[0]
[c_2] = [0]
[0]
[c_3](x1) = [1 0] x1 + [0]
[0 1] [0]
[*^#](x1, x2) = [0]
[0]
[+Full^#](x1, x2) = [0]
[0]
[c_4](x1) = [1 0] x1 + [2]
[0 1] [2]
[c_5] = [0]
[0]
[goal^#](x1) = [2 2] x1 + [2]
[2 1] [2]
[c_6](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_7](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_8] = [0]
[0]
[c_9] = [0]
[0]
[c_10] = [0]
[0]
The order satisfies the following ordering constraints:
[map^#(Cons(x, xs))] = [2 2] x + [2 2] xs + [0]
[0 0] [0 0] [0]
? [2 2] xs + [2]
[0 0] [2]
= [c_1(f^#(x), map^#(xs))]
[map^#(Nil())] = [0]
[0]
>= [0]
[0]
= [c_2()]
[f^#(x)] = [0]
[0]
>= [0]
[0]
= [c_3(*^#(x, x))]
[*^#(x, S(S(y)))] = [0]
[0]
>= [0]
[0]
= [c_7(*^#(x, S(y)))]
[*^#(x, S(0()))] = [0]
[0]
>= [0]
[0]
= [c_8()]
[*^#(x, 0())] = [0]
[0]
>= [0]
[0]
= [c_9()]
[*^#(0(), y)] = [0]
[0]
>= [0]
[0]
= [c_10()]
[+Full^#(S(x), y)] = [0]
[0]
? [2]
[2]
= [c_4(+Full^#(x, S(y)))]
[+Full^#(0(), y)] = [0]
[0]
>= [0]
[0]
= [c_5()]
[goal^#(xs)] = [2 2] xs + [2]
[2 1] [2]
> [2 2] xs + [0]
[0 0] [0]
= [c_6(map^#(xs))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(f^#(x), map^#(xs))
, map^#(Nil()) -> c_2()
, f^#(x) -> c_3(*^#(x, x))
, +Full^#(S(x), y) -> c_4(+Full^#(x, S(y)))
, +Full^#(0(), y) -> c_5() }
Weak DPs:
{ *^#(x, S(S(y))) -> c_7(*^#(x, S(y)))
, *^#(x, S(0())) -> c_8()
, *^#(x, 0()) -> c_9()
, *^#(0(), y) -> c_10()
, goal^#(xs) -> c_6(map^#(xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {3,5} by applications of
Pre({3,5}) = {1,4}. Here rules are labeled as follows:
DPs:
{ 1: map^#(Cons(x, xs)) -> c_1(f^#(x), map^#(xs))
, 2: map^#(Nil()) -> c_2()
, 3: f^#(x) -> c_3(*^#(x, x))
, 4: +Full^#(S(x), y) -> c_4(+Full^#(x, S(y)))
, 5: +Full^#(0(), y) -> c_5()
, 6: *^#(x, S(S(y))) -> c_7(*^#(x, S(y)))
, 7: *^#(x, S(0())) -> c_8()
, 8: *^#(x, 0()) -> c_9()
, 9: *^#(0(), y) -> c_10()
, 10: goal^#(xs) -> c_6(map^#(xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(f^#(x), map^#(xs))
, map^#(Nil()) -> c_2()
, +Full^#(S(x), y) -> c_4(+Full^#(x, S(y))) }
Weak DPs:
{ f^#(x) -> c_3(*^#(x, x))
, *^#(x, S(S(y))) -> c_7(*^#(x, S(y)))
, *^#(x, S(0())) -> c_8()
, *^#(x, 0()) -> c_9()
, *^#(0(), y) -> c_10()
, +Full^#(0(), y) -> c_5()
, goal^#(xs) -> c_6(map^#(xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ f^#(x) -> c_3(*^#(x, x))
, *^#(x, S(S(y))) -> c_7(*^#(x, S(y)))
, *^#(x, S(0())) -> c_8()
, *^#(x, 0()) -> c_9()
, *^#(0(), y) -> c_10()
, +Full^#(0(), y) -> c_5() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(f^#(x), map^#(xs))
, map^#(Nil()) -> c_2()
, +Full^#(S(x), y) -> c_4(+Full^#(x, S(y))) }
Weak DPs: { goal^#(xs) -> c_6(map^#(xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ map^#(Cons(x, xs)) -> c_1(f^#(x), map^#(xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(map^#(xs))
, map^#(Nil()) -> c_2()
, +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) }
Weak DPs: { goal^#(xs) -> c_4(map^#(xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Consider the dependency graph
1: map^#(Cons(x, xs)) -> c_1(map^#(xs))
-->_1 map^#(Nil()) -> c_2() :2
-->_1 map^#(Cons(x, xs)) -> c_1(map^#(xs)) :1
2: map^#(Nil()) -> c_2()
3: +Full^#(S(x), y) -> c_3(+Full^#(x, S(y)))
-->_1 +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) :3
4: goal^#(xs) -> c_4(map^#(xs))
-->_1 map^#(Nil()) -> c_2() :2
-->_1 map^#(Cons(x, xs)) -> c_1(map^#(xs)) :1
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).
{ goal^#(xs) -> c_4(map^#(xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(map^#(xs))
, map^#(Nil()) -> c_2()
, +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {2} by applications of
Pre({2}) = {1}. Here rules are labeled as follows:
DPs:
{ 1: map^#(Cons(x, xs)) -> c_1(map^#(xs))
, 2: map^#(Nil()) -> c_2()
, 3: +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(map^#(xs))
, +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) }
Weak DPs: { map^#(Nil()) -> c_2() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ map^#(Nil()) -> c_2() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ map^#(Cons(x, xs)) -> c_1(map^#(xs))
, +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) }
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: map^#(Cons(x, xs)) -> c_1(map^#(xs))
, 2: +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(S) = {1}, safe(Cons) = {1, 2}, safe(map^#) = {},
safe(+Full^#) = {2}, safe(c_1) = {}, safe(c_3) = {}
and precedence
empty .
Following symbols are considered recursive:
{map^#, +Full^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(S) = [1], pi(Cons) = [2], pi(map^#) = [1], pi(+Full^#) = [1],
pi(c_1) = [1], pi(c_3) = [1]
Usable defined function symbols are a subset of:
{map^#, +Full^#}
For your convenience, here are the satisfied ordering constraints:
pi(map^#(Cons(x, xs))) = map^#(Cons(; xs);)
> c_1(map^#(xs;);)
= pi(c_1(map^#(xs)))
pi(+Full^#(S(x), y)) = +Full^#(S(; x);)
> c_3(+Full^#(x;);)
= pi(c_3(+Full^#(x, S(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:
{ map^#(Cons(x, xs)) -> c_1(map^#(xs))
, +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) }
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.
{ map^#(Cons(x, xs)) -> c_1(map^#(xs))
, +Full^#(S(x), y) -> c_3(+Full^#(x, S(y))) }
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^1))