interpretations
YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ first(X1, X2) -> n__first(X1, X2)
, first(0(), X) -> nil()
, first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
, activate(X) -> X
, activate(n__first(X1, X2)) -> first(X1, X2)
, activate(n__from(X)) -> from(X)
, from(X) -> cons(X, n__from(s(X)))
, from(X) -> n__from(X) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The following argument positions are usable:
Uargs(first) = {}, Uargs(s) = {}, Uargs(cons) = {2},
Uargs(n__first) = {2}, Uargs(activate) = {}, Uargs(from) = {},
Uargs(n__from) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[first](x1, x2) = [2] x1 + [2] x2 + [1]
[0] = [3]
[nil] = [0]
[s](x1) = [1] x1 + [2]
[cons](x1, x2) = [1] x2 + [0]
[n__first](x1, x2) = [1] x1 + [1] x2 + [0]
[activate](x1) = [2] x1 + [3]
[from](x1) = [2]
[n__from](x1) = [0]
This order satisfies following ordering constraints
[first(X1, X2)] = [2] X1 + [2] X2 + [1]
> [1] X1 + [1] X2 + [0]
= [n__first(X1, X2)]
[first(0(), X)] = [2] X + [7]
> [0]
= [nil()]
[first(s(X), cons(Y, Z))] = [2] X + [2] Z + [5]
> [1] X + [2] Z + [3]
= [cons(Y, n__first(X, activate(Z)))]
[activate(X)] = [2] X + [3]
> [1] X + [0]
= [X]
[activate(n__first(X1, X2))] = [2] X1 + [2] X2 + [3]
> [2] X1 + [2] X2 + [1]
= [first(X1, X2)]
[activate(n__from(X))] = [3]
> [2]
= [from(X)]
[from(X)] = [2]
> [0]
= [cons(X, n__from(s(X)))]
[from(X)] = [2]
> [0]
= [n__from(X)]
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:
{ first(0(), X) -> nil()
, first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
, from(X) -> cons(X, n__from(s(X)))
, first(X1, X2) -> n__first(X1, X2)
, from(X) -> n__from(X)
, activate(n__first(X1, X2)) -> first(X1, X2)
, activate(n__from(X)) -> from(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(first) = {}, safe(0) = {}, safe(nil) = {}, safe(s) = {1},
safe(cons) = {1, 2}, safe(n__first) = {1, 2}, safe(activate) = {},
safe(from) = {}, safe(n__from) = {1}
and precedence
first ~ activate, activate ~ from .
Following symbols are considered recursive:
{first, activate, from}
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:
{ first(0(), X;) -> nil()
, first(s(; X), cons(; Y, Z);) ->
cons(; Y, n__first(; X, activate(Z;)))
, from(X;) -> cons(; X, n__from(; s(; X)))
, first(X1, X2;) -> n__first(; X1, X2)
, from(X;) -> n__from(; X)
, activate(n__first(; X1, X2);) -> first(X1, X2;)
, activate(n__from(; X);) -> from(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:
{ first(0(), X) -> nil()
, first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
, from(X) -> cons(X, n__from(s(X)))
, first(X1, X2) -> n__first(X1, X2)
, from(X) -> n__from(X)
, activate(n__first(X1, X2)) -> first(X1, X2)
, activate(n__from(X)) -> from(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
first > cons, first > n__first, 0 > nil, activate > from, from > s,
from > cons, from > n__from, first ~ activate .
Hurray, we answered YES(?,PRIMREC)
popstar
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ first(0(), X) -> nil()
, first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
, from(X) -> cons(X, n__from(s(X)))
, first(X1, X2) -> n__first(X1, X2)
, from(X) -> n__from(X)
, activate(n__first(X1, X2)) -> first(X1, X2)
, activate(n__from(X)) -> from(X)
, activate(X) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order'
as induced by the safe mapping
safe(first) = {}, safe(0) = {}, safe(nil) = {}, safe(s) = {1},
safe(cons) = {1, 2}, safe(n__first) = {1, 2}, safe(activate) = {},
safe(from) = {}, safe(n__from) = {1}
and precedence
first ~ activate, activate ~ from .
Following symbols are considered recursive:
{first, activate, from}
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:
{ first(0(), X;) -> nil()
, first(s(; X), cons(; Y, Z);) ->
cons(; Y, n__first(; X, activate(Z;)))
, from(X;) -> cons(; X, n__from(; s(; X)))
, first(X1, X2;) -> n__first(; X1, X2)
, from(X;) -> n__from(; X)
, activate(n__first(; X1, X2);) -> first(X1, X2;)
, activate(n__from(; X);) -> from(X;)
, activate(X;) -> X }
Weak Trs :
Hurray, we answered YES(?,POLY)
popstar-ps
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ first(0(), X) -> nil()
, first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
, from(X) -> cons(X, n__from(s(X)))
, first(X1, X2) -> n__first(X1, X2)
, from(X) -> n__from(X)
, activate(n__first(X1, X2)) -> first(X1, X2)
, activate(n__from(X)) -> from(X)
, activate(X) -> X }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order
(PS)' as induced by the safe mapping
safe(first) = {}, safe(0) = {}, safe(nil) = {}, safe(s) = {1},
safe(cons) = {1, 2}, safe(n__first) = {1, 2}, safe(activate) = {},
safe(from) = {1}, safe(n__from) = {1}
and precedence
first ~ activate, activate ~ from .
Following symbols are considered recursive:
{first, activate, from}
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:
{ first(0(), X;) -> nil()
, first(s(; X), cons(; Y, Z);) ->
cons(; Y, n__first(; X, activate(Z;)))
, from(; X) -> cons(; X, n__from(; s(; X)))
, first(X1, X2;) -> n__first(; X1, X2)
, from(; X) -> n__from(; X)
, activate(n__first(; X1, X2);) -> first(X1, X2;)
, activate(n__from(; X);) -> from(; X)
, activate(X;) -> X }
Weak Trs :
Hurray, we answered YES(?,POLY)