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