YES 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)) max/plus interpretations on N: flatten_A(x1) = max{7, 2 + x1} flatten#_A(x1) = max{0, 1 + x1} nil_A = 8 nil#_A = 6 unit_A(x1) = max{1, 1 + x1} unit#_A(x1) = max{6, 7} ++_A(x1,x2) = max{4, x1, x2} ++#_A(x1,x2) = max{3, -1, 3} rev_A(x1) = max{6, 1 + x1} rev#_A(x1) = max{4, 5} precedence: flatten > unit = ++ > rev > nil