MAYBE Problem: f(a(),f(b(),x)) -> f(b(),f(a(),x)) f(b(),f(c(),x)) -> f(c(),f(b(),x)) f(c(),f(a(),x)) -> f(a(),f(c(),x)) Proof: RT Transformation Processor: strict: f(a(),f(b(),x)) -> f(b(),f(a(),x)) f(b(),f(c(),x)) -> f(c(),f(b(),x)) f(c(),f(a(),x)) -> f(a(),f(c(),x)) weak: Open