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))
  ADG 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))
   graph:
    rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> rev#(y)
    rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> ++#(rev(y),rev(x))
    rev#(++(x,y)) -> rev#(x) -> rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> rev#(x) -> rev#(++(x,y)) -> rev#(y)
    rev#(++(x,y)) -> rev#(x) ->
    rev#(++(x,y)) -> ++#(rev(y),rev(x))
    rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
    ++#(++(x,y),z) -> ++#(y,z)
    rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
    ++#(++(x,y),z) -> ++#(x,++(y,z))
    ++#(++(x,y),z) -> ++#(y,z) -> ++#(++(x,y),z) -> ++#(y,z)
    ++#(++(x,y),z) -> ++#(y,z) -> ++#(++(x,y),z) -> ++#(x,++(y,z))
    ++#(++(x,y),z) -> ++#(x,++(y,z)) -> ++#(++(x,y),z) -> ++#(y,z)
    ++#(++(x,y),z) -> ++#(x,++(y,z)) ->
    ++#(++(x,y),z) -> ++#(x,++(y,z))
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y)) ->
    ++#(++(x,y),z) -> ++#(y,z)
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y)) ->
    ++#(++(x,y),z) -> ++#(x,++(y,z))
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y)) ->
    ++#(++(x,y),z) -> ++#(y,z)
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y)) ->
    ++#(++(x,y),z) -> ++#(x,++(y,z))
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(unit(x)) -> flatten#(x) -> flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
   Restore Modifier:
    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))
    SCC Processor:
     #sccs: 3
     #rules: 9
     #arcs: 51/144
     DPs:
      flatten#(++(unit(x),y)) -> flatten#(y)
      flatten#(++(unit(x),y)) -> flatten#(x)
      flatten#(++(x,y)) -> flatten#(x)
      flatten#(++(x,y)) -> flatten#(y)
      flatten#(unit(x)) -> flatten#(x)
     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:
      dimension: 1
      interpretation:
       [flatten#](x0) = x0,
       
       [rev](x0) = x0,
       
       [++](x0, x1) = x0 + x1,
       
       [unit](x0) = x0 + 1,
       
       [flatten](x0) = x0,
       
       [nil] = 0
      orientation:
       flatten#(++(unit(x),y)) = x + y + 1 >= y = flatten#(y)
       
       flatten#(++(unit(x),y)) = x + y + 1 >= x = flatten#(x)
       
       flatten#(++(x,y)) = x + y >= x = flatten#(x)
       
       flatten#(++(x,y)) = x + y >= y = flatten#(y)
       
       flatten#(unit(x)) = x + 1 >= x = flatten#(x)
       
       flatten(nil()) = 0 >= 0 = nil()
       
       flatten(unit(x)) = x + 1 >= x = flatten(x)
       
       flatten(++(x,y)) = x + y >= x + y = ++(flatten(x),flatten(y))
       
       flatten(++(unit(x),y)) = x + y + 1 >= x + y = ++(flatten(x),flatten(y))
       
       flatten(flatten(x)) = x >= x = flatten(x)
       
       rev(nil()) = 0 >= 0 = nil()
       
       rev(unit(x)) = x + 1 >= x + 1 = unit(x)
       
       rev(++(x,y)) = x + y >= x + y = ++(rev(y),rev(x))
       
       rev(rev(x)) = x >= x = x
       
       ++(x,nil()) = x >= x = x
       
       ++(nil(),y) = y >= y = y
       
       ++(++(x,y),z) = x + y + z >= x + y + z = ++(x,++(y,z))
      problem:
       DPs:
        flatten#(++(x,y)) -> flatten#(x)
        flatten#(++(x,y)) -> flatten#(y)
       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:
       dimension: 1
       interpretation:
        [flatten#](x0) = x0,
        
        [rev](x0) = x0,
        
        [++](x0, x1) = x0 + x1 + 1,
        
        [unit](x0) = x0 + 1,
        
        [flatten](x0) = x0,
        
        [nil] = 0
       orientation:
        flatten#(++(x,y)) = x + y + 1 >= x = flatten#(x)
        
        flatten#(++(x,y)) = x + y + 1 >= y = flatten#(y)
        
        flatten(nil()) = 0 >= 0 = nil()
        
        flatten(unit(x)) = x + 1 >= x = flatten(x)
        
        flatten(++(x,y)) = x + y + 1 >= x + y + 1 = ++(flatten(x),flatten(y))
        
        flatten(++(unit(x),y)) = x + y + 2 >= x + y + 1 = ++(flatten(x),flatten(y))
        
        flatten(flatten(x)) = x >= x = flatten(x)
        
        rev(nil()) = 0 >= 0 = nil()
        
        rev(unit(x)) = x + 1 >= x + 1 = unit(x)
        
        rev(++(x,y)) = x + y + 1 >= x + y + 1 = ++(rev(y),rev(x))
        
        rev(rev(x)) = x >= x = x
        
        ++(x,nil()) = x + 1 >= x = x
        
        ++(nil(),y) = y + 1 >= y = y
        
        ++(++(x,y),z) = x + y + z + 2 >= x + y + z + 2 = ++(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
     
     DPs:
      rev#(++(x,y)) -> rev#(y)
      rev#(++(x,y)) -> rev#(x)
     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:
      dimension: 1
      interpretation:
       [rev#](x0) = x0 + 1,
       
       [rev](x0) = x0,
       
       [++](x0, x1) = x0 + x1 + 1,
       
       [unit](x0) = x0 + 1,
       
       [flatten](x0) = x0,
       
       [nil] = 0
      orientation:
       rev#(++(x,y)) = x + y + 2 >= y + 1 = rev#(y)
       
       rev#(++(x,y)) = x + y + 2 >= x + 1 = rev#(x)
       
       flatten(nil()) = 0 >= 0 = nil()
       
       flatten(unit(x)) = x + 1 >= x = flatten(x)
       
       flatten(++(x,y)) = x + y + 1 >= x + y + 1 = ++(flatten(x),flatten(y))
       
       flatten(++(unit(x),y)) = x + y + 2 >= x + y + 1 = ++(flatten(x),flatten(y))
       
       flatten(flatten(x)) = x >= x = flatten(x)
       
       rev(nil()) = 0 >= 0 = nil()
       
       rev(unit(x)) = x + 1 >= x + 1 = unit(x)
       
       rev(++(x,y)) = x + y + 1 >= x + y + 1 = ++(rev(y),rev(x))
       
       rev(rev(x)) = x >= x = x
       
       ++(x,nil()) = x + 1 >= x = x
       
       ++(nil(),y) = y + 1 >= y = y
       
       ++(++(x,y),z) = x + y + z + 2 >= x + y + z + 2 = ++(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
     
     DPs:
      ++#(++(x,y),z) -> ++#(x,++(y,z))
      ++#(++(x,y),z) -> ++#(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:
      dimension: 1
      interpretation:
       [++#](x0, x1) = x0 + 1,
       
       [rev](x0) = x0,
       
       [++](x0, x1) = x0 + x1 + 1,
       
       [unit](x0) = x0,
       
       [flatten](x0) = x0,
       
       [nil] = 0
      orientation:
       ++#(++(x,y),z) = x + y + 2 >= x + 1 = ++#(x,++(y,z))
       
       ++#(++(x,y),z) = x + y + 2 >= y + 1 = ++#(y,z)
       
       flatten(nil()) = 0 >= 0 = nil()
       
       flatten(unit(x)) = x >= x = flatten(x)
       
       flatten(++(x,y)) = x + y + 1 >= x + y + 1 = ++(flatten(x),flatten(y))
       
       flatten(++(unit(x),y)) = x + y + 1 >= x + y + 1 = ++(flatten(x),flatten(y))
       
       flatten(flatten(x)) = x >= x = flatten(x)
       
       rev(nil()) = 0 >= 0 = nil()
       
       rev(unit(x)) = x >= x = unit(x)
       
       rev(++(x,y)) = x + y + 1 >= x + y + 1 = ++(rev(y),rev(x))
       
       rev(rev(x)) = x >= x = x
       
       ++(x,nil()) = x + 1 >= x = x
       
       ++(nil(),y) = y + 1 >= y = y
       
       ++(++(x,y),z) = x + y + z + 2 >= x + y + z + 2 = ++(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