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