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)
   CDG 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)
    graph:
     ++#(.(x,y),z) -> ++#(y,z) -> ++#(.(x,y),z) -> ++#(y,z)
     ++#(x,++(y,z)) -> ++#(++(x,y),z) -> ++#(.(x,y),z) -> ++#(y,z)
     ++#(x,++(y,z)) -> ++#(x,y) -> ++#(.(x,y),z) -> ++#(y,z)
     rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
     ++#(.(x,y),z) -> ++#(y,z)
     rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
     ++#(x,++(y,z)) -> ++#(x,y)
     rev#(++(x,y)) -> ++#(rev(y),rev(x)) -> ++#(x,++(y,z)) -> ++#(++(x,y),z)
    Restore Modifier:
     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())
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 6/36
      DPs:
       ++#(.(x,y),z) -> ++#(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:
       dimension: 1
       interpretation:
        [++#](x0, x1) = x0 + 1,
        
        [make](x0) = x0 + 1,
        
        [.](x0, x1) = x1 + 1,
        
        [++](x0, x1) = x0 + x1,
        
        [rev](x0) = x0,
        
        [nil] = 0
       orientation:
        ++#(.(x,y),z) = y + 2 >= y + 1 = ++#(y,z)
        
        rev(nil()) = 0 >= 0 = nil()
        
        rev(rev(x)) = x >= x = x
        
        rev(++(x,y)) = x + y >= x + y = ++(rev(y),rev(x))
        
        ++(nil(),y) = y >= y = y
        
        ++(x,nil()) = x >= x = x
        
        ++(.(x,y),z) = y + z + 1 >= y + z + 1 = .(x,++(y,z))
        
        ++(x,++(y,z)) = x + y + z >= x + y + z = ++(++(x,y),z)
        
        make(x) = x + 1 >= 1 = .(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