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