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