YES(?,PRIMREC)

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

Strict Trs:
  { rev(nil()) -> nil()
  , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
  , ++(nil(), y) -> y
  , ++(.(x, y), z) -> .(x, ++(y, z))
  , car(.(x, y)) -> x
  , cdr(.(x, y)) -> y
  , null(nil()) -> true()
  , null(.(x, y)) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 rev > nil, rev > ., rev > ++, rev > cdr, rev > false, . > nil,
 ++ > nil, ++ > ., ++ > false, car > nil, car > ., car > ++,
 car > cdr, car > false, cdr > nil, cdr > ., cdr > false,
 null > nil, null > ., null > ++, null > cdr, null > false,
 true > nil, true > ., true > ++, true > cdr, true > false,
 false > nil, rev ~ car, rev ~ null, rev ~ true, . ~ false,
 ++ ~ cdr, car ~ null, car ~ true, null ~ true .

Hurray, we answered YES(?,PRIMREC)