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))
  KBO Processor:
   argument filtering:
    pi(nil) = []
    pi(flatten) = 0
    pi(unit) = [0]
    pi(++) = [0,1]
    pi(rev) = [0]
    pi(flatten#) = 0
    pi(++#) = [0,1]
    pi(rev#) = 0
   usable rules:
    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))
   weight function:
    w0 = 1
    w(++#) = w(flatten#) = w(++) = w(unit) = w(nil) = 1
    w(rev#) = w(rev) = w(flatten) = 0
   precedence:
    flatten# > rev > ++ > rev# ~ ++# ~ unit ~ flatten ~ nil
   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