Problem: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) Proof: Complexity Transformation Processor: strict: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [h](x0, x1) = x0 + x1 + 13, [g](x0, x1) = x0 + x1 + 2, [f](x0) = x0 + 6 orientation: g(f(x),y) = x + y + 8 >= x + y + 19 = f(h(x,y)) h(x,y) = x + y + 13 >= x + y + 8 = g(x,f(y)) problem: strict: g(f(x),y) -> f(h(x,y)) weak: h(x,y) -> g(x,f(y)) Matrix Interpretation Processor: dimension: 4 max_matrix: [1 0 0 1] [0 0 0 1] [0 0 0 1] [0 0 0 1] interpretation: [1 0 0 1] [1 0 0 0] [0] [0 0 0 1] [0 0 0 0] [1] [h](x0, x1) = [0 0 0 0]x0 + [0 0 0 1]x1 + [0] [0 0 0 1] [0 0 0 0] [0], [1 0 0 1] [1 0 0 0] [0 0 0 1] [0 0 0 0] [g](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 [0 0 0 1] [0 0 0 0] , [1 0 0 0] [0] [0 0 0 0] [0] [f](x0) = [0 0 0 0]x0 + [0] [0 0 0 1] [1] orientation: [1 0 0 1] [1 0 0 0] [1] [1 0 0 1] [1 0 0 0] [0] [0 0 0 1] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0] g(f(x),y) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = f(h(x,y)) [0 0 0 1] [0 0 0 0] [1] [0 0 0 1] [0 0 0 0] [1] [1 0 0 1] [1 0 0 0] [0] [1 0 0 1] [1 0 0 0] [0 0 0 1] [0 0 0 0] [1] [0 0 0 1] [0 0 0 0] h(x,y) = [0 0 0 0]x + [0 0 0 1]y + [0] >= [0 0 0 0]x + [0 0 0 0]y = g(x,f(y)) [0 0 0 1] [0 0 0 0] [0] [0 0 0 1] [0 0 0 0] problem: strict: weak: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) Qed