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