MAYBE Problem: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) Proof: Complexity Transformation Processor: strict: d(0()) -> 0() d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [sup](x0, x1) = x0 + x1 + 1, [e](x0, x1) = x0 + x1, [s](x0) = x0, [d](x0) = x0 + 1, [0] = 0 orientation: d(0()) = 1 >= 0 = 0() d(s(x)) = x + 1 >= x + 1 = s(s(d(x))) e(s(x),y) = x + y >= x + y + 1 = e(x,d(y)) sup(s(x),e(0(),y)) = x + y + 1 >= x + y + 1 = sup(x,e(y,s(0()))) problem: strict: d(s(x)) -> s(s(d(x))) e(s(x),y) -> e(x,d(y)) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) weak: d(0()) -> 0() Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [sup](x0, x1) = x0 + x1 + 1, [e](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [d](x0) = x0, [0] = 1 orientation: d(s(x)) = x + 1 >= x + 2 = s(s(d(x))) e(s(x),y) = x + y + 1 >= x + y = e(x,d(y)) sup(s(x),e(0(),y)) = x + y + 3 >= x + y + 3 = sup(x,e(y,s(0()))) d(0()) = 1 >= 1 = 0() problem: strict: d(s(x)) -> s(s(d(x))) sup(s(x),e(0(),y)) -> sup(x,e(y,s(0()))) weak: e(s(x),y) -> e(x,d(y)) d(0()) -> 0() Open