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))
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     rev(nil()) -> nil()
     rev(.(x,y)) -> ++(rev(y),.(x,nil()))
     ++(nil(),y) -> y
     ++(.(x,y),z) -> .(x,++(y,z))
    interpretation:
     [++#](x0, x1) = 5x0 + 2,
     
     [rev#](x0) = 5x0 + 2,
     
     [++](x0, x1) = x0 + x1,
     
     [.](x0, x1) = x1 + 5,
     
     [rev](x0) = x0,
     
     [nil] = 0
    orientation:
     rev#(.(x,y)) = 5y + 27 >= 5y + 2 = rev#(y)
     
     rev#(.(x,y)) = 5y + 27 >= 5y + 2 = ++#(rev(y),.(x,nil()))
     
     ++#(.(x,y),z) = 5y + 27 >= 5y + 2 = ++#(y,z)
     
     rev(nil()) = 0 >= 0 = nil()
     
     rev(.(x,y)) = y + 5 >= y + 5 = ++(rev(y),.(x,nil()))
     
     ++(nil(),y) = y >= y = y
     
     ++(.(x,y),z) = y + z + 5 >= y + z + 5 = .(x,++(y,z))
    problem:
     DPs:
      
     TRS:
      rev(nil()) -> nil()
      rev(.(x,y)) -> ++(rev(y),.(x,nil()))
      ++(nil(),y) -> y
      ++(.(x,y),z) -> .(x,++(y,z))
    Qed