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))))
  TDG 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))))
   graph:
    rev1#(x,++(y,z)) -> rev1#(y,z) -> rev1#(x,++(y,z)) -> rev1#(y,z)
    rev2#(x,++(y,z)) -> rev2#(y,z) ->
    rev2#(x,++(y,z)) -> rev#(++(x,rev(rev2(y,z))))
    rev2#(x,++(y,z)) -> rev2#(y,z) ->
    rev2#(x,++(y,z)) -> rev#(rev2(y,z))
    rev2#(x,++(y,z)) -> rev2#(y,z) ->
    rev2#(x,++(y,z)) -> rev2#(y,z)
    rev2#(x,++(y,z)) -> rev#(rev2(y,z)) ->
    rev#(++(x,y)) -> rev1#(x,y)
    rev2#(x,++(y,z)) -> rev#(rev2(y,z)) ->
    rev#(++(x,y)) -> rev2#(x,y)
    rev2#(x,++(y,z)) -> rev#(++(x,rev(rev2(y,z)))) ->
    rev#(++(x,y)) -> rev1#(x,y)
    rev2#(x,++(y,z)) -> rev#(++(x,rev(rev2(y,z)))) ->
    rev#(++(x,y)) -> rev2#(x,y)
    rev#(++(x,y)) -> rev1#(x,y) -> rev1#(x,++(y,z)) -> rev1#(y,z)
    rev#(++(x,y)) -> rev2#(x,y) ->
    rev2#(x,++(y,z)) -> rev#(++(x,rev(rev2(y,z))))
    rev#(++(x,y)) -> rev2#(x,y) -> rev2#(x,++(y,z)) -> rev#(rev2(y,z))
    rev#(++(x,y)) -> rev2#(x,y) -> rev2#(x,++(y,z)) -> rev2#(y,z)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 12/36
    DPs:
     rev2#(x,++(y,z)) -> rev2#(y,z)
     rev2#(x,++(y,z)) -> rev#(rev2(y,z))
     rev#(++(x,y)) -> rev2#(x,y)
     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))))
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
      [rev2#](x0, x1) = [0  -&]x1,
      
      [rev#](x0) = [0  -&]x0 + [0],
      
                       [-& -&]     [0  -&]     [-&]
      [rev2](x0, x1) = [0  0 ]x0 + [1  0 ]x1 + [3 ],
      
                       [0 0]     [0 0]     [-&]
      [rev1](x0, x1) = [0 0]x0 + [0 0]x1 + [0 ],
      
                     [-& -&]     [1  -&]     [0]
      [++](x0, x1) = [0  0 ]x0 + [0  0 ]x1 + [0],
      
                  [0  -&]     [-&]
      [rev](x0) = [0  0 ]x0 + [3 ],
      
              [2]
      [nil] = [1]
     orientation:
      rev2#(x,++(y,z)) = [1  -&]z + [0] >= [0  -&]z = rev2#(y,z)
      
      rev2#(x,++(y,z)) = [1  -&]z + [0] >= [0  -&]z + [0] = rev#(rev2(y,z))
      
      rev#(++(x,y)) = [1  -&]y + [0] >= [0  -&]y = rev2#(x,y)
      
      rev2#(x,++(y,z)) = [1  -&]z + [0] >= [1  -&]z + [0] = rev#(++(x,rev(rev2(y,z))))
      
                   [2]    [2]        
      rev(nil()) = [3] >= [1] = nil()
      
                     [-& -&]    [1  -&]    [0]    [-& -&]    [1  -&]    [0]                          
      rev(++(x,y)) = [0  0 ]x + [1  0 ]y + [3] >= [0  0 ]x + [1  0 ]y + [3] = ++(rev1(x,y),rev2(x,y))
      
                      [0 0]    [2]         
      rev1(x,nil()) = [0 0]x + [2] >= x = x
      
                        [0 0]    [0 0]    [1 0]    [0]    [0 0]    [0 0]    [-&]            
      rev1(x,++(y,z)) = [0 0]x + [0 0]y + [1 0]z + [0] >= [0 0]y + [0 0]z + [0 ] = rev1(y,z)
      
                      [-& -&]    [2]    [2]        
      rev2(x,nil()) = [0  0 ]x + [3] >= [1] = nil()
      
                        [-& -&]    [-& -&]    [1  -&]    [0]    [-& -&]    [-& -&]    [1  -&]    [0]                            
      rev2(x,++(y,z)) = [0  0 ]x + [0  0 ]y + [2  0 ]z + [3] >= [0  0 ]x + [0  0 ]y + [1  0 ]z + [3] = rev(++(x,rev(rev2(y,z))))
     problem:
      DPs:
       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))))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 8/4
      
    
    DPs:
     rev1#(x,++(y,z)) -> rev1#(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))))
    Subterm Criterion Processor:
     simple projection:
      pi(rev1#) = 1
     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