YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ rec[even_0][1](0()) -> True()
, rec[even_0][1](S(0())) -> False()
, rec[even_0][1](S(S(x2))) -> rec[even_0][1](x2)
, main(x1) -> rec[even_0][1](x1) }
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(0) = {}, safe(rec[even_0][1]) = {}, safe(True) = {},
safe(S) = {1}, safe(False) = {}, safe(main) = {}
and precedence
main > rec[even_0][1] .
Following symbols are considered recursive:
{rec[even_0][1]}
The recursion depth is 1.
For your convenience, here are the satisfied ordering constraints:
rec[even_0][1](0();) > True()
rec[even_0][1](S(; 0());) > False()
rec[even_0][1](S(; S(; x2));) > rec[even_0][1](x2;)
main(x1;) > rec[even_0][1](x1;)
Hurray, we answered YES(?,O(n^1))