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))
  Usable Rule 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()))
    ++(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()))
     ++(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()))
      ++(nil(),y) -> y
      ++(.(x,y),z) -> .(x,++(y,z))
     graph:
      rev#(.(x,y)) -> ++#(rev(y),.(x,nil())) -> ++#(.(x,y),z) -> ++#(y,z)
     Restore Modifier:
      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))
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 1/9