YES(?,O(n^2)) 29.78/10.46 YES(?,O(n^2)) 29.78/10.46 29.78/10.46 Problem: 29.78/10.46 f(X) -> g(n__h(n__f(X))) 29.78/10.46 h(X) -> n__h(X) 29.78/10.46 f(X) -> n__f(X) 29.78/10.46 activate(n__h(X)) -> h(activate(X)) 29.78/10.46 activate(n__f(X)) -> f(activate(X)) 29.78/10.46 activate(X) -> X 29.78/10.46 29.78/10.46 Proof: 29.78/10.46 Complexity Transformation Processor: 29.78/10.46 strict: 29.78/10.46 f(X) -> g(n__h(n__f(X))) 29.78/10.46 h(X) -> n__h(X) 29.78/10.46 f(X) -> n__f(X) 29.78/10.46 activate(n__h(X)) -> h(activate(X)) 29.78/10.46 activate(n__f(X)) -> f(activate(X)) 29.78/10.46 activate(X) -> X 29.78/10.46 weak: 29.78/10.46 29.78/10.46 Matrix Interpretation Processor: dim=1 29.78/10.46 29.78/10.46 max_matrix: 29.78/10.46 1 29.78/10.46 interpretation: 29.78/10.46 [activate](x0) = x0 + 58, 29.78/10.46 29.78/10.46 [h](x0) = x0 + 198, 29.78/10.46 29.78/10.46 [g](x0) = x0 + 46, 29.78/10.46 29.78/10.46 [n__h](x0) = x0 + 208, 29.78/10.46 29.78/10.46 [n__f](x0) = x0 + 131, 29.78/10.46 29.78/10.46 [f](x0) = x0 + 70 29.78/10.46 orientation: 29.78/10.46 f(X) = X + 70 >= X + 385 = g(n__h(n__f(X))) 29.78/10.46 29.78/10.46 h(X) = X + 198 >= X + 208 = n__h(X) 29.78/10.46 29.78/10.46 f(X) = X + 70 >= X + 131 = n__f(X) 29.78/10.46 29.78/10.46 activate(n__h(X)) = X + 266 >= X + 256 = h(activate(X)) 29.78/10.46 29.78/10.46 activate(n__f(X)) = X + 189 >= X + 128 = f(activate(X)) 29.78/10.46 29.78/10.46 activate(X) = X + 58 >= X = X 29.78/10.46 problem: 29.78/10.46 strict: 29.78/10.46 f(X) -> g(n__h(n__f(X))) 29.78/10.46 h(X) -> n__h(X) 29.78/10.46 f(X) -> n__f(X) 29.78/10.46 weak: 29.78/10.46 activate(n__h(X)) -> h(activate(X)) 29.78/10.46 activate(n__f(X)) -> f(activate(X)) 29.78/10.46 activate(X) -> X 29.78/10.46 Matrix Interpretation Processor: dim=2 29.78/10.46 29.78/10.46 max_matrix: 29.78/10.46 [1 2] 29.78/10.46 [0 1] 29.78/10.46 interpretation: 29.78/10.46 [1 2] [2] 29.78/10.46 [activate](x0) = [0 1]x0 + [0], 29.78/10.46 29.78/10.46 [1] 29.78/10.46 [h](x0) = x0 + [0], 29.78/10.46 29.78/10.46 [1 0] [1] 29.78/10.46 [g](x0) = [0 0]x0 + [1], 29.78/10.46 29.78/10.46 [1] 29.78/10.46 [n__h](x0) = x0 + [0], 29.78/10.46 29.78/10.46 [0] 29.78/10.46 [n__f](x0) = x0 + [1], 29.78/10.46 29.78/10.46 [2] 29.78/10.46 [f](x0) = x0 + [1] 29.78/10.46 orientation: 29.78/10.46 [2] [1 0] [2] 29.78/10.46 f(X) = X + [1] >= [0 0]X + [1] = g(n__h(n__f(X))) 29.78/10.46 29.78/10.46 [1] [1] 29.78/10.46 h(X) = X + [0] >= X + [0] = n__h(X) 29.78/10.46 29.78/10.46 [2] [0] 29.78/10.46 f(X) = X + [1] >= X + [1] = n__f(X) 29.78/10.46 29.78/10.46 [1 2] [3] [1 2] [3] 29.78/10.46 activate(n__h(X)) = [0 1]X + [0] >= [0 1]X + [0] = h(activate(X)) 29.78/10.46 29.78/10.46 [1 2] [4] [1 2] [4] 29.78/10.46 activate(n__f(X)) = [0 1]X + [1] >= [0 1]X + [1] = f(activate(X)) 29.78/10.46 29.78/10.46 [1 2] [2] 29.78/10.46 activate(X) = [0 1]X + [0] >= X = X 29.78/10.46 problem: 29.78/10.46 strict: 29.78/10.46 f(X) -> g(n__h(n__f(X))) 29.78/10.46 h(X) -> n__h(X) 29.78/10.46 weak: 29.78/10.46 f(X) -> n__f(X) 29.78/10.46 activate(n__h(X)) -> h(activate(X)) 29.78/10.46 activate(n__f(X)) -> f(activate(X)) 29.78/10.46 activate(X) -> X 29.78/10.46 Splitting Processor: 29.78/10.46 strict: 29.78/10.46 h(X) -> n__h(X) 29.78/10.46 weak: 29.78/10.46 f(X) -> n__f(X) 29.78/10.46 activate(n__h(X)) -> h(activate(X)) 29.78/10.46 activate(n__f(X)) -> f(activate(X)) 29.78/10.46 activate(X) -> X 29.78/10.46 f(X) -> g(n__h(n__f(X))) 29.78/10.46 Matrix Interpretation Processor: dim=2 29.78/10.46 29.78/10.46 max_matrix: 29.78/10.46 [1 2] 29.78/10.46 [0 1] 29.78/10.46 interpretation: 29.78/10.46 [1 2] 29.78/10.46 [activate](x0) = [0 1]x0, 29.78/10.46 29.78/10.46 [1] 29.78/10.46 [h](x0) = x0 + [1], 29.78/10.46 29.78/10.46 [1 0] 29.78/10.46 [g](x0) = [0 0]x0, 29.78/10.46 29.78/10.46 [0] 29.78/10.46 [n__h](x0) = x0 + [1], 29.78/10.46 29.78/10.46 [2] 29.78/10.46 [n__f](x0) = x0 + [3], 29.78/10.46 29.78/10.46 [3] 29.78/10.46 [f](x0) = x0 + [3] 29.78/10.46 orientation: 29.78/10.46 [3] [1 0] [2] 29.78/10.46 f(X) = X + [3] >= [0 0]X + [0] = g(n__h(n__f(X))) 29.78/10.46 29.78/10.46 [1] [0] 29.78/10.46 h(X) = X + [1] >= X + [1] = n__h(X) 29.78/10.46 29.78/10.46 [3] [2] 29.78/10.46 f(X) = X + [3] >= X + [3] = n__f(X) 29.78/10.46 29.78/10.46 [1 2] [2] [1 2] [1] 29.78/10.46 activate(n__h(X)) = [0 1]X + [1] >= [0 1]X + [1] = h(activate(X)) 29.78/10.46 29.78/10.46 [1 2] [8] [1 2] [3] 29.78/10.46 activate(n__f(X)) = [0 1]X + [3] >= [0 1]X + [3] = f(activate(X)) 29.78/10.46 29.78/10.46 [1 2] 29.78/10.46 activate(X) = [0 1]X >= X = X 29.78/10.46 problem: 29.78/10.46 strict: 29.78/10.46 29.78/10.46 weak: 29.78/10.46 f(X) -> g(n__h(n__f(X))) 29.78/10.46 h(X) -> n__h(X) 29.78/10.47 f(X) -> n__f(X) 29.78/10.47 activate(n__h(X)) -> h(activate(X)) 29.78/10.47 activate(n__f(X)) -> f(activate(X)) 29.78/10.47 activate(X) -> X 29.78/10.47 Qed 29.78/10.47 29.78/10.47 strict: 29.78/10.47 f(X) -> g(n__h(n__f(X))) 29.78/10.47 weak: 29.78/10.47 h(X) -> n__h(X) 29.78/10.47 f(X) -> n__f(X) 29.78/10.47 activate(n__h(X)) -> h(activate(X)) 29.78/10.47 activate(n__f(X)) -> f(activate(X)) 29.78/10.47 activate(X) -> X 29.78/10.47 Matrix Interpretation Processor: dim=2 29.78/10.47 29.78/10.47 max_matrix: 29.78/10.47 [1 1] 29.78/10.47 [0 1] 29.78/10.47 interpretation: 29.78/10.47 [1 1] 29.78/10.47 [activate](x0) = [0 1]x0, 29.78/10.47 29.78/10.47 [2] 29.78/10.47 [h](x0) = x0 + [2], 29.78/10.47 29.78/10.47 [1 0] 29.78/10.47 [g](x0) = [0 0]x0, 29.78/10.47 29.78/10.47 [0] 29.78/10.47 [n__h](x0) = x0 + [2], 29.78/10.47 29.78/10.47 29.78/10.47 [n__f](x0) = x0, 29.78/10.47 29.78/10.47 29.78/10.47 [f](x0) = x0 29.78/10.47 orientation: 29.78/10.47 [2] [0] 29.78/10.47 h(X) = X + [2] >= X + [2] = n__h(X) 29.78/10.47 29.78/10.47 29.78/10.47 f(X) = X >= X = n__f(X) 29.78/10.47 29.78/10.47 [1 1] [2] [1 1] [2] 29.78/10.47 activate(n__h(X)) = [0 1]X + [2] >= [0 1]X + [2] = h(activate(X)) 29.78/10.47 29.78/10.47 [1 1] [1 1] 29.78/10.47 activate(n__f(X)) = [0 1]X >= [0 1]X = f(activate(X)) 29.78/10.47 29.78/10.47 [1 1] 29.78/10.47 activate(X) = [0 1]X >= X = X 29.78/10.47 29.78/10.47 [1 0] 29.78/10.47 f(X) = X >= [0 0]X = g(n__h(n__f(X))) 29.78/10.47 problem: 29.78/10.47 strict: 29.78/10.47 29.78/10.47 weak: 29.78/10.47 h(X) -> n__h(X) 29.78/10.47 f(X) -> n__f(X) 29.78/10.47 activate(n__h(X)) -> h(activate(X)) 29.78/10.47 activate(n__f(X)) -> f(activate(X)) 29.78/10.47 activate(X) -> X 29.78/10.47 f(X) -> g(n__h(n__f(X))) 29.78/10.47 Qed 29.78/10.47 EOF