We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ sum(0()) -> 0()
, sum(s(x)) -> +(sum(x), s(x))
, sum1(0()) -> 0()
, sum1(s(x)) -> s(+(sum1(x), +(x, x))) }
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(sum) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1, 2},
safe(sum1) = {}
and precedence
empty .
Following symbols are considered recursive:
{sum, sum1}
The recursion depth is 1.
For your convenience, here are the satisfied ordering constraints:
sum(0();) > 0()
sum(s(; x);) > +(; sum(x;), s(; x))
sum1(0();) > 0()
sum1(s(; x);) > s(; +(; sum1(x;), +(; x, x)))
Hurray, we answered YES(?,O(n^1))