YES

Problem:
 flatten(nil()) -> nil()
 flatten(unit(x)) -> flatten(x)
 flatten(++(x,y)) -> ++(flatten(x),flatten(y))
 flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
 flatten(flatten(x)) -> flatten(x)
 rev(nil()) -> nil()
 rev(unit(x)) -> unit(x)
 rev(++(x,y)) -> ++(rev(y),rev(x))
 rev(rev(x)) -> x
 ++(x,nil()) -> x
 ++(nil(),y) -> y
 ++(++(x,y),z) -> ++(x,++(y,z))

Proof:
 DP Processor:
  DPs:
   flatten#(unit(x)) -> flatten#(x)
   flatten#(++(x,y)) -> flatten#(y)
   flatten#(++(x,y)) -> flatten#(x)
   flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
   flatten#(++(unit(x),y)) -> flatten#(y)
   flatten#(++(unit(x),y)) -> flatten#(x)
   flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
   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,z))
  TRS:
   flatten(nil()) -> nil()
   flatten(unit(x)) -> flatten(x)
   flatten(++(x,y)) -> ++(flatten(x),flatten(y))
   flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
   flatten(flatten(x)) -> flatten(x)
   rev(nil()) -> nil()
   rev(unit(x)) -> unit(x)
   rev(++(x,y)) -> ++(rev(y),rev(x))
   rev(rev(x)) -> x
   ++(x,nil()) -> x
   ++(nil(),y) -> y
   ++(++(x,y),z) -> ++(x,++(y,z))
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [rev#](x0) = 2x0,
    
    [++#](x0, x1) = x0 + 4,
    
    [flatten#](x0) = x0 + 4,
    
    [rev](x0) = 2x0,
    
    [++](x0, x1) = x0 + x1 + 3,
    
    [unit](x0) = x0 + 3,
    
    [flatten](x0) = x0,
    
    [nil] = 0
   orientation:
    flatten#(unit(x)) = x + 7 >= x + 4 = flatten#(x)
    
    flatten#(++(x,y)) = x + y + 7 >= y + 4 = flatten#(y)
    
    flatten#(++(x,y)) = x + y + 7 >= x + 4 = flatten#(x)
    
    flatten#(++(x,y)) = x + y + 7 >= x + 4 = ++#(flatten(x),flatten(y))
    
    flatten#(++(unit(x),y)) = x + y + 10 >= y + 4 = flatten#(y)
    
    flatten#(++(unit(x),y)) = x + y + 10 >= x + 4 = flatten#(x)
    
    flatten#(++(unit(x),y)) = x + y + 10 >= x + 4 = ++#(flatten(x),flatten(y))
    
    rev#(++(x,y)) = 2x + 2y + 6 >= 2x = rev#(x)
    
    rev#(++(x,y)) = 2x + 2y + 6 >= 2y = rev#(y)
    
    rev#(++(x,y)) = 2x + 2y + 6 >= 2y + 4 = ++#(rev(y),rev(x))
    
    ++#(++(x,y),z) = x + y + 7 >= y + 4 = ++#(y,z)
    
    ++#(++(x,y),z) = x + y + 7 >= x + 4 = ++#(x,++(y,z))
    
    flatten(nil()) = 0 >= 0 = nil()
    
    flatten(unit(x)) = x + 3 >= x = flatten(x)
    
    flatten(++(x,y)) = x + y + 3 >= x + y + 3 = ++(flatten(x),flatten(y))
    
    flatten(++(unit(x),y)) = x + y + 6 >= x + y + 3 = ++(flatten(x),flatten(y))
    
    flatten(flatten(x)) = x >= x = flatten(x)
    
    rev(nil()) = 0 >= 0 = nil()
    
    rev(unit(x)) = 2x + 6 >= x + 3 = unit(x)
    
    rev(++(x,y)) = 2x + 2y + 6 >= 2x + 2y + 3 = ++(rev(y),rev(x))
    
    rev(rev(x)) = 4x >= x = x
    
    ++(x,nil()) = x + 3 >= x = x
    
    ++(nil(),y) = y + 3 >= y = y
    
    ++(++(x,y),z) = x + y + z + 6 >= x + y + z + 6 = ++(x,++(y,z))
   problem:
    DPs:
     
    TRS:
     flatten(nil()) -> nil()
     flatten(unit(x)) -> flatten(x)
     flatten(++(x,y)) -> ++(flatten(x),flatten(y))
     flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
     flatten(flatten(x)) -> flatten(x)
     rev(nil()) -> nil()
     rev(unit(x)) -> unit(x)
     rev(++(x,y)) -> ++(rev(y),rev(x))
     rev(rev(x)) -> x
     ++(x,nil()) -> x
     ++(nil(),y) -> y
     ++(++(x,y),z) -> ++(x,++(y,z))
   Qed