(VAR x y z) (RULES f(nil) -> nil f(.(nil,y)) -> .(nil,f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil) -> nil g(.(x,nil)) -> .(g(x),nil) g(.(x,.(y,z))) -> g(.(.(x,y),z)) ) (COMMENT Example 4.30 (Binary Trees) in \cite{SK90})