YES(?,O(n^2)) 59.30/19.51 YES(?,O(n^2)) 59.30/19.52 59.30/19.52 Problem: 59.30/19.52 a(a(x1)) -> d(c(x1)) 59.30/19.52 a(b(x1)) -> c(c(c(x1))) 59.30/19.52 b(b(x1)) -> a(c(c(x1))) 59.30/19.52 c(c(x1)) -> b(x1) 59.30/19.52 c(d(x1)) -> a(a(x1)) 59.30/19.52 d(d(x1)) -> b(a(c(x1))) 59.30/19.52 59.30/19.52 Proof: 59.30/19.52 Complexity Transformation Processor: 59.30/19.52 strict: 59.30/19.52 a(a(x1)) -> d(c(x1)) 59.30/19.52 a(b(x1)) -> c(c(c(x1))) 59.30/19.52 b(b(x1)) -> a(c(c(x1))) 59.30/19.52 c(c(x1)) -> b(x1) 59.30/19.52 c(d(x1)) -> a(a(x1)) 59.30/19.52 d(d(x1)) -> b(a(c(x1))) 59.30/19.52 weak: 59.30/19.52 59.30/19.52 Matrix Interpretation Processor: dim=1 59.30/19.52 59.30/19.52 max_matrix: 59.30/19.52 1 59.30/19.52 interpretation: 59.30/19.52 [b](x0) = x0 + 162, 59.30/19.52 59.30/19.52 [d](x0) = x0 + 16, 59.30/19.52 59.30/19.52 [c](x0) = x0 + 137, 59.30/19.52 59.30/19.52 [a](x0) = x0 + 120 59.30/19.52 orientation: 59.30/19.52 a(a(x1)) = x1 + 240 >= x1 + 153 = d(c(x1)) 59.30/19.52 59.30/19.52 a(b(x1)) = x1 + 282 >= x1 + 411 = c(c(c(x1))) 59.30/19.52 59.30/19.52 b(b(x1)) = x1 + 324 >= x1 + 394 = a(c(c(x1))) 59.30/19.52 59.30/19.52 c(c(x1)) = x1 + 274 >= x1 + 162 = b(x1) 59.30/19.52 59.30/19.52 c(d(x1)) = x1 + 153 >= x1 + 240 = a(a(x1)) 59.30/19.52 59.30/19.52 d(d(x1)) = x1 + 32 >= x1 + 419 = b(a(c(x1))) 59.30/19.52 problem: 59.30/19.52 strict: 59.30/19.52 a(b(x1)) -> c(c(c(x1))) 59.30/19.52 b(b(x1)) -> a(c(c(x1))) 59.30/19.52 c(d(x1)) -> a(a(x1)) 59.30/19.52 d(d(x1)) -> b(a(c(x1))) 59.30/19.52 weak: 59.30/19.52 a(a(x1)) -> d(c(x1)) 59.30/19.52 c(c(x1)) -> b(x1) 59.30/19.52 Matrix Interpretation Processor: dim=1 59.30/19.52 59.30/19.52 max_matrix: 59.30/19.52 1 59.30/19.52 interpretation: 59.30/19.52 [b](x0) = x0, 59.30/19.52 59.30/19.52 [d](x0) = x0 + 195, 59.30/19.52 59.30/19.52 [c](x0) = x0 + 129, 59.30/19.52 59.30/19.52 [a](x0) = x0 + 162 59.30/19.52 orientation: 59.30/19.52 a(b(x1)) = x1 + 162 >= x1 + 387 = c(c(c(x1))) 59.30/19.52 59.30/19.52 b(b(x1)) = x1 >= x1 + 420 = a(c(c(x1))) 59.30/19.52 59.30/19.52 c(d(x1)) = x1 + 324 >= x1 + 324 = a(a(x1)) 59.30/19.52 59.30/19.52 d(d(x1)) = x1 + 390 >= x1 + 291 = b(a(c(x1))) 59.30/19.52 59.30/19.52 a(a(x1)) = x1 + 324 >= x1 + 324 = d(c(x1)) 59.30/19.52 59.30/19.52 c(c(x1)) = x1 + 258 >= x1 = b(x1) 59.30/19.52 problem: 59.30/19.52 strict: 59.30/19.52 a(b(x1)) -> c(c(c(x1))) 59.30/19.52 b(b(x1)) -> a(c(c(x1))) 59.30/19.52 c(d(x1)) -> a(a(x1)) 59.30/19.52 weak: 59.30/19.52 d(d(x1)) -> b(a(c(x1))) 59.30/19.52 a(a(x1)) -> d(c(x1)) 59.30/19.52 c(c(x1)) -> b(x1) 59.30/19.52 Matrix Interpretation Processor: dim=1 59.30/19.52 59.30/19.52 max_matrix: 59.30/19.52 1 59.30/19.52 interpretation: 59.30/19.52 [b](x0) = x0 + 72, 59.30/19.52 59.30/19.52 [d](x0) = x0 + 128, 59.30/19.52 59.30/19.52 [c](x0) = x0 + 36, 59.30/19.52 59.30/19.52 [a](x0) = x0 + 98 59.30/19.52 orientation: 59.30/19.52 a(b(x1)) = x1 + 170 >= x1 + 108 = c(c(c(x1))) 59.30/19.52 59.30/19.52 b(b(x1)) = x1 + 144 >= x1 + 170 = a(c(c(x1))) 59.30/19.52 59.30/19.52 c(d(x1)) = x1 + 164 >= x1 + 196 = a(a(x1)) 59.30/19.52 59.30/19.52 d(d(x1)) = x1 + 256 >= x1 + 206 = b(a(c(x1))) 59.30/19.52 59.30/19.52 a(a(x1)) = x1 + 196 >= x1 + 164 = d(c(x1)) 59.30/19.52 59.30/19.52 c(c(x1)) = x1 + 72 >= x1 + 72 = b(x1) 59.30/19.52 problem: 59.30/19.52 strict: 59.30/19.52 b(b(x1)) -> a(c(c(x1))) 59.30/19.52 c(d(x1)) -> a(a(x1)) 59.30/19.52 weak: 59.30/19.52 a(b(x1)) -> c(c(c(x1))) 59.30/19.52 d(d(x1)) -> b(a(c(x1))) 59.30/19.52 a(a(x1)) -> d(c(x1)) 59.30/19.52 c(c(x1)) -> b(x1) 59.30/19.52 Matrix Interpretation Processor: dim=1 59.30/19.52 59.30/19.52 max_matrix: 59.30/19.52 1 59.30/19.52 interpretation: 59.30/19.52 [b](x0) = x0 + 6, 59.30/19.52 59.30/19.52 [d](x0) = x0 + 7, 59.30/19.52 59.30/19.52 [c](x0) = x0 + 3, 59.30/19.52 59.30/19.52 [a](x0) = x0 + 5 59.30/19.52 orientation: 59.30/19.52 b(b(x1)) = x1 + 12 >= x1 + 11 = a(c(c(x1))) 59.30/19.52 59.30/19.52 c(d(x1)) = x1 + 10 >= x1 + 10 = a(a(x1)) 59.30/19.52 59.30/19.52 a(b(x1)) = x1 + 11 >= x1 + 9 = c(c(c(x1))) 59.30/19.52 59.30/19.52 d(d(x1)) = x1 + 14 >= x1 + 14 = b(a(c(x1))) 59.30/19.52 59.30/19.52 a(a(x1)) = x1 + 10 >= x1 + 10 = d(c(x1)) 59.30/19.52 59.30/19.52 c(c(x1)) = x1 + 6 >= x1 + 6 = b(x1) 59.30/19.52 problem: 59.30/19.52 strict: 59.30/19.52 c(d(x1)) -> a(a(x1)) 59.30/19.52 weak: 59.30/19.52 b(b(x1)) -> a(c(c(x1))) 59.30/19.52 a(b(x1)) -> c(c(c(x1))) 59.30/19.52 d(d(x1)) -> b(a(c(x1))) 59.30/19.52 a(a(x1)) -> d(c(x1)) 59.30/19.52 c(c(x1)) -> b(x1) 59.30/19.52 Matrix Interpretation Processor: dim=2 59.30/19.52 59.30/19.52 max_matrix: 59.30/19.52 [1 7] 59.30/19.52 [0 1] 59.30/19.52 interpretation: 59.30/19.52 [1 6] [2] 59.30/19.52 [b](x0) = [0 1]x0 + [2], 59.30/19.52 59.30/19.52 [1 7] [2] 59.30/19.52 [d](x0) = [0 1]x0 + [3], 59.30/19.52 59.30/19.52 [1 3] [0] 59.30/19.52 [c](x0) = [0 1]x0 + [1], 59.30/19.52 59.30/19.52 [1 5] [0] 59.30/19.52 [a](x0) = [0 1]x0 + [2] 59.30/19.52 orientation: 59.30/19.52 [1 10] [11] [1 10] [10] 59.30/19.52 c(d(x1)) = [0 1 ]x1 + [4 ] >= [0 1 ]x1 + [4 ] = a(a(x1)) 59.30/19.52 59.30/19.52 [1 12] [16] [1 11] [13] 59.30/19.52 b(b(x1)) = [0 1 ]x1 + [4 ] >= [0 1 ]x1 + [4 ] = a(c(c(x1))) 59.30/19.52 59.30/19.52 [1 11] [12] [1 9] [9] 59.30/19.52 a(b(x1)) = [0 1 ]x1 + [4 ] >= [0 1]x1 + [3] = c(c(c(x1))) 59.30/19.52 59.30/19.52 [1 14] [25] [1 14] [25] 59.30/19.52 d(d(x1)) = [0 1 ]x1 + [6 ] >= [0 1 ]x1 + [5 ] = b(a(c(x1))) 59.30/19.52 59.30/19.52 [1 10] [10] [1 10] [9] 59.30/19.52 a(a(x1)) = [0 1 ]x1 + [4 ] >= [0 1 ]x1 + [4] = d(c(x1)) 59.30/19.52 59.30/19.52 [1 6] [3] [1 6] [2] 59.30/19.52 c(c(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = b(x1) 59.30/19.52 problem: 59.30/19.52 strict: 59.30/19.52 59.30/19.52 weak: 59.30/19.52 c(d(x1)) -> a(a(x1)) 59.30/19.52 b(b(x1)) -> a(c(c(x1))) 59.30/19.52 a(b(x1)) -> c(c(c(x1))) 59.30/19.52 d(d(x1)) -> b(a(c(x1))) 59.30/19.52 a(a(x1)) -> d(c(x1)) 59.30/19.52 c(c(x1)) -> b(x1) 59.30/19.52 Qed 59.30/19.52 EOF