(VAR x y) (RULES \(x,x) -> e /(x,x) -> e .(e,x) -> x .(x,e) -> x \(e,x) -> x /(x,e) -> x .(x,\(x,y)) -> y .(/(y,x),x) -> y \(x,.(x,y)) -> y /(.(y,x),x) -> y /(x,\(y,x)) -> y \(/(x,y),x) -> y ) (COMMENT Example 1 in \cite{D33})