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())) -> c(n__f(n__g(n__f(n__a()))))
, a() -> n__a()
, g(X) -> n__g(X)
, activate(X) -> X
, activate(n__f(X)) -> f(activate(X))
, activate(n__g(X)) -> g(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())) -> c(n__f(n__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()
, g(X) -> n__g(X)
, activate(X) -> X
, activate(n__f(X)) -> f(activate(X))
, activate(n__g(X)) -> g(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__g) = {1},
safe(n__a) = {}, safe(g) = {1}, safe(activate) = {}
and precedence
activate > f, activate > a, activate > g .
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()
g(; X) > n__g(; X)
activate(X;) > X
activate(n__f(; X);) > f(; activate(X;))
activate(n__g(; X);) > g(; activate(X;))
activate(n__a();) > a()
Hurray, we answered YES(?,O(n^1))