We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ f(X) -> g(n__h(n__f(X)))
, f(X) -> n__f(X)
, h(X) -> n__h(X)
, activate(X) -> X
, activate(n__h(X)) -> h(activate(X))
, activate(n__f(X)) -> f(activate(X)) }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
The input is overlay and right-linear. Switching to innermost
rewriting.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ f(X) -> g(n__h(n__f(X)))
, f(X) -> n__f(X)
, h(X) -> n__h(X)
, activate(X) -> X
, activate(n__h(X)) -> h(activate(X))
, activate(n__f(X)) -> f(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(f) = {1}, safe(g) = {1}, safe(n__h) = {1}, safe(n__f) = {1},
safe(h) = {1}, safe(activate) = {}
and precedence
activate > f, activate > h .
Following symbols are considered recursive:
{activate}
The recursion depth is 1.
For your convenience, here are the satisfied ordering constraints:
f(; X) > g(; n__h(; n__f(; X)))
f(; X) > n__f(; X)
h(; X) > n__h(; X)
activate(X;) > X
activate(n__h(; X);) > h(; activate(X;))
activate(n__f(; X);) > f(; activate(X;))
Hurray, we answered YES(?,O(n^1))