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