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