YES(?,ELEMENTARY)

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

Strict Trs:
  { merge(x, nil()) -> x
  , merge(nil(), y) -> y
  , merge(.(x, y), .(u, v)) ->
    if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
  , if(true(), x, y) -> x
  , if(false(), x, y) -> x
  , ++(nil(), y) -> y
  , ++(.(x, y), z) -> .(x, ++(y, z)) }
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(merge) = {}, safe(nil) = {}, safe(.) = {1, 2},
 safe(if) = {1, 2, 3}, safe(<) = {1, 2}, safe(++) = {2},
 safe(true) = {}, safe(false) = {}

and precedence

 merge > if, merge > ++, if ~ ++ .

Following symbols are considered recursive:

 {merge, if, ++}

The recursion depth is 2.

For your convenience, here are the satisfied ordering constraints:

                merge(x,  nil();) > x                                     
                                                                          
                merge(nil(),  y;) > y                                     
                                                                          
  merge(.(; x,  y),  .(; u,  v);) > if(; <(; x,  u),                   
                                         .(; x,  merge(y,  .(; u,  v);)), 
                                         .(; u,  merge(.(; x,  y),  v;))) 
                                                                          
             if(; true(),  x,  y) > x                                     
                                                                          
            if(; false(),  x,  y) > x                                     
                                                                          
                     ++(nil(); y) > y                                     
                                                                          
                ++(.(; x,  y); z) > .(; x,  ++(y; z))                     
                                                                          

Hurray, we answered YES(?,ELEMENTARY)