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