YES(?,ELEMENTARY)

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

Strict Trs:
  { bin(x, 0()) -> s(0())
  , bin(0(), s(y)) -> 0()
  , bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,ELEMENTARY)

The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping

 safe(bin) = {2}, safe(0) = {}, safe(s) = {1}, safe(+) = {1, 2}

and precedence

 empty .

Following symbols are considered recursive:

 {bin}

The recursion depth is 1.

For your convenience, here are the satisfied ordering constraints:

          bin(x; 0()) > s(; 0())                       
                                                       
     bin(0(); s(; y)) > 0()                            
                                                       
  bin(s(; x); s(; y)) > +(; bin(x; s(; y)),  bin(x; y))
                                                       

Hurray, we answered YES(?,ELEMENTARY)