TRS:
 {    rev(nil()) -> nil(),
    rev(.(x, y)) -> ++(rev(y), .(x, nil())),
    car(.(x, y)) -> x,
    cdr(.(x, y)) -> y,
     null(nil()) -> true(),
   null(.(x, y)) -> false(),
    ++(nil(), y) -> y,
  ++(.(x, y), z) -> .(x, ++(y, z))}
 MPO:
  Prec:
   null > true, 
   null > false, 
   rev > nil, 
   rev > ++, 
   rev > ., 
   ++ > .
   empty
  Strict:
   {}
   Weak:
    {}
  Qed