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:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {5,4,3}
   transitions:
    unit1(2) -> 4*
    unit1(1) -> 4*
    nil1() -> 4,3
    flatten1(2) -> 3*
    flatten1(1) -> 3*
    flatten0(2) -> 3*
    flatten0(1) -> 3*
    nil0() -> 1*
    unit0(2) -> 2*
    unit0(1) -> 2*
    ++0(1,2) -> 5*
    ++0(2,1) -> 5*
    ++0(1,1) -> 5*
    ++0(2,2) -> 5*
    rev0(2) -> 4*
    rev0(1) -> 4*
    1 -> 5*
    2 -> 5*
  problem:
   
  Qed