YES(?,O(n^2)) 22.01/9.80 YES(?,O(n^2)) 22.16/9.81 22.16/9.81 Problem: 22.16/9.81 not(true()) -> false() 22.16/9.81 not(false()) -> true() 22.16/9.81 odd(0()) -> false() 22.16/9.81 odd(s(x)) -> not(odd(x)) 22.16/9.81 +(x,0()) -> x 22.16/9.81 +(x,s(y)) -> s(+(x,y)) 22.16/9.81 +(s(x),y) -> s(+(x,y)) 22.16/9.81 22.16/9.81 Proof: 22.16/9.81 Complexity Transformation Processor: 22.16/9.81 strict: 22.16/9.81 not(true()) -> false() 22.16/9.81 not(false()) -> true() 22.16/9.81 odd(0()) -> false() 22.16/9.81 odd(s(x)) -> not(odd(x)) 22.16/9.81 +(x,0()) -> x 22.16/9.81 +(x,s(y)) -> s(+(x,y)) 22.16/9.81 +(s(x),y) -> s(+(x,y)) 22.16/9.81 weak: 22.16/9.81 22.16/9.81 Matrix Interpretation Processor: dim=1 22.16/9.81 22.16/9.81 max_matrix: 22.16/9.81 1 22.16/9.81 interpretation: 22.16/9.81 [+](x0, x1) = x0 + x1 + 4, 22.16/9.81 22.16/9.81 [s](x0) = x0, 22.16/9.81 22.16/9.81 [odd](x0) = x0 + 67, 22.16/9.81 22.16/9.81 [0] = 1, 22.16/9.81 22.16/9.81 [false] = 67, 22.16/9.81 22.16/9.81 [not](x0) = x0 + 237, 22.16/9.81 22.16/9.81 [true] = 49 22.16/9.81 orientation: 22.16/9.81 not(true()) = 286 >= 67 = false() 22.16/9.81 22.16/9.81 not(false()) = 304 >= 49 = true() 22.16/9.81 22.16/9.81 odd(0()) = 68 >= 67 = false() 22.16/9.81 22.16/9.81 odd(s(x)) = x + 67 >= x + 304 = not(odd(x)) 22.16/9.81 22.16/9.81 +(x,0()) = x + 5 >= x = x 22.16/9.81 22.16/9.81 +(x,s(y)) = x + y + 4 >= x + y + 4 = s(+(x,y)) 22.16/9.81 22.16/9.81 +(s(x),y) = x + y + 4 >= x + y + 4 = s(+(x,y)) 22.16/9.81 problem: 22.16/9.81 strict: 22.16/9.81 odd(s(x)) -> not(odd(x)) 22.16/9.81 +(x,s(y)) -> s(+(x,y)) 22.16/9.81 +(s(x),y) -> s(+(x,y)) 22.16/9.81 weak: 22.16/9.81 not(true()) -> false() 22.16/9.81 not(false()) -> true() 22.16/9.81 odd(0()) -> false() 22.16/9.81 +(x,0()) -> x 22.16/9.81 Matrix Interpretation Processor: dim=1 22.16/9.81 22.16/9.81 max_matrix: 22.16/9.81 1 22.16/9.81 interpretation: 22.16/9.81 [+](x0, x1) = x0 + x1, 22.16/9.81 22.16/9.81 [s](x0) = x0 + 213, 22.16/9.81 22.16/9.81 [odd](x0) = x0 + 166, 22.16/9.81 22.16/9.81 [0] = 0, 22.16/9.81 22.16/9.81 [false] = 166, 22.16/9.81 22.16/9.81 [not](x0) = x0, 22.16/9.81 22.16/9.81 [true] = 166 22.16/9.81 orientation: 22.16/9.81 odd(s(x)) = x + 379 >= x + 166 = not(odd(x)) 22.16/9.81 22.16/9.81 +(x,s(y)) = x + y + 213 >= x + y + 213 = s(+(x,y)) 22.16/9.81 22.16/9.81 +(s(x),y) = x + y + 213 >= x + y + 213 = s(+(x,y)) 22.16/9.81 22.16/9.81 not(true()) = 166 >= 166 = false() 22.16/9.81 22.16/9.81 not(false()) = 166 >= 166 = true() 22.16/9.81 22.16/9.81 odd(0()) = 166 >= 166 = false() 22.16/9.81 22.16/9.81 +(x,0()) = x >= x = x 22.16/9.81 problem: 22.16/9.81 strict: 22.16/9.81 +(x,s(y)) -> s(+(x,y)) 22.16/9.81 +(s(x),y) -> s(+(x,y)) 22.16/9.81 weak: 22.16/9.81 odd(s(x)) -> not(odd(x)) 22.16/9.81 not(true()) -> false() 22.16/9.81 not(false()) -> true() 22.16/9.81 odd(0()) -> false() 22.16/9.81 +(x,0()) -> x 22.16/9.81 Splitting Processor: 22.16/9.81 strict: 22.16/9.81 +(s(x),y) -> s(+(x,y)) 22.16/9.81 weak: 22.16/9.81 odd(s(x)) -> not(odd(x)) 22.16/9.81 not(true()) -> false() 22.16/9.81 not(false()) -> true() 22.16/9.81 odd(0()) -> false() 22.16/9.81 +(x,0()) -> x 22.16/9.81 +(x,s(y)) -> s(+(x,y)) 22.16/9.81 Matrix Interpretation Processor: dim=2 22.16/9.81 22.16/9.81 max_matrix: 22.16/9.81 [1 1] 22.16/9.81 [0 1] 22.16/9.81 interpretation: 22.16/9.81 [1 1] 22.16/9.81 [+](x0, x1) = x0 + [0 1]x1, 22.16/9.81 22.16/9.81 [2] 22.16/9.81 [s](x0) = x0 + [1], 22.16/9.81 22.16/9.81 [3] 22.16/9.81 [odd](x0) = x0 + [1], 22.16/9.81 22.16/9.81 [3] 22.16/9.81 [0] = [2], 22.16/9.81 22.16/9.81 [0] 22.16/9.81 [false] = [0], 22.16/9.81 22.16/9.81 22.16/9.81 [not](x0) = x0, 22.16/9.81 22.16/9.81 [0] 22.16/9.81 [true] = [0] 22.16/9.81 orientation: 22.16/9.81 [1 1] [3] [1 1] [2] 22.16/9.81 +(x,s(y)) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y)) 22.16/9.81 22.16/9.81 [1 1] [2] [1 1] [2] 22.16/9.81 +(s(x),y) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y)) 22.16/9.81 22.16/9.81 [5] [3] 22.16/9.81 odd(s(x)) = x + [2] >= x + [1] = not(odd(x)) 22.16/9.81 22.16/9.81 [0] [0] 22.16/9.81 not(true()) = [0] >= [0] = false() 22.16/9.81 22.16/9.81 [0] [0] 22.16/9.81 not(false()) = [0] >= [0] = true() 22.16/9.81 22.16/9.81 [6] [0] 22.16/9.81 odd(0()) = [3] >= [0] = false() 22.16/9.81 22.16/9.81 [5] 22.16/9.81 +(x,0()) = x + [2] >= x = x 22.16/9.81 problem: 22.16/9.81 strict: 22.16/9.81 22.16/9.81 weak: 22.16/9.81 +(x,s(y)) -> s(+(x,y)) 22.16/9.81 +(s(x),y) -> s(+(x,y)) 22.16/9.81 odd(s(x)) -> not(odd(x)) 22.16/9.81 not(true()) -> false() 22.16/9.81 not(false()) -> true() 22.16/9.81 odd(0()) -> false() 22.16/9.81 +(x,0()) -> x 22.16/9.81 Qed 22.16/9.81 22.16/9.81 strict: 22.16/9.81 +(x,s(y)) -> s(+(x,y)) 22.16/9.81 weak: 22.16/9.81 +(s(x),y) -> s(+(x,y)) 22.16/9.81 odd(s(x)) -> not(odd(x)) 22.16/9.81 not(true()) -> false() 22.16/9.81 not(false()) -> true() 22.16/9.81 odd(0()) -> false() 22.16/9.81 +(x,0()) -> x 22.16/9.81 Matrix Interpretation Processor: dim=2 22.16/9.81 22.16/9.81 max_matrix: 22.16/9.81 [1 2] 22.16/9.81 [0 1] 22.16/9.81 interpretation: 22.16/9.81 [1 1] [1 2] [0] 22.16/9.81 [+](x0, x1) = [0 1]x0 + [0 1]x1 + [2], 22.16/9.81 22.16/9.81 [0] 22.16/9.81 [s](x0) = x0 + [1], 22.16/9.81 22.16/9.81 [1 2] [2] 22.16/9.81 [odd](x0) = [0 0]x0 + [0], 22.16/9.81 22.16/9.81 [2] 22.16/9.81 [0] = [3], 22.16/9.81 22.16/9.81 [2] 22.16/9.81 [false] = [0], 22.16/9.81 22.16/9.81 [1 2] [1] 22.16/9.81 [not](x0) = [0 0]x0 + [0], 22.16/9.81 22.16/9.81 [2] 22.16/9.81 [true] = [0] 22.16/9.81 orientation: 22.16/9.81 [1 1] [1 2] [1] [1 1] [1 2] [0] 22.16/9.81 +(s(x),y) = [0 1]x + [0 1]y + [3] >= [0 1]x + [0 1]y + [3] = s(+(x,y)) 22.16/9.81 22.16/9.81 [1 2] [4] [1 2] [3] 22.16/9.81 odd(s(x)) = [0 0]x + [0] >= [0 0]x + [0] = not(odd(x)) 22.16/9.81 22.16/9.81 [3] [2] 22.16/9.81 not(true()) = [0] >= [0] = false() 22.16/9.81 22.16/9.81 [3] [2] 22.16/9.81 not(false()) = [0] >= [0] = true() 22.16/9.81 22.16/9.81 [10] [2] 22.16/9.81 odd(0()) = [0 ] >= [0] = false() 22.16/9.81 22.16/9.81 [1 1] [8] 22.16/9.81 +(x,0()) = [0 1]x + [5] >= x = x 22.16/9.81 22.16/9.81 [1 1] [1 2] [2] [1 1] [1 2] [0] 22.16/9.81 +(x,s(y)) = [0 1]x + [0 1]y + [3] >= [0 1]x + [0 1]y + [3] = s(+(x,y)) 22.16/9.81 problem: 22.16/9.81 strict: 22.16/9.81 22.16/9.81 weak: 22.16/9.81 +(s(x),y) -> s(+(x,y)) 22.16/9.81 odd(s(x)) -> not(odd(x)) 22.16/9.81 not(true()) -> false() 22.16/9.81 not(false()) -> true() 22.16/9.81 odd(0()) -> false() 22.16/9.81 +(x,0()) -> x 22.16/9.81 +(x,s(y)) -> s(+(x,y)) 22.16/9.81 Qed 22.16/9.82 EOF