MAYBE Problem: c() -> f(g(c())) f(g(X)) -> g(X) Proof: RT Transformation Processor: strict: c() -> f(g(c())) f(g(X)) -> g(X) weak: Matrix Interpretation Processor: dimension: 1 interpretation: [f](x0) = x0 + 29, [g](x0) = x0, [c] = 0 orientation: c() = 0 >= 29 = f(g(c())) f(g(X)) = X + 29 >= X = g(X) problem: strict: c() -> f(g(c())) weak: f(g(X)) -> g(X) Open