YES

Problem:
 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))

Proof:
 DP Processor:
  DPs:
   rev#(.(x,y)) -> rev#(y)
   rev#(.(x,y)) -> ++#(rev(y),.(x,nil()))
   ++#(.(x,y),z) -> ++#(y,z)
  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))
  TDG Processor:
   DPs:
    rev#(.(x,y)) -> rev#(y)
    rev#(.(x,y)) -> ++#(rev(y),.(x,nil()))
    ++#(.(x,y),z) -> ++#(y,z)
   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))
   graph:
    ++#(.(x,y),z) -> ++#(y,z) -> ++#(.(x,y),z) -> ++#(y,z)
    rev#(.(x,y)) -> ++#(rev(y),.(x,nil())) -> ++#(.(x,y),z) -> ++#(y,z)
    rev#(.(x,y)) -> rev#(y) -> rev#(.(x,y)) -> ++#(rev(y),.(x,nil()))
    rev#(.(x,y)) -> rev#(y) -> rev#(.(x,y)) -> rev#(y)
   CDG Processor:
    DPs:
     rev#(.(x,y)) -> rev#(y)
     rev#(.(x,y)) -> ++#(rev(y),.(x,nil()))
     ++#(.(x,y),z) -> ++#(y,z)
    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))
    graph:
     rev#(.(x,y)) -> ++#(rev(y),.(x,nil())) -> ++#(.(x,y),z) -> ++#(y,z)
    SCC Processor:
     #sccs: 0
     #rules: 0
     #arcs: 1/9