YES(?,O(n^4)) 1173.50/295.38 YES(?,O(n^4)) 1173.50/295.39 1173.50/295.39 Problem: 1173.50/295.39 C(x1) -> c(x1) 1173.50/295.39 c(c(x1)) -> x1 1173.50/295.39 b(b(x1)) -> B(x1) 1173.50/295.39 B(B(x1)) -> b(x1) 1173.50/295.39 c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 b(B(x1)) -> x1 1173.50/295.39 B(b(x1)) -> x1 1173.50/295.39 c(C(x1)) -> x1 1173.50/295.39 C(c(x1)) -> x1 1173.50/295.39 1173.50/295.39 Proof: 1173.50/295.39 Complexity Transformation Processor: 1173.50/295.39 strict: 1173.50/295.39 C(x1) -> c(x1) 1173.50/295.39 c(c(x1)) -> x1 1173.50/295.39 b(b(x1)) -> B(x1) 1173.50/295.39 B(B(x1)) -> b(x1) 1173.50/295.39 c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 b(B(x1)) -> x1 1173.50/295.39 B(b(x1)) -> x1 1173.50/295.39 c(C(x1)) -> x1 1173.50/295.39 C(c(x1)) -> x1 1173.50/295.39 weak: 1173.50/295.39 1173.50/295.39 Matrix Interpretation Processor: dim=1 1173.50/295.39 1173.50/295.39 max_matrix: 1173.50/295.39 1 1173.50/295.39 interpretation: 1173.50/295.39 [B](x0) = x0, 1173.50/295.39 1173.50/295.39 [b](x0) = x0 + 7, 1173.50/295.39 1173.50/295.39 [c](x0) = x0 + 1, 1173.50/295.39 1173.50/295.39 [C](x0) = x0 1173.50/295.39 orientation: 1173.50/295.39 C(x1) = x1 >= x1 + 1 = c(x1) 1173.50/295.39 1173.50/295.39 c(c(x1)) = x1 + 2 >= x1 = x1 1173.50/295.39 1173.50/295.39 b(b(x1)) = x1 + 14 >= x1 = B(x1) 1173.50/295.39 1173.50/295.39 B(B(x1)) = x1 >= x1 + 7 = b(x1) 1173.50/295.39 1173.50/295.39 c(B(c(b(c(x1))))) = x1 + 10 >= x1 + 17 = B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 1173.50/295.39 b(B(x1)) = x1 + 7 >= x1 = x1 1173.50/295.39 1173.50/295.39 B(b(x1)) = x1 + 7 >= x1 = x1 1173.50/295.39 1173.50/295.39 c(C(x1)) = x1 + 1 >= x1 = x1 1173.50/295.39 1173.50/295.39 C(c(x1)) = x1 + 1 >= x1 = x1 1173.50/295.39 problem: 1173.50/295.39 strict: 1173.50/295.39 C(x1) -> c(x1) 1173.50/295.39 B(B(x1)) -> b(x1) 1173.50/295.39 c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 weak: 1173.50/295.39 c(c(x1)) -> x1 1173.50/295.39 b(b(x1)) -> B(x1) 1173.50/295.39 b(B(x1)) -> x1 1173.50/295.39 B(b(x1)) -> x1 1173.50/295.39 c(C(x1)) -> x1 1173.50/295.39 C(c(x1)) -> x1 1173.50/295.39 Matrix Interpretation Processor: dim=1 1173.50/295.39 1173.50/295.39 max_matrix: 1173.50/295.39 1 1173.50/295.39 interpretation: 1173.50/295.39 [B](x0) = x0, 1173.50/295.39 1173.50/295.39 [b](x0) = x0, 1173.50/295.39 1173.50/295.39 [c](x0) = x0, 1173.50/295.39 1173.50/295.39 [C](x0) = x0 + 4 1173.50/295.39 orientation: 1173.50/295.39 C(x1) = x1 + 4 >= x1 = c(x1) 1173.50/295.39 1173.50/295.39 B(B(x1)) = x1 >= x1 = b(x1) 1173.50/295.39 1173.50/295.39 c(B(c(b(c(x1))))) = x1 >= x1 = B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 1173.50/295.39 c(c(x1)) = x1 >= x1 = x1 1173.50/295.39 1173.50/295.39 b(b(x1)) = x1 >= x1 = B(x1) 1173.50/295.39 1173.50/295.39 b(B(x1)) = x1 >= x1 = x1 1173.50/295.39 1173.50/295.39 B(b(x1)) = x1 >= x1 = x1 1173.50/295.39 1173.50/295.39 c(C(x1)) = x1 + 4 >= x1 = x1 1173.50/295.39 1173.50/295.39 C(c(x1)) = x1 + 4 >= x1 = x1 1173.50/295.39 problem: 1173.50/295.39 strict: 1173.50/295.39 B(B(x1)) -> b(x1) 1173.50/295.39 c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 weak: 1173.50/295.39 C(x1) -> c(x1) 1173.50/295.39 c(c(x1)) -> x1 1173.50/295.39 b(b(x1)) -> B(x1) 1173.50/295.39 b(B(x1)) -> x1 1173.50/295.39 B(b(x1)) -> x1 1173.50/295.39 c(C(x1)) -> x1 1173.50/295.39 C(c(x1)) -> x1 1173.50/295.39 Matrix Interpretation Processor: dim=1 1173.50/295.39 1173.50/295.39 max_matrix: 1173.50/295.39 1 1173.50/295.39 interpretation: 1173.50/295.39 [B](x0) = x0 + 12, 1173.50/295.39 1173.50/295.39 [b](x0) = x0 + 18, 1173.50/295.39 1173.50/295.39 [c](x0) = x0 + 1, 1173.50/295.39 1173.50/295.39 [C](x0) = x0 + 28 1173.50/295.39 orientation: 1173.50/295.39 B(B(x1)) = x1 + 24 >= x1 + 18 = b(x1) 1173.50/295.39 1173.50/295.39 c(B(c(b(c(x1))))) = x1 + 33 >= x1 + 63 = B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 1173.50/295.39 C(x1) = x1 + 28 >= x1 + 1 = c(x1) 1173.50/295.39 1173.50/295.39 c(c(x1)) = x1 + 2 >= x1 = x1 1173.50/295.39 1173.50/295.39 b(b(x1)) = x1 + 36 >= x1 + 12 = B(x1) 1173.50/295.39 1173.50/295.39 b(B(x1)) = x1 + 30 >= x1 = x1 1173.50/295.39 1173.50/295.39 B(b(x1)) = x1 + 30 >= x1 = x1 1173.50/295.39 1173.50/295.39 c(C(x1)) = x1 + 29 >= x1 = x1 1173.50/295.39 1173.50/295.39 C(c(x1)) = x1 + 29 >= x1 = x1 1173.50/295.39 problem: 1173.50/295.39 strict: 1173.50/295.39 c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 weak: 1173.50/295.39 B(B(x1)) -> b(x1) 1173.50/295.39 C(x1) -> c(x1) 1173.50/295.39 c(c(x1)) -> x1 1173.50/295.39 b(b(x1)) -> B(x1) 1173.50/295.39 b(B(x1)) -> x1 1173.50/295.39 B(b(x1)) -> x1 1173.50/295.39 c(C(x1)) -> x1 1173.50/295.39 C(c(x1)) -> x1 1173.50/295.39 Matrix Interpretation Processor: dim=4 1173.50/295.39 1173.50/295.39 max_matrix: 1173.50/295.39 [1 0 1 0] 1173.50/295.39 [0 0 1 1] 1173.50/295.39 [0 1 0 1] 1173.50/295.39 [0 1 1 1] 1173.50/295.39 interpretation: 1173.50/295.39 [1 0 0 0] 1173.50/295.39 [0 0 0 1] 1173.50/295.39 [B](x0) = [0 1 0 0]x0 1173.50/295.39 [0 0 1 0] , 1173.50/295.39 1173.50/295.39 [1 0 0 0] 1173.50/295.39 [0 0 1 0] 1173.50/295.39 [b](x0) = [0 0 0 1]x0 1173.50/295.39 [0 1 0 0] , 1173.50/295.39 1173.50/295.39 [1 0 1 0] [0] 1173.50/295.39 [0 0 1 0] [0] 1173.50/295.39 [c](x0) = [0 1 0 0]x0 + [0] 1173.50/295.39 [0 0 0 1] [1], 1173.50/295.39 1173.50/295.39 [1 0 1 0] [0] 1173.50/295.39 [0 0 1 0] [2] 1173.50/295.39 [C](x0) = [0 1 0 0]x0 + [3] 1173.50/295.39 [0 0 0 1] [1] 1173.50/295.39 orientation: 1173.50/295.39 [1 0 1 2] [2] [1 0 1 2] [1] 1173.50/295.39 [0 0 0 1] [1] [0 0 0 1] [1] 1173.50/295.39 c(B(c(b(c(x1))))) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 [0 1 0 0] [1] [0 1 0 0] [1] 1173.50/295.39 1173.50/295.39 [1 0 0 0] [1 0 0 0] 1173.50/295.39 [0 0 1 0] [0 0 1 0] 1173.50/295.39 B(B(x1)) = [0 0 0 1]x1 >= [0 0 0 1]x1 = b(x1) 1173.50/295.39 [0 1 0 0] [0 1 0 0] 1173.50/295.39 1173.50/295.39 [1 0 1 0] [0] [1 0 1 0] [0] 1173.50/295.39 [0 0 1 0] [2] [0 0 1 0] [0] 1173.50/295.39 C(x1) = [0 1 0 0]x1 + [3] >= [0 1 0 0]x1 + [0] = c(x1) 1173.50/295.39 [0 0 0 1] [1] [0 0 0 1] [1] 1173.50/295.39 1173.50/295.39 [1 1 1 0] [0] 1173.50/295.39 [0 1 0 0] [0] 1173.50/295.39 c(c(x1)) = [0 0 1 0]x1 + [0] >= x1 = x1 1173.50/295.39 [0 0 0 1] [2] 1173.50/295.39 1173.50/295.39 [1 0 0 0] [1 0 0 0] 1173.50/295.39 [0 0 0 1] [0 0 0 1] 1173.50/295.39 b(b(x1)) = [0 1 0 0]x1 >= [0 1 0 0]x1 = B(x1) 1173.50/295.39 [0 0 1 0] [0 0 1 0] 1173.50/295.39 1173.50/295.39 1173.50/295.39 1173.50/295.39 b(B(x1)) = x1 >= x1 = x1 1173.50/295.39 1173.50/295.39 1173.50/295.39 1173.50/295.39 1173.50/295.39 B(b(x1)) = x1 >= x1 = x1 1173.50/295.39 1173.50/295.39 1173.50/295.39 [1 1 1 0] [3] 1173.50/295.39 [0 1 0 0] [3] 1173.50/295.39 c(C(x1)) = [0 0 1 0]x1 + [2] >= x1 = x1 1173.50/295.39 [0 0 0 1] [2] 1173.50/295.39 1173.50/295.39 [1 1 1 0] [0] 1173.50/295.39 [0 1 0 0] [2] 1173.50/295.39 C(c(x1)) = [0 0 1 0]x1 + [3] >= x1 = x1 1173.50/295.39 [0 0 0 1] [2] 1173.50/295.39 problem: 1173.50/295.39 strict: 1173.50/295.39 1173.50/295.39 weak: 1173.50/295.39 c(B(c(b(c(x1))))) -> B(c(b(c(B(c(b(x1))))))) 1173.50/295.39 B(B(x1)) -> b(x1) 1173.50/295.39 C(x1) -> c(x1) 1173.50/295.39 c(c(x1)) -> x1 1173.50/295.39 b(b(x1)) -> B(x1) 1173.50/295.39 b(B(x1)) -> x1 1173.50/295.39 B(b(x1)) -> x1 1173.50/295.39 c(C(x1)) -> x1 1173.50/295.39 C(c(x1)) -> x1 1173.50/295.39 Qed 1173.59/295.40 EOF