YES(?,PRIMREC)

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

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(?,PRIMREC)

The input was oriented with the instance of'multiset path order' as
induced by the precedence

 merge > nil, merge > ., merge > if, merge > <, nil > .,
 nil > if, < > ., < > if, ++ > nil, ++ > ., ++ > if,
 ++ > <, true > nil, true > ., true > if, true > <,
 false > nil, false > ., false > if, false > <, merge ~ ++,
 merge ~ true, merge ~ false, nil ~ <, . ~ if, ++ ~ true,
 ++ ~ false, true ~ false .

Hurray, we answered YES(?,PRIMREC)