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)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 4/9
    DPs:
     rev#(.(x,y)) -> rev#(y)
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(rev#) = 0
     problem:
      DPs:
       
      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))
     Qed
    
    DPs:
     ++#(.(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))
    Subterm Criterion Processor:
     simple projection:
      pi(++#) = 0
     problem:
      DPs:
       
      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))
     Qed