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())) -> ++(x, merge(y, ++(u(), v())))
  , merge(++(x, y), ++(u(), v())) -> ++(u(), merge(++(x, y), v())) }
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 > v, ++ > nil, u > nil, u > ++,
 u > v, v > nil, merge ~ u, ++ ~ v .

Hurray, we answered YES(?,PRIMREC)