We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ f(X) -> n__f(X)
, f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, 0() -> n__0()
, s(X) -> n__s(X)
, p(s(X)) -> X
, activate(X) -> X
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
Arguments of following rules are not normal-forms:
{ f(0()) -> cons(0(), n__f(n__s(n__0())))
, f(s(0())) -> f(p(s(0())))
, p(s(X)) -> X }
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:
{ f(X) -> n__f(X)
, 0() -> n__0()
, s(X) -> n__s(X)
, activate(X) -> X
, activate(n__f(X)) -> f(activate(X))
, activate(n__s(X)) -> s(activate(X))
, activate(n__0()) -> 0() }
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(f) = {1}, safe(0) = {}, safe(n__f) = {1}, safe(n__s) = {1},
safe(n__0) = {}, safe(s) = {1}, safe(activate) = {}
and precedence
activate > f, activate > 0, activate > s .
Following symbols are considered recursive:
{activate}
The recursion depth is 1.
For your convenience, here are the satisfied ordering constraints:
f(; X) > n__f(; X)
0() > n__0()
s(; X) > n__s(; X)
activate(X;) > X
activate(n__f(; X);) > f(; activate(X;))
activate(n__s(; X);) > s(; activate(X;))
activate(n__0();) > 0()
Hurray, we answered YES(?,O(n^1))