YES

Problem:
 rev(nil()) -> nil()
 rev(rev(x)) -> x
 rev(++(x,y)) -> ++(rev(y),rev(x))
 ++(nil(),y) -> y
 ++(x,nil()) -> x
 ++(.(x,y),z) -> .(x,++(y,z))
 ++(x,++(y,z)) -> ++(++(x,y),z)
 make(x) -> .(x,nil())

Proof:
 DP Processor:
  DPs:
   rev#(++(x,y)) -> rev#(x)
   rev#(++(x,y)) -> rev#(y)
   rev#(++(x,y)) -> ++#(rev(y),rev(x))
   ++#(.(x,y),z) -> ++#(y,z)
   ++#(x,++(y,z)) -> ++#(x,y)
   ++#(x,++(y,z)) -> ++#(++(x,y),z)
  TRS:
   rev(nil()) -> nil()
   rev(rev(x)) -> x
   rev(++(x,y)) -> ++(rev(y),rev(x))
   ++(nil(),y) -> y
   ++(x,nil()) -> x
   ++(.(x,y),z) -> .(x,++(y,z))
   ++(x,++(y,z)) -> ++(++(x,y),z)
   make(x) -> .(x,nil())
  Usable Rule Processor:
   DPs:
    rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> rev#(y)
    rev#(++(x,y)) -> ++#(rev(y),rev(x))
    ++#(.(x,y),z) -> ++#(y,z)
    ++#(x,++(y,z)) -> ++#(x,y)
    ++#(x,++(y,z)) -> ++#(++(x,y),z)
   TRS:
    rev(nil()) -> nil()
    rev(rev(x)) -> x
    rev(++(x,y)) -> ++(rev(y),rev(x))
    ++(nil(),y) -> y
    ++(x,nil()) -> x
    ++(.(x,y),z) -> .(x,++(y,z))
    ++(x,++(y,z)) -> ++(++(x,y),z)
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     rev(nil()) -> nil()
     rev(rev(x)) -> x
     rev(++(x,y)) -> ++(rev(y),rev(x))
     ++(nil(),y) -> y
     ++(x,nil()) -> x
     ++(.(x,y),z) -> .(x,++(y,z))
     ++(x,++(y,z)) -> ++(++(x,y),z)
    interpretation:
     [++#](x0, x1) = 4x0 + 6x1 + 6,
     
     [rev#](x0) = 7x0 + 3,
     
     [.](x0, x1) = x1 + 2,
     
     [++](x0, x1) = x0 + x1 + 4,
     
     [rev](x0) = x0,
     
     [nil] = 4
    orientation:
     rev#(++(x,y)) = 7x + 7y + 31 >= 7x + 3 = rev#(x)
     
     rev#(++(x,y)) = 7x + 7y + 31 >= 7y + 3 = rev#(y)
     
     rev#(++(x,y)) = 7x + 7y + 31 >= 6x + 4y + 6 = ++#(rev(y),rev(x))
     
     ++#(.(x,y),z) = 4y + 6z + 14 >= 4y + 6z + 6 = ++#(y,z)
     
     ++#(x,++(y,z)) = 4x + 6y + 6z + 30 >= 4x + 6y + 6 = ++#(x,y)
     
     ++#(x,++(y,z)) = 4x + 6y + 6z + 30 >= 4x + 4y + 6z + 22 = ++#(++(x,y),z)
     
     rev(nil()) = 4 >= 4 = nil()
     
     rev(rev(x)) = x >= x = x
     
     rev(++(x,y)) = x + y + 4 >= x + y + 4 = ++(rev(y),rev(x))
     
     ++(nil(),y) = y + 8 >= y = y
     
     ++(x,nil()) = x + 8 >= x = x
     
     ++(.(x,y),z) = y + z + 6 >= y + z + 6 = .(x,++(y,z))
     
     ++(x,++(y,z)) = x + y + z + 8 >= x + y + z + 8 = ++(++(x,y),z)
    problem:
     DPs:
      
     TRS:
      rev(nil()) -> nil()
      rev(rev(x)) -> x
      rev(++(x,y)) -> ++(rev(y),rev(x))
      ++(nil(),y) -> y
      ++(x,nil()) -> x
      ++(.(x,y),z) -> .(x,++(y,z))
      ++(x,++(y,z)) -> ++(++(x,y),z)
    Qed