YES(?,O(n^2)) 7.99/5.84 YES(?,O(n^2)) 7.99/5.85 7.99/5.85 Problem: 7.99/5.85 +(x,0()) -> x 7.99/5.85 +(x,s(y)) -> s(+(x,y)) 7.99/5.85 +(0(),s(y)) -> s(y) 7.99/5.85 s(+(0(),y)) -> s(y) 7.99/5.85 7.99/5.85 Proof: 7.99/5.85 Complexity Transformation Processor: 7.99/5.85 strict: 7.99/5.85 +(x,0()) -> x 7.99/5.85 +(x,s(y)) -> s(+(x,y)) 7.99/5.85 +(0(),s(y)) -> s(y) 7.99/5.85 s(+(0(),y)) -> s(y) 7.99/5.85 weak: 7.99/5.85 7.99/5.85 Matrix Interpretation Processor: dim=1 7.99/5.85 7.99/5.85 max_matrix: 7.99/5.85 1 7.99/5.85 interpretation: 7.99/5.85 [s](x0) = x0 + 96, 7.99/5.85 7.99/5.85 [+](x0, x1) = x0 + x1 + 48, 7.99/5.85 7.99/5.85 [0] = 225 7.99/5.85 orientation: 7.99/5.85 +(x,0()) = x + 273 >= x = x 7.99/5.85 7.99/5.85 +(x,s(y)) = x + y + 144 >= x + y + 144 = s(+(x,y)) 7.99/5.85 7.99/5.85 +(0(),s(y)) = y + 369 >= y + 96 = s(y) 7.99/5.85 7.99/5.85 s(+(0(),y)) = y + 369 >= y + 96 = s(y) 7.99/5.85 problem: 7.99/5.85 strict: 7.99/5.85 +(x,s(y)) -> s(+(x,y)) 7.99/5.85 weak: 7.99/5.85 +(x,0()) -> x 7.99/5.85 +(0(),s(y)) -> s(y) 7.99/5.85 s(+(0(),y)) -> s(y) 7.99/5.85 Matrix Interpretation Processor: dim=2 7.99/5.85 7.99/5.85 max_matrix: 7.99/5.85 [1 1] 7.99/5.85 [0 1] 7.99/5.85 interpretation: 7.99/5.85 [4] 7.99/5.85 [s](x0) = x0 + [5], 7.99/5.85 7.99/5.85 [1 1] [4] 7.99/5.85 [+](x0, x1) = x0 + [0 1]x1 + [2], 7.99/5.85 7.99/5.85 [2] 7.99/5.85 [0] = [0] 7.99/5.85 orientation: 7.99/5.85 [1 1] [13] [1 1] [8] 7.99/5.85 +(x,s(y)) = x + [0 1]y + [7 ] >= x + [0 1]y + [7] = s(+(x,y)) 7.99/5.85 7.99/5.85 [6] 7.99/5.85 +(x,0()) = x + [2] >= x = x 7.99/5.85 7.99/5.85 [1 1] [15] [4] 7.99/5.85 +(0(),s(y)) = [0 1]y + [7 ] >= y + [5] = s(y) 7.99/5.85 7.99/5.85 [1 1] [10] [4] 7.99/5.85 s(+(0(),y)) = [0 1]y + [7 ] >= y + [5] = s(y) 7.99/5.85 problem: 7.99/5.85 strict: 7.99/5.85 7.99/5.85 weak: 7.99/5.85 +(x,s(y)) -> s(+(x,y)) 7.99/5.85 +(x,0()) -> x 7.99/5.85 +(0(),s(y)) -> s(y) 7.99/5.85 s(+(0(),y)) -> s(y) 7.99/5.85 Qed 7.99/5.85 EOF