YES(?,ELEMENTARY)

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

Strict Trs:
  { a__eq(X, Y) -> false()
  , a__eq(X1, X2) -> eq(X1, X2)
  , a__eq(0(), 0()) -> true()
  , a__eq(s(X), s(Y)) -> a__eq(X, Y)
  , a__inf(X) -> cons(X, inf(s(X)))
  , a__inf(X) -> inf(X)
  , a__take(X1, X2) -> take(X1, X2)
  , a__take(0(), X) -> nil()
  , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
  , a__length(X) -> length(X)
  , a__length(cons(X, L)) -> s(length(L))
  , a__length(nil()) -> 0()
  , mark(0()) -> 0()
  , mark(true()) -> true()
  , mark(s(X)) -> s(X)
  , mark(false()) -> false()
  , mark(cons(X1, X2)) -> cons(X1, X2)
  , mark(inf(X)) -> a__inf(mark(X))
  , mark(nil()) -> nil()
  , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
  , mark(length(X)) -> a__length(mark(X))
  , mark(eq(X1, X2)) -> a__eq(X1, X2) }
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(a__eq) = {}, safe(0) = {}, safe(true) = {}, safe(s) = {1},
 safe(false) = {}, safe(a__inf) = {1}, safe(cons) = {1, 2},
 safe(inf) = {1}, safe(a__take) = {1, 2}, safe(nil) = {},
 safe(take) = {1, 2}, safe(a__length) = {1}, safe(length) = {1},
 safe(mark) = {}, safe(eq) = {1, 2}

and precedence

 mark > a__eq, mark > a__inf, mark > a__take, mark > a__length,
 a__eq ~ a__inf, a__eq ~ a__take, a__eq ~ a__length,
 a__inf ~ a__take, a__inf ~ a__length, a__take ~ a__length .

Following symbols are considered recursive:

 {a__eq, a__inf, a__take, a__length, mark}

The recursion depth is 2.

For your convenience, here are the satisfied ordering constraints:

                      a__eq(X,  Y;) > false()                         
                                                                      
                    a__eq(X1,  X2;) > eq(; X1,  X2)                   
                                                                      
                  a__eq(0(),  0();) > true()                          
                                                                      
            a__eq(s(; X),  s(; Y);) > a__eq(X,  Y;)                   
                                                                      
                        a__inf(; X) > cons(; X,  inf(; s(; X)))       
                                                                      
                        a__inf(; X) > inf(; X)                        
                                                                      
                 a__take(; X1,  X2) > take(; X1,  X2)                 
                                                                      
                 a__take(; 0(),  X) > nil()                           
                                                                      
  a__take(; s(; X),  cons(; Y,  L)) > cons(; Y,  take(; X,  L))       
                                                                      
                     a__length(; X) > length(; X)                     
                                                                      
         a__length(; cons(; X,  L)) > s(; length(; L))                
                                                                      
                 a__length(; nil()) > 0()                             
                                                                      
                         mark(0();) > 0()                             
                                                                      
                      mark(true();) > true()                          
                                                                      
                      mark(s(; X);) > s(; X)                          
                                                                      
                     mark(false();) > false()                         
                                                                      
             mark(cons(; X1,  X2);) > cons(; X1,  X2)                 
                                                                      
                    mark(inf(; X);) > a__inf(; mark(X;))              
                                                                      
                       mark(nil();) > nil()                           
                                                                      
             mark(take(; X1,  X2);) > a__take(; mark(X1;),  mark(X2;))
                                                                      
                 mark(length(; X);) > a__length(; mark(X;))           
                                                                      
               mark(eq(; X1,  X2);) > a__eq(X1,  X2;)                 
                                                                      

Hurray, we answered YES(?,ELEMENTARY)