We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, sel(0(), cons(X, Y)) -> X
, sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(activate(X)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
Arguments of following rules are not normal-forms:
{ sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)) }
All above mentioned rules can be savely removed.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ from(X) -> cons(X, n__from(n__s(X)))
, from(X) -> n__from(X)
, sel(0(), cons(X, Y)) -> X
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__from(X)) -> from(activate(X))
, activate(n__s(X)) -> s(activate(X)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(from) = {1}, safe(cons) = {1, 2}, safe(n__from) = {1},
safe(n__s) = {1}, safe(sel) = {}, safe(0) = {}, safe(s) = {1},
safe(activate) = {}
and precedence
activate > from, activate > s .
Following symbols are considered recursive:
{activate}
The recursion depth is 1.
For your convenience, here are the satisfied ordering constraints:
from(; X) > cons(; X, n__from(; n__s(; X)))
from(; X) > n__from(; X)
sel(0(), cons(; X, Y);) > X
s(; X) > n__s(; X)
activate(X;) > X
activate(n__from(; X);) > from(; activate(X;))
activate(n__s(; X);) > s(; activate(X;))
Hurray, we answered YES(?,O(n^1))