We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ g(s(x)) -> f(x)
, g(0()) -> 0()
, f(s(x)) -> s(s(g(x)))
, f(0()) -> s(0()) }
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:
{ g(s(x)) -> f(x)
, g(0()) -> 0()
, f(s(x)) -> s(s(g(x)))
, f(0()) -> s(0()) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The input was oriented with the instance of 'Small Polynomial Path
Order (PS)' as induced by the safe mapping
safe(g) = {}, safe(s) = {1}, safe(f) = {}, safe(0) = {}
and precedence
g ~ f .
Following symbols are considered recursive:
{g, f}
The recursion depth is 1.
For your convenience, here are the satisfied ordering constraints:
g(s(; x);) > f(x;)
g(0();) > 0()
f(s(; x);) > s(; s(; g(x;)))
f(0();) > s(; 0())
Hurray, we answered YES(?,O(n^1))