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