We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, fst(s(X), cons(Y, Z)) ->
cons(Y, n__fst(activate(X), activate(Z)))
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, add(s(X), Y) -> s(n__add(activate(X), Y))
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Arguments of following rules are not normal-forms:
{ fst(s(X), cons(Y, Z)) ->
cons(Y, n__fst(activate(X), activate(Z)))
, add(s(X), Y) -> s(n__add(activate(X), Y)) }
All above mentioned rules can be savely removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following dependency tuples:
Strict DPs:
{ fst^#(X1, X2) -> c_1()
, fst^#(0(), Z) -> c_2()
, s^#(X) -> c_3()
, activate^#(X) -> c_4()
, activate^#(n__fst(X1, X2)) ->
c_5(fst^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__from(X)) -> c_6(from^#(activate(X)), activate^#(X))
, activate^#(n__s(X)) -> c_7(s^#(X))
, activate^#(n__add(X1, X2)) ->
c_8(add^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__len(X)) -> c_9(len^#(activate(X)), activate^#(X))
, from^#(X) -> c_10()
, from^#(X) -> c_11()
, add^#(X1, X2) -> c_12()
, add^#(0(), X) -> c_13()
, len^#(X) -> c_14()
, len^#(nil()) -> c_15()
, len^#(cons(X, Z)) ->
c_16(s^#(n__len(activate(Z))), activate^#(Z)) }
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:
{ fst^#(X1, X2) -> c_1()
, fst^#(0(), Z) -> c_2()
, s^#(X) -> c_3()
, activate^#(X) -> c_4()
, activate^#(n__fst(X1, X2)) ->
c_5(fst^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__from(X)) -> c_6(from^#(activate(X)), activate^#(X))
, activate^#(n__s(X)) -> c_7(s^#(X))
, activate^#(n__add(X1, X2)) ->
c_8(add^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__len(X)) -> c_9(len^#(activate(X)), activate^#(X))
, from^#(X) -> c_10()
, from^#(X) -> c_11()
, add^#(X1, X2) -> c_12()
, add^#(0(), X) -> c_13()
, len^#(X) -> c_14()
, len^#(nil()) -> c_15()
, len^#(cons(X, Z)) ->
c_16(s^#(n__len(activate(Z))), activate^#(Z)) }
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of
{1,2,3,4,10,11,12,13,14,15} by applications of
Pre({1,2,3,4,10,11,12,13,14,15}) = {5,6,7,8,9,16}. Here rules are
labeled as follows:
DPs:
{ 1: fst^#(X1, X2) -> c_1()
, 2: fst^#(0(), Z) -> c_2()
, 3: s^#(X) -> c_3()
, 4: activate^#(X) -> c_4()
, 5: activate^#(n__fst(X1, X2)) ->
c_5(fst^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, 6: activate^#(n__from(X)) ->
c_6(from^#(activate(X)), activate^#(X))
, 7: activate^#(n__s(X)) -> c_7(s^#(X))
, 8: activate^#(n__add(X1, X2)) ->
c_8(add^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, 9: activate^#(n__len(X)) ->
c_9(len^#(activate(X)), activate^#(X))
, 10: from^#(X) -> c_10()
, 11: from^#(X) -> c_11()
, 12: add^#(X1, X2) -> c_12()
, 13: add^#(0(), X) -> c_13()
, 14: len^#(X) -> c_14()
, 15: len^#(nil()) -> c_15()
, 16: len^#(cons(X, Z)) ->
c_16(s^#(n__len(activate(Z))), activate^#(Z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ activate^#(n__fst(X1, X2)) ->
c_5(fst^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__from(X)) -> c_6(from^#(activate(X)), activate^#(X))
, activate^#(n__s(X)) -> c_7(s^#(X))
, activate^#(n__add(X1, X2)) ->
c_8(add^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__len(X)) -> c_9(len^#(activate(X)), activate^#(X))
, len^#(cons(X, Z)) ->
c_16(s^#(n__len(activate(Z))), activate^#(Z)) }
Weak DPs:
{ fst^#(X1, X2) -> c_1()
, fst^#(0(), Z) -> c_2()
, s^#(X) -> c_3()
, activate^#(X) -> c_4()
, from^#(X) -> c_10()
, from^#(X) -> c_11()
, add^#(X1, X2) -> c_12()
, add^#(0(), X) -> c_13()
, len^#(X) -> c_14()
, len^#(nil()) -> c_15() }
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {3} by applications of
Pre({3}) = {1,2,4,5,6}. Here rules are labeled as follows:
DPs:
{ 1: activate^#(n__fst(X1, X2)) ->
c_5(fst^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, 2: activate^#(n__from(X)) ->
c_6(from^#(activate(X)), activate^#(X))
, 3: activate^#(n__s(X)) -> c_7(s^#(X))
, 4: activate^#(n__add(X1, X2)) ->
c_8(add^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, 5: activate^#(n__len(X)) ->
c_9(len^#(activate(X)), activate^#(X))
, 6: len^#(cons(X, Z)) ->
c_16(s^#(n__len(activate(Z))), activate^#(Z))
, 7: fst^#(X1, X2) -> c_1()
, 8: fst^#(0(), Z) -> c_2()
, 9: s^#(X) -> c_3()
, 10: activate^#(X) -> c_4()
, 11: from^#(X) -> c_10()
, 12: from^#(X) -> c_11()
, 13: add^#(X1, X2) -> c_12()
, 14: add^#(0(), X) -> c_13()
, 15: len^#(X) -> c_14()
, 16: len^#(nil()) -> c_15() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ activate^#(n__fst(X1, X2)) ->
c_5(fst^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__from(X)) -> c_6(from^#(activate(X)), activate^#(X))
, activate^#(n__add(X1, X2)) ->
c_8(add^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__len(X)) -> c_9(len^#(activate(X)), activate^#(X))
, len^#(cons(X, Z)) ->
c_16(s^#(n__len(activate(Z))), activate^#(Z)) }
Weak DPs:
{ fst^#(X1, X2) -> c_1()
, fst^#(0(), Z) -> c_2()
, s^#(X) -> c_3()
, activate^#(X) -> c_4()
, activate^#(n__s(X)) -> c_7(s^#(X))
, from^#(X) -> c_10()
, from^#(X) -> c_11()
, add^#(X1, X2) -> c_12()
, add^#(0(), X) -> c_13()
, len^#(X) -> c_14()
, len^#(nil()) -> c_15() }
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
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.
{ fst^#(X1, X2) -> c_1()
, fst^#(0(), Z) -> c_2()
, s^#(X) -> c_3()
, activate^#(X) -> c_4()
, activate^#(n__s(X)) -> c_7(s^#(X))
, from^#(X) -> c_10()
, from^#(X) -> c_11()
, add^#(X1, X2) -> c_12()
, add^#(0(), X) -> c_13()
, len^#(X) -> c_14()
, len^#(nil()) -> c_15() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ activate^#(n__fst(X1, X2)) ->
c_5(fst^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__from(X)) -> c_6(from^#(activate(X)), activate^#(X))
, activate^#(n__add(X1, X2)) ->
c_8(add^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__len(X)) -> c_9(len^#(activate(X)), activate^#(X))
, len^#(cons(X, Z)) ->
c_16(s^#(n__len(activate(Z))), activate^#(Z)) }
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
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:
{ activate^#(n__fst(X1, X2)) ->
c_5(fst^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__from(X)) -> c_6(from^#(activate(X)), activate^#(X))
, activate^#(n__add(X1, X2)) ->
c_8(add^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, len^#(cons(X, Z)) ->
c_16(s^#(n__len(activate(Z))), activate^#(Z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ activate^#(n__fst(X1, X2)) -> c_1(activate^#(X1), activate^#(X2))
, activate^#(n__from(X)) -> c_2(activate^#(X))
, activate^#(n__add(X1, X2)) -> c_3(activate^#(X1), activate^#(X2))
, activate^#(n__len(X)) -> c_4(len^#(activate(X)), activate^#(X))
, len^#(cons(X, Z)) -> c_5(activate^#(Z)) }
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 3: activate^#(n__add(X1, X2)) ->
c_3(activate^#(X1), activate^#(X2)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[fst](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [0]
[0] = [0]
[0]
[nil] = [0]
[0]
[s](x1) = [0]
[0]
[cons](x1, x2) = [1 0] x1 + [0 1] x2 + [0]
[0 1] [0 0] [0]
[n__fst](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [0]
[activate](x1) = [1 0] x1 + [0]
[0 4] [0]
[from](x1) = [1 0] x1 + [0]
[0 1] [0]
[n__from](x1) = [1 0] x1 + [0]
[0 1] [0]
[n__s](x1) = [0]
[0]
[add](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [4]
[n__add](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [1]
[len](x1) = [0 0] x1 + [0]
[2 1] [0]
[n__len](x1) = [0 0] x1 + [0]
[1 1] [0]
[activate^#](x1) = [0 1] x1 + [0]
[0 1] [0]
[len^#](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_2](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_4](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_5](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[fst(X1, X2)] = [0 0] X1 + [0 0] X2 + [0]
[0 1] [0 1] [0]
>= [0 0] X1 + [0 0] X2 + [0]
[0 1] [0 1] [0]
= [n__fst(X1, X2)]
[fst(0(), Z)] = [0 0] Z + [0]
[0 1] [0]
>= [0]
[0]
= [nil()]
[s(X)] = [0]
[0]
>= [0]
[0]
= [n__s(X)]
[activate(X)] = [1 0] X + [0]
[0 4] [0]
>= [1 0] X + [0]
[0 1] [0]
= [X]
[activate(n__fst(X1, X2))] = [0 0] X1 + [0 0] X2 + [0]
[0 4] [0 4] [0]
>= [0 0] X1 + [0 0] X2 + [0]
[0 4] [0 4] [0]
= [fst(activate(X1), activate(X2))]
[activate(n__from(X))] = [1 0] X + [0]
[0 4] [0]
>= [1 0] X + [0]
[0 4] [0]
= [from(activate(X))]
[activate(n__s(X))] = [0]
[0]
>= [0]
[0]
= [s(X)]
[activate(n__add(X1, X2))] = [1 0] X1 + [1 0] X2 + [0]
[0 4] [0 4] [4]
>= [1 0] X1 + [1 0] X2 + [0]
[0 4] [0 4] [4]
= [add(activate(X1), activate(X2))]
[activate(n__len(X))] = [0 0] X + [0]
[4 4] [0]
>= [0 0] X + [0]
[2 4] [0]
= [len(activate(X))]
[from(X)] = [1 0] X + [0]
[0 1] [0]
>= [1 0] X + [0]
[0 1] [0]
= [cons(X, n__from(n__s(X)))]
[from(X)] = [1 0] X + [0]
[0 1] [0]
>= [1 0] X + [0]
[0 1] [0]
= [n__from(X)]
[add(X1, X2)] = [1 0] X1 + [1 0] X2 + [0]
[0 1] [0 1] [4]
>= [1 0] X1 + [1 0] X2 + [0]
[0 1] [0 1] [1]
= [n__add(X1, X2)]
[add(0(), X)] = [1 0] X + [0]
[0 1] [4]
>= [1 0] X + [0]
[0 1] [0]
= [X]
[len(X)] = [0 0] X + [0]
[2 1] [0]
>= [0 0] X + [0]
[1 1] [0]
= [n__len(X)]
[len(nil())] = [0]
[0]
>= [0]
[0]
= [0()]
[len(cons(X, Z))] = [0 0] Z + [0 0] X + [0]
[0 2] [2 1] [0]
>= [0]
[0]
= [s(n__len(activate(Z)))]
[activate^#(n__fst(X1, X2))] = [0 1] X1 + [0 1] X2 + [0]
[0 1] [0 1] [0]
>= [0 1] X1 + [0 1] X2 + [0]
[0 0] [0 0] [0]
= [c_1(activate^#(X1), activate^#(X2))]
[activate^#(n__from(X))] = [0 1] X + [0]
[0 1] [0]
>= [0 1] X + [0]
[0 0] [0]
= [c_2(activate^#(X))]
[activate^#(n__add(X1, X2))] = [0 1] X1 + [0 1] X2 + [1]
[0 1] [0 1] [1]
> [0 1] X1 + [0 1] X2 + [0]
[0 0] [0 0] [0]
= [c_3(activate^#(X1), activate^#(X2))]
[activate^#(n__len(X))] = [1 1] X + [0]
[1 1] [0]
>= [1 1] X + [0]
[0 0] [0]
= [c_4(len^#(activate(X)), activate^#(X))]
[len^#(cons(X, Z))] = [0 1] Z + [1 0] X + [0]
[0 0] [0 0] [0]
>= [0 1] Z + [0]
[0 0] [0]
= [c_5(activate^#(Z))]
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^1)).
Strict DPs:
{ activate^#(n__fst(X1, X2)) -> c_1(activate^#(X1), activate^#(X2))
, activate^#(n__from(X)) -> c_2(activate^#(X))
, activate^#(n__len(X)) -> c_4(len^#(activate(X)), activate^#(X))
, len^#(cons(X, Z)) -> c_5(activate^#(Z)) }
Weak DPs:
{ activate^#(n__add(X1, X2)) ->
c_3(activate^#(X1), activate^#(X2)) }
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 1: activate^#(n__fst(X1, X2)) ->
c_1(activate^#(X1), activate^#(X2))
, 3: activate^#(n__len(X)) ->
c_4(len^#(activate(X)), activate^#(X))
, 4: len^#(cons(X, Z)) -> c_5(activate^#(Z)) }
Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[fst](x1, x2) = [1 4] x1 + [1 0] x2 + [4]
[0 0] [0 1] [0]
[0] = [0]
[0]
[nil] = [4]
[0]
[s](x1) = [0 0] x1 + [0]
[0 1] [0]
[cons](x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [0]
[n__fst](x1, x2) = [1 1] x1 + [1 0] x2 + [2]
[0 0] [0 1] [0]
[activate](x1) = [4 0] x1 + [0]
[0 1] [0]
[from](x1) = [1 0] x1 + [0]
[0 1] [0]
[n__from](x1) = [1 0] x1 + [0]
[0 1] [0]
[n__s](x1) = [0 0] x1 + [0]
[0 1] [0]
[add](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
[n__add](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
[len](x1) = [1 2] x1 + [5]
[0 0] [0]
[n__len](x1) = [1 1] x1 + [2]
[0 0] [0]
[activate^#](x1) = [6 0] x1 + [0]
[0 2] [1]
[len^#](x1) = [0 6] x1 + [2]
[0 0] [2]
[c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_2](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_4](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_5](x1) = [1 1] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[fst(X1, X2)] = [1 4] X1 + [1 0] X2 + [4]
[0 0] [0 1] [0]
> [1 1] X1 + [1 0] X2 + [2]
[0 0] [0 1] [0]
= [n__fst(X1, X2)]
[fst(0(), Z)] = [1 0] Z + [4]
[0 1] [0]
>= [4]
[0]
= [nil()]
[s(X)] = [0 0] X + [0]
[0 1] [0]
>= [0 0] X + [0]
[0 1] [0]
= [n__s(X)]
[activate(X)] = [4 0] X + [0]
[0 1] [0]
>= [1 0] X + [0]
[0 1] [0]
= [X]
[activate(n__fst(X1, X2))] = [4 4] X1 + [4 0] X2 + [8]
[0 0] [0 1] [0]
> [4 4] X1 + [4 0] X2 + [4]
[0 0] [0 1] [0]
= [fst(activate(X1), activate(X2))]
[activate(n__from(X))] = [4 0] X + [0]
[0 1] [0]
>= [4 0] X + [0]
[0 1] [0]
= [from(activate(X))]
[activate(n__s(X))] = [0 0] X + [0]
[0 1] [0]
>= [0 0] X + [0]
[0 1] [0]
= [s(X)]
[activate(n__add(X1, X2))] = [4 0] X1 + [4 0] X2 + [0]
[0 1] [0 1] [0]
>= [4 0] X1 + [4 0] X2 + [0]
[0 1] [0 1] [0]
= [add(activate(X1), activate(X2))]
[activate(n__len(X))] = [4 4] X + [8]
[0 0] [0]
> [4 2] X + [5]
[0 0] [0]
= [len(activate(X))]
[from(X)] = [1 0] X + [0]
[0 1] [0]
>= [1 0] X + [0]
[0 1] [0]
= [cons(X, n__from(n__s(X)))]
[from(X)] = [1 0] X + [0]
[0 1] [0]
>= [1 0] X + [0]
[0 1] [0]
= [n__from(X)]
[add(X1, X2)] = [1 0] X1 + [1 0] X2 + [0]
[0 1] [0 1] [0]
>= [1 0] X1 + [1 0] X2 + [0]
[0 1] [0 1] [0]
= [n__add(X1, X2)]
[add(0(), X)] = [1 0] X + [0]
[0 1] [0]
>= [1 0] X + [0]
[0 1] [0]
= [X]
[len(X)] = [1 2] X + [5]
[0 0] [0]
> [1 1] X + [2]
[0 0] [0]
= [n__len(X)]
[len(nil())] = [9]
[0]
> [0]
[0]
= [0()]
[len(cons(X, Z))] = [2 2] Z + [1 0] X + [5]
[0 0] [0 0] [0]
> [0]
[0]
= [s(n__len(activate(Z)))]
[activate^#(n__fst(X1, X2))] = [6 6] X1 + [6 0] X2 + [12]
[0 0] [0 2] [1]
> [6 0] X1 + [6 0] X2 + [0]
[0 0] [0 0] [0]
= [c_1(activate^#(X1), activate^#(X2))]
[activate^#(n__from(X))] = [6 0] X + [0]
[0 2] [1]
>= [6 0] X + [0]
[0 0] [0]
= [c_2(activate^#(X))]
[activate^#(n__add(X1, X2))] = [6 0] X1 + [6 0] X2 + [0]
[0 2] [0 2] [1]
>= [6 0] X1 + [6 0] X2 + [0]
[0 0] [0 0] [0]
= [c_3(activate^#(X1), activate^#(X2))]
[activate^#(n__len(X))] = [6 6] X + [12]
[0 0] [1]
> [6 6] X + [4]
[0 0] [0]
= [c_4(len^#(activate(X)), activate^#(X))]
[len^#(cons(X, Z))] = [6 6] Z + [2]
[0 0] [2]
> [6 2] Z + [1]
[0 0] [0]
= [c_5(activate^#(Z))]
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^1)).
Strict DPs: { activate^#(n__from(X)) -> c_2(activate^#(X)) }
Weak DPs:
{ activate^#(n__fst(X1, X2)) -> c_1(activate^#(X1), activate^#(X2))
, activate^#(n__add(X1, X2)) -> c_3(activate^#(X1), activate^#(X2))
, activate^#(n__len(X)) -> c_4(len^#(activate(X)), activate^#(X))
, len^#(cons(X, Z)) -> c_5(activate^#(Z)) }
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 1: activate^#(n__from(X)) -> c_2(activate^#(X))
, 2: activate^#(n__fst(X1, X2)) ->
c_1(activate^#(X1), activate^#(X2))
, 5: len^#(cons(X, Z)) -> c_5(activate^#(Z)) }
Trs:
{ activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__len(X)) -> len(activate(X))
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[fst](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [4]
[0] = [0]
[0]
[nil] = [0]
[0]
[s](x1) = [0]
[0]
[cons](x1, x2) = [0 1] x2 + [4]
[0 0] [3]
[n__fst](x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [4]
[activate](x1) = [1 0] x1 + [1]
[0 3] [3]
[from](x1) = [0 0] x1 + [6]
[0 1] [3]
[n__from](x1) = [0 0] x1 + [6]
[0 1] [2]
[n__s](x1) = [0]
[0]
[add](x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[2 1] [0 1] [3]
[n__add](x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 1] [0 1] [3]
[len](x1) = [0 0] x1 + [3]
[1 1] [1]
[n__len](x1) = [0 0] x1 + [3]
[1 1] [1]
[activate^#](x1) = [0 2] x1 + [6]
[1 1] [1]
[len^#](x1) = [2 0] x1 + [0]
[0 1] [0]
[c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_2](x1) = [1 0] x1 + [1]
[0 0] [0]
[c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_4](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
[c_5](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[fst(X1, X2)] = [0 0] X1 + [0 0] X2 + [0]
[0 1] [0 1] [4]
>= [0 0] X1 + [0 0] X2 + [0]
[0 1] [0 1] [4]
= [n__fst(X1, X2)]
[fst(0(), Z)] = [0 0] Z + [0]
[0 1] [4]
>= [0]
[0]
= [nil()]
[s(X)] = [0]
[0]
>= [0]
[0]
= [n__s(X)]
[activate(X)] = [1 0] X + [1]
[0 3] [3]
> [1 0] X + [0]
[0 1] [0]
= [X]
[activate(n__fst(X1, X2))] = [0 0] X1 + [0 0] X2 + [1]
[0 3] [0 3] [15]
> [0 0] X1 + [0 0] X2 + [0]
[0 3] [0 3] [10]
= [fst(activate(X1), activate(X2))]
[activate(n__from(X))] = [0 0] X + [7]
[0 3] [9]
> [0 0] X + [6]
[0 3] [6]
= [from(activate(X))]
[activate(n__s(X))] = [1]
[3]
> [0]
[0]
= [s(X)]
[activate(n__add(X1, X2))] = [0 0] X1 + [1 0] X2 + [1]
[3 3] [0 3] [12]
>= [0 0] X1 + [1 0] X2 + [1]
[2 3] [0 3] [11]
= [add(activate(X1), activate(X2))]
[activate(n__len(X))] = [0 0] X + [4]
[3 3] [6]
> [0 0] X + [3]
[1 3] [5]
= [len(activate(X))]
[from(X)] = [0 0] X + [6]
[0 1] [3]
>= [6]
[3]
= [cons(X, n__from(n__s(X)))]
[from(X)] = [0 0] X + [6]
[0 1] [3]
>= [0 0] X + [6]
[0 1] [2]
= [n__from(X)]
[add(X1, X2)] = [0 0] X1 + [1 0] X2 + [0]
[2 1] [0 1] [3]
>= [0 0] X1 + [1 0] X2 + [0]
[1 1] [0 1] [3]
= [n__add(X1, X2)]
[add(0(), X)] = [1 0] X + [0]
[0 1] [3]
>= [1 0] X + [0]
[0 1] [0]
= [X]
[len(X)] = [0 0] X + [3]
[1 1] [1]
>= [0 0] X + [3]
[1 1] [1]
= [n__len(X)]
[len(nil())] = [3]
[1]
> [0]
[0]
= [0()]
[len(cons(X, Z))] = [0 0] Z + [3]
[0 1] [8]
> [0]
[0]
= [s(n__len(activate(Z)))]
[activate^#(n__fst(X1, X2))] = [0 2] X1 + [0 2] X2 + [14]
[0 1] [0 1] [5]
> [0 2] X1 + [0 2] X2 + [12]
[0 0] [0 0] [0]
= [c_1(activate^#(X1), activate^#(X2))]
[activate^#(n__from(X))] = [0 2] X + [10]
[0 1] [9]
> [0 2] X + [7]
[0 0] [0]
= [c_2(activate^#(X))]
[activate^#(n__add(X1, X2))] = [2 2] X1 + [0 2] X2 + [12]
[1 1] [1 1] [4]
>= [0 2] X1 + [0 2] X2 + [12]
[0 0] [0 0] [0]
= [c_3(activate^#(X1), activate^#(X2))]
[activate^#(n__len(X))] = [2 2] X + [8]
[1 1] [5]
>= [2 2] X + [8]
[0 0] [0]
= [c_4(len^#(activate(X)), activate^#(X))]
[len^#(cons(X, Z))] = [0 2] Z + [8]
[0 0] [3]
> [0 2] Z + [6]
[0 0] [0]
= [c_5(activate^#(Z))]
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:
{ activate^#(n__fst(X1, X2)) -> c_1(activate^#(X1), activate^#(X2))
, activate^#(n__from(X)) -> c_2(activate^#(X))
, activate^#(n__add(X1, X2)) -> c_3(activate^#(X1), activate^#(X2))
, activate^#(n__len(X)) -> c_4(len^#(activate(X)), activate^#(X))
, len^#(cons(X, Z)) -> c_5(activate^#(Z)) }
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
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.
{ activate^#(n__fst(X1, X2)) -> c_1(activate^#(X1), activate^#(X2))
, activate^#(n__from(X)) -> c_2(activate^#(X))
, activate^#(n__add(X1, X2)) -> c_3(activate^#(X1), activate^#(X2))
, activate^#(n__len(X)) -> c_4(len^#(activate(X)), activate^#(X))
, len^#(cons(X, Z)) -> c_5(activate^#(Z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ fst(X1, X2) -> n__fst(X1, X2)
, fst(0(), Z) -> nil()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2))
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(X)
, activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
, activate(n__len(X)) -> len(activate(X))
, from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, add(0(), X) -> X
, len(X) -> n__len(X)
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z))) }
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^1))