YES(?,ELEMENTARY)

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

Strict Trs:
  { app(nil(), YS) -> YS
  , app(cons(X), YS) -> cons(X)
  , from(X) -> cons(X)
  , zWadr(XS, nil()) -> nil()
  , zWadr(nil(), YS) -> nil()
  , zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
  , prefix(L) -> cons(nil()) }
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(app) = {2}, safe(nil) = {}, safe(cons) = {1}, safe(from) = {},
 safe(zWadr) = {1}, safe(prefix) = {}

and precedence

 app > from, app > prefix, zWadr > from, zWadr > prefix,
 app ~ zWadr, from ~ prefix .

Following symbols are considered recursive:

 {app, zWadr}

The recursion depth is 1.

For your convenience, here are the satisfied ordering constraints:

               app(nil(); YS) > YS                       
                                                         
           app(cons(; X); YS) > cons(; X)                
                                                         
                     from(X;) > cons(; X)                
                                                         
             zWadr(nil(); XS) > nil()                    
                                                         
             zWadr(YS; nil()) > nil()                    
                                                         
  zWadr(cons(; Y); cons(; X)) > cons(; app(Y; cons(; X)))
                                                         
                   prefix(L;) > cons(; nil())            
                                                         

Hurray, we answered YES(?,ELEMENTARY)