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