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