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