YES

Problem:
 rev(nil()) -> nil()
 rev(++(x,y)) -> ++(rev1(x,y),rev2(x,y))
 rev1(x,nil()) -> x
 rev1(x,++(y,z)) -> rev1(y,z)
 rev2(x,nil()) -> nil()
 rev2(x,++(y,z)) -> rev(++(x,rev(rev2(y,z))))

Proof:
 DP Processor:
  DPs:
   rev#(++(x,y)) -> rev2#(x,y)
   rev#(++(x,y)) -> rev1#(x,y)
   rev1#(x,++(y,z)) -> rev1#(y,z)
   rev2#(x,++(y,z)) -> rev2#(y,z)
   rev2#(x,++(y,z)) -> rev#(rev2(y,z))
   rev2#(x,++(y,z)) -> rev#(++(x,rev(rev2(y,z))))
  TRS:
   rev(nil()) -> nil()
   rev(++(x,y)) -> ++(rev1(x,y),rev2(x,y))
   rev1(x,nil()) -> x
   rev1(x,++(y,z)) -> rev1(y,z)
   rev2(x,nil()) -> nil()
   rev2(x,++(y,z)) -> rev(++(x,rev(rev2(y,z))))
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    rev(nil()) -> nil()
    rev(++(x,y)) -> ++(rev1(x,y),rev2(x,y))
    rev2(x,nil()) -> nil()
    rev2(x,++(y,z)) -> rev(++(x,rev(rev2(y,z))))
   interpretation:
    [rev1#](x0, x1) = x1,
    
    [rev2#](x0, x1) = 4x1 + 6,
    
    [rev#](x0) = 2x0 + 7,
    
    [rev2](x0, x1) = x1,
    
    [rev1](x0, x1) = 4x1 + 6,
    
    [++](x0, x1) = 2x1 + 1,
    
    [rev](x0) = x0,
    
    [nil] = 2
   orientation:
    rev#(++(x,y)) = 4y + 9 >= 4y + 6 = rev2#(x,y)
    
    rev#(++(x,y)) = 4y + 9 >= y = rev1#(x,y)
    
    rev1#(x,++(y,z)) = 2z + 1 >= z = rev1#(y,z)
    
    rev2#(x,++(y,z)) = 8z + 10 >= 4z + 6 = rev2#(y,z)
    
    rev2#(x,++(y,z)) = 8z + 10 >= 2z + 7 = rev#(rev2(y,z))
    
    rev2#(x,++(y,z)) = 8z + 10 >= 4z + 9 = rev#(++(x,rev(rev2(y,z))))
    
    rev(nil()) = 2 >= 2 = nil()
    
    rev(++(x,y)) = 2y + 1 >= 2y + 1 = ++(rev1(x,y),rev2(x,y))
    
    rev1(x,nil()) = 14 >= x = x
    
    rev1(x,++(y,z)) = 8z + 10 >= 4z + 6 = rev1(y,z)
    
    rev2(x,nil()) = 2 >= 2 = nil()
    
    rev2(x,++(y,z)) = 2z + 1 >= 2z + 1 = rev(++(x,rev(rev2(y,z))))
   problem:
    DPs:
     
    TRS:
     rev(nil()) -> nil()
     rev(++(x,y)) -> ++(rev1(x,y),rev2(x,y))
     rev1(x,nil()) -> x
     rev1(x,++(y,z)) -> rev1(y,z)
     rev2(x,nil()) -> nil()
     rev2(x,++(y,z)) -> rev(++(x,rev(rev2(y,z))))
   Qed