YES(?,O(n^2)) 20.80/6.76 YES(?,O(n^2)) 20.80/6.77 20.80/6.77 Problem: 20.80/6.77 b(c(x1)) -> a(x1) 20.80/6.77 b(b(x1)) -> a(c(x1)) 20.80/6.77 a(x1) -> c(b(x1)) 20.80/6.77 c(c(c(x1))) -> b(x1) 20.80/6.77 20.80/6.77 Proof: 20.80/6.77 Complexity Transformation Processor: 20.80/6.77 strict: 20.80/6.77 b(c(x1)) -> a(x1) 20.80/6.77 b(b(x1)) -> a(c(x1)) 20.80/6.77 a(x1) -> c(b(x1)) 20.80/6.77 c(c(c(x1))) -> b(x1) 20.80/6.77 weak: 20.80/6.77 20.80/6.77 Matrix Interpretation Processor: dim=1 20.80/6.77 20.80/6.77 max_matrix: 20.80/6.77 1 20.80/6.77 interpretation: 20.80/6.77 [a](x0) = x0 + 64, 20.80/6.77 20.80/6.77 [b](x0) = x0 + 49, 20.80/6.77 20.80/6.77 [c](x0) = x0 + 96 20.80/6.77 orientation: 20.80/6.77 b(c(x1)) = x1 + 145 >= x1 + 64 = a(x1) 20.80/6.77 20.80/6.77 b(b(x1)) = x1 + 98 >= x1 + 160 = a(c(x1)) 20.80/6.77 20.80/6.77 a(x1) = x1 + 64 >= x1 + 145 = c(b(x1)) 20.80/6.77 20.80/6.77 c(c(c(x1))) = x1 + 288 >= x1 + 49 = b(x1) 20.80/6.77 problem: 20.80/6.77 strict: 20.80/6.77 b(b(x1)) -> a(c(x1)) 20.80/6.77 a(x1) -> c(b(x1)) 20.80/6.77 weak: 20.80/6.77 b(c(x1)) -> a(x1) 20.80/6.77 c(c(c(x1))) -> b(x1) 20.80/6.77 Matrix Interpretation Processor: dim=1 20.80/6.77 20.80/6.77 max_matrix: 20.80/6.77 1 20.80/6.77 interpretation: 20.80/6.77 [a](x0) = x0, 20.80/6.77 20.80/6.77 [b](x0) = x0 + 162, 20.80/6.77 20.80/6.77 [c](x0) = x0 + 96 20.80/6.77 orientation: 20.80/6.77 b(b(x1)) = x1 + 324 >= x1 + 96 = a(c(x1)) 20.80/6.77 20.80/6.77 a(x1) = x1 >= x1 + 258 = c(b(x1)) 20.80/6.77 20.80/6.77 b(c(x1)) = x1 + 258 >= x1 = a(x1) 20.80/6.77 20.80/6.77 c(c(c(x1))) = x1 + 288 >= x1 + 162 = b(x1) 20.80/6.77 problem: 20.80/6.77 strict: 20.80/6.77 a(x1) -> c(b(x1)) 20.80/6.77 weak: 20.80/6.77 b(b(x1)) -> a(c(x1)) 20.80/6.77 b(c(x1)) -> a(x1) 20.80/6.77 c(c(c(x1))) -> b(x1) 20.80/6.77 Matrix Interpretation Processor: dim=2 20.80/6.77 20.80/6.77 max_matrix: 20.80/6.77 [1 4] 20.80/6.77 [0 1] 20.80/6.77 interpretation: 20.80/6.77 [1 4] [6] 20.80/6.77 [a](x0) = [0 1]x0 + [6], 20.80/6.77 20.80/6.77 [1 3] [1] 20.80/6.77 [b](x0) = [0 1]x0 + [4], 20.80/6.77 20.80/6.77 [1 1] [0] 20.80/6.77 [c](x0) = [0 1]x0 + [2] 20.80/6.77 orientation: 20.80/6.77 [1 4] [6] [1 4] [5] 20.80/6.77 a(x1) = [0 1]x1 + [6] >= [0 1]x1 + [6] = c(b(x1)) 20.80/6.77 20.80/6.77 [1 6] [14] [1 5] [14] 20.80/6.77 b(b(x1)) = [0 1]x1 + [8 ] >= [0 1]x1 + [8 ] = a(c(x1)) 20.80/6.77 20.80/6.77 [1 4] [7] [1 4] [6] 20.80/6.77 b(c(x1)) = [0 1]x1 + [6] >= [0 1]x1 + [6] = a(x1) 20.80/6.77 20.80/6.77 [1 3] [6] [1 3] [1] 20.80/6.77 c(c(c(x1))) = [0 1]x1 + [6] >= [0 1]x1 + [4] = b(x1) 20.80/6.77 problem: 20.80/6.77 strict: 20.80/6.77 20.80/6.77 weak: 20.80/6.77 a(x1) -> c(b(x1)) 20.80/6.77 b(b(x1)) -> a(c(x1)) 20.80/6.77 b(c(x1)) -> a(x1) 20.80/6.77 c(c(c(x1))) -> b(x1) 20.80/6.77 Qed 20.80/6.77 EOF