We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ f(X) -> n__f(X)
, f(f(a())) -> f(g(n__f(n__a())))
, a() -> n__a()
, activate(X) -> X
, activate(n__f(X)) -> f(activate(X))
, activate(n__a()) -> a() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
Arguments of following rules are not normal-forms:
{ f(f(a())) -> f(g(n__f(n__a()))) }
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)
, a() -> n__a()
, activate(X) -> X
, activate(n__f(X)) -> f(activate(X))
, activate(n__a()) -> a() }
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(a) = {}, safe(n__f) = {1}, safe(n__a) = {},
safe(activate) = {}
and precedence
activate > f, activate > a .
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)
a() > n__a()
activate(X;) > X
activate(n__f(; X);) > f(; activate(X;))
activate(n__a();) > a()
Hurray, we answered YES(?,O(n^1))