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