MAYBE Problem: f(a(),f(a(),x)) -> f(c(),f(b(),x)) f(b(),f(b(),x)) -> f(a(),f(c(),x)) f(c(),f(c(),x)) -> f(b(),f(a(),x)) Proof: Complexity Transformation Processor: strict: f(a(),f(a(),x)) -> f(c(),f(b(),x)) f(b(),f(b(),x)) -> f(a(),f(c(),x)) f(c(),f(c(),x)) -> f(b(),f(a(),x)) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [b] = 0, [c] = 1, [f](x0, x1) = x0 + x1, [a] = 0 orientation: f(a(),f(a(),x)) = x >= x + 1 = f(c(),f(b(),x)) f(b(),f(b(),x)) = x >= x + 1 = f(a(),f(c(),x)) f(c(),f(c(),x)) = x + 2 >= x = f(b(),f(a(),x)) problem: strict: f(a(),f(a(),x)) -> f(c(),f(b(),x)) f(b(),f(b(),x)) -> f(a(),f(c(),x)) weak: f(c(),f(c(),x)) -> f(b(),f(a(),x)) Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [b] = 1, [c] = 1, [f](x0, x1) = x0 + x1, [a] = 0 orientation: f(a(),f(a(),x)) = x >= x + 2 = f(c(),f(b(),x)) f(b(),f(b(),x)) = x + 2 >= x + 1 = f(a(),f(c(),x)) f(c(),f(c(),x)) = x + 2 >= x + 1 = f(b(),f(a(),x)) problem: strict: f(a(),f(a(),x)) -> f(c(),f(b(),x)) weak: f(b(),f(b(),x)) -> f(a(),f(c(),x)) f(c(),f(c(),x)) -> f(b(),f(a(),x)) Open