interpretations
YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,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)))
, activate(X) -> X
, activate(n__fst(X1, X2)) -> fst(X1, X2)
, activate(n__from(X)) -> from(X)
, activate(n__add(X1, X2)) -> add(X1, X2)
, activate(n__len(X)) -> len(X)
, from(X) -> cons(X, n__from(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(n^1))
The following argument positions are usable:
Uargs(fst) = {}, Uargs(s) = {1}, Uargs(cons) = {2},
Uargs(n__fst) = {1, 2}, Uargs(activate) = {}, Uargs(from) = {},
Uargs(n__from) = {}, Uargs(add) = {}, Uargs(n__add) = {1},
Uargs(len) = {}, Uargs(n__len) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[fst](x1, x2) = [3] x1 + [3] x2 + [2]
[0] = [2]
[nil] = [3]
[s](x1) = [1] x1 + [1]
[cons](x1, x2) = [1] x2 + [1]
[n__fst](x1, x2) = [1] x1 + [1] x2 + [0]
[activate](x1) = [3] x1 + [3]
[from](x1) = [2]
[n__from](x1) = [0]
[add](x1, x2) = [3] x1 + [1] x2 + [2]
[n__add](x1, x2) = [1] x1 + [1] x2 + [0]
[len](x1) = [3] x1 + [2]
[n__len](x1) = [1] x1 + [0]
This order satisfies following ordering constraints
[fst(X1, X2)] = [3] X1 + [3] X2 + [2]
> [1] X1 + [1] X2 + [0]
= [n__fst(X1, X2)]
[fst(0(), Z)] = [3] Z + [8]
> [3]
= [nil()]
[fst(s(X), cons(Y, Z))] = [3] Z + [3] X + [8]
> [3] Z + [3] X + [7]
= [cons(Y, n__fst(activate(X), activate(Z)))]
[activate(X)] = [3] X + [3]
> [1] X + [0]
= [X]
[activate(n__fst(X1, X2))] = [3] X1 + [3] X2 + [3]
> [3] X1 + [3] X2 + [2]
= [fst(X1, X2)]
[activate(n__from(X))] = [3]
> [2]
= [from(X)]
[activate(n__add(X1, X2))] = [3] X1 + [3] X2 + [3]
> [3] X1 + [1] X2 + [2]
= [add(X1, X2)]
[activate(n__len(X))] = [3] X + [3]
> [3] X + [2]
= [len(X)]
[from(X)] = [2]
> [1]
= [cons(X, n__from(s(X)))]
[from(X)] = [2]
> [0]
= [n__from(X)]
[add(X1, X2)] = [3] X1 + [1] X2 + [2]
> [1] X1 + [1] X2 + [0]
= [n__add(X1, X2)]
[add(0(), X)] = [1] X + [8]
> [1] X + [0]
= [X]
[add(s(X), Y)] = [3] X + [1] Y + [5]
> [3] X + [1] Y + [4]
= [s(n__add(activate(X), Y))]
[len(X)] = [3] X + [2]
> [1] X + [0]
= [n__len(X)]
[len(nil())] = [11]
> [2]
= [0()]
[len(cons(X, Z))] = [3] Z + [5]
> [3] Z + [4]
= [s(n__len(activate(Z)))]
Hurray, we answered YES(?,O(n^1))
lmpo
YES(?,ELEMENTARY)
We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).
Strict Trs:
{ fst(0(), Z) -> nil()
, fst(s(X), cons(Y, Z)) ->
cons(Y, n__fst(activate(X), activate(Z)))
, from(X) -> cons(X, n__from(s(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(n__add(activate(X), Y))
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z)))
, fst(X1, X2) -> n__fst(X1, X2)
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, len(X) -> n__len(X)
, activate(n__fst(X1, X2)) -> fst(X1, X2)
, activate(n__from(X)) -> from(X)
, activate(n__add(X1, X2)) -> add(X1, X2)
, activate(n__len(X)) -> len(X)
, activate(X) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(?,ELEMENTARY)
The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping
safe(fst) = {}, safe(0) = {}, safe(nil) = {}, safe(s) = {1},
safe(cons) = {1, 2}, safe(n__fst) = {1, 2}, safe(activate) = {},
safe(from) = {}, safe(n__from) = {1}, safe(add) = {},
safe(n__add) = {1, 2}, safe(len) = {}, safe(n__len) = {1}
and precedence
fst ~ activate, activate ~ from, activate ~ add, activate ~ len .
Following symbols are considered recursive:
{fst, activate, from, add, len}
The recursion depth is 1.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ fst(0(), Z;) -> nil()
, fst(s(; X), cons(; Y, Z);) ->
cons(; Y, n__fst(; activate(X;), activate(Z;)))
, from(X;) -> cons(; X, n__from(; s(; X)))
, add(0(), X;) -> X
, add(s(; X), Y;) -> s(; n__add(; activate(X;), Y))
, len(nil();) -> 0()
, len(cons(; X, Z);) -> s(; n__len(; activate(Z;)))
, fst(X1, X2;) -> n__fst(; X1, X2)
, from(X;) -> n__from(; X)
, add(X1, X2;) -> n__add(; X1, X2)
, len(X;) -> n__len(; X)
, activate(n__fst(; X1, X2);) -> fst(X1, X2;)
, activate(n__from(; X);) -> from(X;)
, activate(n__add(; X1, X2);) -> add(X1, X2;)
, activate(n__len(; X);) -> len(X;)
, activate(X;) -> X }
Weak Trs :
Hurray, we answered YES(?,ELEMENTARY)
mpo
YES(?,PRIMREC)
We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).
Strict Trs:
{ fst(0(), Z) -> nil()
, fst(s(X), cons(Y, Z)) ->
cons(Y, n__fst(activate(X), activate(Z)))
, from(X) -> cons(X, n__from(s(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(n__add(activate(X), Y))
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z)))
, fst(X1, X2) -> n__fst(X1, X2)
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, len(X) -> n__len(X)
, activate(n__fst(X1, X2)) -> fst(X1, X2)
, activate(n__from(X)) -> from(X)
, activate(n__add(X1, X2)) -> add(X1, X2)
, activate(n__len(X)) -> len(X)
, activate(X) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(?,PRIMREC)
The input was oriented with the instance of'multiset path orders'
as induced by the precedence
fst > cons, fst > n__fst, nil > 0, activate > from, from > s,
from > cons, from > n__from, add > s, add > n__add, len > s,
len > n__len, fst ~ nil, fst ~ activate, activate ~ add,
activate ~ len .
Hurray, we answered YES(?,PRIMREC)
popstar
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fst(0(), Z) -> nil()
, fst(s(X), cons(Y, Z)) ->
cons(Y, n__fst(activate(X), activate(Z)))
, from(X) -> cons(X, n__from(s(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(n__add(activate(X), Y))
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z)))
, fst(X1, X2) -> n__fst(X1, X2)
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, len(X) -> n__len(X)
, activate(n__fst(X1, X2)) -> fst(X1, X2)
, activate(n__from(X)) -> from(X)
, activate(n__add(X1, X2)) -> add(X1, X2)
, activate(n__len(X)) -> len(X)
, activate(X) -> X }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fst(0(), Z) -> nil()
, fst(s(X), cons(Y, Z)) ->
cons(Y, n__fst(activate(X), activate(Z)))
, from(X) -> cons(X, n__from(s(X)))
, add(0(), X) -> X
, add(s(X), Y) -> s(n__add(activate(X), Y))
, len(nil()) -> 0()
, len(cons(X, Z)) -> s(n__len(activate(Z)))
, fst(X1, X2) -> n__fst(X1, X2)
, from(X) -> n__from(X)
, add(X1, X2) -> n__add(X1, X2)
, len(X) -> n__len(X)
, activate(n__fst(X1, X2)) -> fst(X1, X2)
, activate(n__from(X)) -> from(X)
, activate(n__add(X1, X2)) -> add(X1, X2)
, activate(n__len(X)) -> len(X)
, activate(X) -> X }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..