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