(VAR x y z) (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)) ) (COMMENT Example 2.42 (Flattening and Reverse Operation) in \cite{SK90})