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