MAYBE Problem: f(g(x)) -> g(g(f(x))) f(g(x)) -> g(g(g(x))) Proof: RT Transformation Processor: strict: f(g(x)) -> g(g(f(x))) f(g(x)) -> g(g(g(x))) weak: Matrix Interpretation Processor: dimension: 1 interpretation: [f](x0) = x0 + 19, [g](x0) = x0 + 8 orientation: f(g(x)) = x + 27 >= x + 35 = g(g(f(x))) f(g(x)) = x + 27 >= x + 24 = g(g(g(x))) problem: strict: f(g(x)) -> g(g(f(x))) weak: f(g(x)) -> g(g(g(x))) Open