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())
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [++#](x0, x1) = x0 + 3/2x1,
    
    [rev#](x0) = 7/2x0,
    
    [make](x0) = 5/2x0 + 2,
    
    [.](x0, x1) = 2x0 + x1 + 1/2,
    
    [++](x0, x1) = x0 + x1 + 1,
    
    [rev](x0) = 2x0,
    
    [nil] = 3/2
   orientation:
    rev#(++(x,y)) = 7/2x + 7/2y + 7/2 >= 7/2x = rev#(x)
    
    rev#(++(x,y)) = 7/2x + 7/2y + 7/2 >= 7/2y = rev#(y)
    
    rev#(++(x,y)) = 7/2x + 7/2y + 7/2 >= 3x + 2y = ++#(rev(y),rev(x))
    
    ++#(.(x,y),z) = 2x + y + 3/2z + 1/2 >= y + 3/2z = ++#(y,z)
    
    ++#(x,++(y,z)) = x + 3/2y + 3/2z + 3/2 >= x + 3/2y = ++#(x,y)
    
    ++#(x,++(y,z)) = x + 3/2y + 3/2z + 3/2 >= x + y + 3/2z + 1 = ++#(++(x,y),z)
    
    rev(nil()) = 3 >= 3/2 = nil()
    
    rev(rev(x)) = 4x >= x = x
    
    rev(++(x,y)) = 2x + 2y + 2 >= 2x + 2y + 1 = ++(rev(y),rev(x))
    
    ++(nil(),y) = y + 5/2 >= y = y
    
    ++(x,nil()) = x + 5/2 >= x = x
    
    ++(.(x,y),z) = 2x + y + z + 3/2 >= 2x + y + z + 3/2 = .(x,++(y,z))
    
    ++(x,++(y,z)) = x + y + z + 2 >= x + y + z + 2 = ++(++(x,y),z)
    
    make(x) = 5/2x + 2 >= 2x + 2 = .(x,nil())
   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)
     make(x) -> .(x,nil())
   Qed