YES(?,O(1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(1)).

Strict Trs:
  { b(x, y) -> c(a(c(y), a(0(), x)))
  , a(y, x) -> y
  , a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

Arguments of following rules are not normal-forms:

{ a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()) }

All above mentioned rules can be savely removed.

We are left with following problem, upon which TcT provides the
certificate YES(?,O(1)).

Strict Trs:
  { b(x, y) -> c(a(c(y), a(0(), x)))
  , a(y, x) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS,0-bounded)' as induced by the safe mapping

 safe(b) = {1}, safe(c) = {1}, safe(a) = {1, 2}, safe(0) = {}

and precedence

 b > a .

Following symbols are considered recursive:

 {}

The recursion depth is 0.

For your convenience, here are the satisfied ordering constraints:

     b(y; x) > c(; a(; c(; y),  a(; 0(),  x)))
                                              
  a(; y,  x) > y                              
                                              

Hurray, we answered YES(?,O(1))