YES(?,O(n^2)) 47.40/13.11 YES(?,O(n^2)) 47.40/13.11 47.40/13.11 Problem: 47.40/13.11 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.11 c(X) -> d(activate(X)) 47.40/13.11 h(X) -> c(n__d(X)) 47.40/13.11 f(X) -> n__f(X) 47.40/13.11 g(X) -> n__g(X) 47.40/13.11 d(X) -> n__d(X) 47.40/13.11 activate(n__f(X)) -> f(activate(X)) 47.40/13.11 activate(n__g(X)) -> g(X) 47.40/13.11 activate(n__d(X)) -> d(X) 47.40/13.11 activate(X) -> X 47.40/13.11 47.40/13.11 Proof: 47.40/13.11 Complexity Transformation Processor: 47.40/13.11 strict: 47.40/13.11 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.11 c(X) -> d(activate(X)) 47.40/13.11 h(X) -> c(n__d(X)) 47.40/13.11 f(X) -> n__f(X) 47.40/13.11 g(X) -> n__g(X) 47.40/13.11 d(X) -> n__d(X) 47.40/13.11 activate(n__f(X)) -> f(activate(X)) 47.40/13.11 activate(n__g(X)) -> g(X) 47.40/13.11 activate(n__d(X)) -> d(X) 47.40/13.11 activate(X) -> X 47.40/13.11 weak: 47.40/13.11 47.40/13.11 Matrix Interpretation Processor: dim=1 47.40/13.11 47.40/13.11 max_matrix: 47.40/13.11 1 47.40/13.11 interpretation: 47.40/13.11 [g](x0) = x0, 47.40/13.11 47.40/13.11 [n__d](x0) = x0 + 68, 47.40/13.11 47.40/13.11 [h](x0) = x0, 47.40/13.11 47.40/13.11 [d](x0) = x0 + 3, 47.40/13.11 47.40/13.11 [activate](x0) = x0 + 61, 47.40/13.11 47.40/13.11 [c](x0) = x0 + 48, 47.40/13.11 47.40/13.11 [n__g](x0) = x0 + 2, 47.40/13.11 47.40/13.11 [n__f](x0) = x0 + 7, 47.40/13.11 47.40/13.11 [f](x0) = x0 47.40/13.11 orientation: 47.40/13.11 f(f(X)) = X >= X + 64 = c(n__f(n__g(n__f(X)))) 47.40/13.11 47.40/13.11 c(X) = X + 48 >= X + 64 = d(activate(X)) 47.40/13.11 47.40/13.11 h(X) = X >= X + 116 = c(n__d(X)) 47.40/13.11 47.40/13.11 f(X) = X >= X + 7 = n__f(X) 47.40/13.11 47.40/13.11 g(X) = X >= X + 2 = n__g(X) 47.40/13.11 47.40/13.11 d(X) = X + 3 >= X + 68 = n__d(X) 47.40/13.11 47.40/13.11 activate(n__f(X)) = X + 68 >= X + 61 = f(activate(X)) 47.40/13.11 47.40/13.11 activate(n__g(X)) = X + 63 >= X = g(X) 47.40/13.11 47.40/13.11 activate(n__d(X)) = X + 129 >= X + 3 = d(X) 47.40/13.11 47.40/13.11 activate(X) = X + 61 >= X = X 47.40/13.11 problem: 47.40/13.11 strict: 47.40/13.11 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.11 c(X) -> d(activate(X)) 47.40/13.11 h(X) -> c(n__d(X)) 47.40/13.11 f(X) -> n__f(X) 47.40/13.11 g(X) -> n__g(X) 47.40/13.11 d(X) -> n__d(X) 47.40/13.11 weak: 47.40/13.11 activate(n__f(X)) -> f(activate(X)) 47.40/13.11 activate(n__g(X)) -> g(X) 47.40/13.11 activate(n__d(X)) -> d(X) 47.40/13.11 activate(X) -> X 47.40/13.11 Matrix Interpretation Processor: dim=1 47.40/13.11 47.40/13.11 max_matrix: 47.40/13.11 1 47.40/13.11 interpretation: 47.40/13.11 [g](x0) = x0, 47.40/13.11 47.40/13.11 [n__d](x0) = x0 + 208, 47.40/13.11 47.40/13.11 [h](x0) = x0, 47.40/13.11 47.40/13.11 [d](x0) = x0 + 4, 47.40/13.11 47.40/13.11 [activate](x0) = x0 + 32, 47.40/13.11 47.40/13.11 [c](x0) = x0 + 67, 47.40/13.11 47.40/13.11 [n__g](x0) = x0 + 140, 47.40/13.11 47.40/13.11 [n__f](x0) = x0 + 71, 47.40/13.11 47.40/13.11 [f](x0) = x0 + 2 47.40/13.11 orientation: 47.40/13.11 f(f(X)) = X + 4 >= X + 349 = c(n__f(n__g(n__f(X)))) 47.40/13.11 47.40/13.11 c(X) = X + 67 >= X + 36 = d(activate(X)) 47.40/13.11 47.40/13.11 h(X) = X >= X + 275 = c(n__d(X)) 47.40/13.11 47.40/13.11 f(X) = X + 2 >= X + 71 = n__f(X) 47.40/13.11 47.40/13.11 g(X) = X >= X + 140 = n__g(X) 47.40/13.11 47.40/13.11 d(X) = X + 4 >= X + 208 = n__d(X) 47.40/13.11 47.40/13.11 activate(n__f(X)) = X + 103 >= X + 34 = f(activate(X)) 47.40/13.11 47.40/13.11 activate(n__g(X)) = X + 172 >= X = g(X) 47.40/13.11 47.40/13.11 activate(n__d(X)) = X + 240 >= X + 4 = d(X) 47.40/13.11 47.40/13.11 activate(X) = X + 32 >= X = X 47.40/13.11 problem: 47.40/13.11 strict: 47.40/13.11 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.11 h(X) -> c(n__d(X)) 47.40/13.11 f(X) -> n__f(X) 47.40/13.11 g(X) -> n__g(X) 47.40/13.11 d(X) -> n__d(X) 47.40/13.11 weak: 47.40/13.11 c(X) -> d(activate(X)) 47.40/13.11 activate(n__f(X)) -> f(activate(X)) 47.40/13.11 activate(n__g(X)) -> g(X) 47.40/13.11 activate(n__d(X)) -> d(X) 47.40/13.11 activate(X) -> X 47.40/13.11 Matrix Interpretation Processor: dim=1 47.40/13.11 47.40/13.11 max_matrix: 47.40/13.11 1 47.40/13.11 interpretation: 47.40/13.11 [g](x0) = x0 + 113, 47.40/13.11 47.40/13.11 [n__d](x0) = x0 + 9, 47.40/13.11 47.40/13.11 [h](x0) = x0, 47.40/13.11 47.40/13.11 [d](x0) = x0, 47.40/13.11 47.40/13.11 [activate](x0) = x0 + 1, 47.40/13.11 47.40/13.11 [c](x0) = x0 + 189, 47.40/13.11 47.40/13.11 [n__g](x0) = x0 + 112, 47.40/13.11 47.40/13.11 [n__f](x0) = x0, 47.40/13.11 47.40/13.11 [f](x0) = x0 47.40/13.11 orientation: 47.40/13.11 f(f(X)) = X >= X + 301 = c(n__f(n__g(n__f(X)))) 47.40/13.11 47.40/13.11 h(X) = X >= X + 198 = c(n__d(X)) 47.40/13.11 47.40/13.11 f(X) = X >= X = n__f(X) 47.40/13.11 47.40/13.11 g(X) = X + 113 >= X + 112 = n__g(X) 47.40/13.11 47.40/13.11 d(X) = X >= X + 9 = n__d(X) 47.40/13.11 47.40/13.11 c(X) = X + 189 >= X + 1 = d(activate(X)) 47.40/13.11 47.40/13.11 activate(n__f(X)) = X + 1 >= X + 1 = f(activate(X)) 47.40/13.11 47.40/13.11 activate(n__g(X)) = X + 113 >= X + 113 = g(X) 47.40/13.11 47.40/13.11 activate(n__d(X)) = X + 10 >= X = d(X) 47.40/13.11 47.40/13.11 activate(X) = X + 1 >= X = X 47.40/13.11 problem: 47.40/13.11 strict: 47.40/13.11 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.11 h(X) -> c(n__d(X)) 47.40/13.11 f(X) -> n__f(X) 47.40/13.11 d(X) -> n__d(X) 47.40/13.11 weak: 47.40/13.11 g(X) -> n__g(X) 47.40/13.11 c(X) -> d(activate(X)) 47.40/13.11 activate(n__f(X)) -> f(activate(X)) 47.40/13.11 activate(n__g(X)) -> g(X) 47.40/13.11 activate(n__d(X)) -> d(X) 47.40/13.12 activate(X) -> X 47.40/13.12 Matrix Interpretation Processor: dim=1 47.40/13.12 47.40/13.12 max_matrix: 47.40/13.12 1 47.40/13.12 interpretation: 47.40/13.12 [g](x0) = x0 + 128, 47.40/13.12 47.40/13.12 [n__d](x0) = x0 + 80, 47.40/13.12 47.40/13.12 [h](x0) = x0 + 116, 47.40/13.12 47.40/13.12 [d](x0) = x0, 47.40/13.12 47.40/13.12 [activate](x0) = x0 + 32, 47.40/13.12 47.40/13.12 [c](x0) = x0 + 32, 47.40/13.12 47.40/13.12 [n__g](x0) = x0 + 97, 47.40/13.12 47.40/13.12 [n__f](x0) = x0 + 96, 47.40/13.12 47.40/13.12 [f](x0) = x0 47.40/13.12 orientation: 47.40/13.12 f(f(X)) = X >= X + 321 = c(n__f(n__g(n__f(X)))) 47.40/13.12 47.40/13.12 h(X) = X + 116 >= X + 112 = c(n__d(X)) 47.40/13.12 47.40/13.12 f(X) = X >= X + 96 = n__f(X) 47.40/13.12 47.40/13.12 d(X) = X >= X + 80 = n__d(X) 47.40/13.12 47.40/13.12 g(X) = X + 128 >= X + 97 = n__g(X) 47.40/13.12 47.40/13.12 c(X) = X + 32 >= X + 32 = d(activate(X)) 47.40/13.12 47.40/13.12 activate(n__f(X)) = X + 128 >= X + 32 = f(activate(X)) 47.40/13.12 47.40/13.12 activate(n__g(X)) = X + 129 >= X + 128 = g(X) 47.40/13.12 47.40/13.12 activate(n__d(X)) = X + 112 >= X = d(X) 47.40/13.12 47.40/13.12 activate(X) = X + 32 >= X = X 47.40/13.12 problem: 47.40/13.12 strict: 47.40/13.12 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.12 f(X) -> n__f(X) 47.40/13.12 d(X) -> n__d(X) 47.40/13.12 weak: 47.40/13.12 h(X) -> c(n__d(X)) 47.40/13.12 g(X) -> n__g(X) 47.40/13.12 c(X) -> d(activate(X)) 47.40/13.12 activate(n__f(X)) -> f(activate(X)) 47.40/13.12 activate(n__g(X)) -> g(X) 47.40/13.12 activate(n__d(X)) -> d(X) 47.40/13.12 activate(X) -> X 47.40/13.12 Matrix Interpretation Processor: dim=1 47.40/13.12 47.40/13.12 max_matrix: 47.40/13.12 1 47.40/13.12 interpretation: 47.40/13.12 [g](x0) = x0 + 19, 47.40/13.12 47.40/13.12 [n__d](x0) = x0, 47.40/13.12 47.40/13.12 [h](x0) = x0 + 128, 47.40/13.12 47.40/13.12 [d](x0) = x0 + 2, 47.40/13.12 47.40/13.12 [activate](x0) = x0 + 2, 47.40/13.12 47.40/13.12 [c](x0) = x0 + 5, 47.40/13.12 47.40/13.12 [n__g](x0) = x0 + 17, 47.40/13.12 47.40/13.12 [n__f](x0) = x0, 47.40/13.12 47.40/13.12 [f](x0) = x0 47.40/13.12 orientation: 47.40/13.12 f(f(X)) = X >= X + 22 = c(n__f(n__g(n__f(X)))) 47.40/13.12 47.40/13.12 f(X) = X >= X = n__f(X) 47.40/13.12 47.40/13.12 d(X) = X + 2 >= X = n__d(X) 47.40/13.12 47.40/13.12 h(X) = X + 128 >= X + 5 = c(n__d(X)) 47.40/13.12 47.40/13.12 g(X) = X + 19 >= X + 17 = n__g(X) 47.40/13.12 47.40/13.12 c(X) = X + 5 >= X + 4 = d(activate(X)) 47.40/13.12 47.40/13.12 activate(n__f(X)) = X + 2 >= X + 2 = f(activate(X)) 47.40/13.12 47.40/13.12 activate(n__g(X)) = X + 19 >= X + 19 = g(X) 47.40/13.12 47.40/13.12 activate(n__d(X)) = X + 2 >= X + 2 = d(X) 47.40/13.12 47.40/13.12 activate(X) = X + 2 >= X = X 47.40/13.12 problem: 47.40/13.12 strict: 47.40/13.12 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.12 f(X) -> n__f(X) 47.40/13.12 weak: 47.40/13.12 d(X) -> n__d(X) 47.40/13.12 h(X) -> c(n__d(X)) 47.40/13.12 g(X) -> n__g(X) 47.40/13.12 c(X) -> d(activate(X)) 47.40/13.12 activate(n__f(X)) -> f(activate(X)) 47.40/13.12 activate(n__g(X)) -> g(X) 47.40/13.12 activate(n__d(X)) -> d(X) 47.40/13.12 activate(X) -> X 47.40/13.12 Splitting Processor: 47.40/13.12 strict: 47.40/13.12 f(X) -> n__f(X) 47.40/13.12 weak: 47.40/13.12 d(X) -> n__d(X) 47.40/13.12 h(X) -> c(n__d(X)) 47.40/13.12 g(X) -> n__g(X) 47.40/13.12 c(X) -> d(activate(X)) 47.40/13.12 activate(n__f(X)) -> f(activate(X)) 47.40/13.12 activate(n__g(X)) -> g(X) 47.40/13.12 activate(n__d(X)) -> d(X) 47.40/13.12 activate(X) -> X 47.40/13.12 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.12 Matrix Interpretation Processor: dim=2 47.40/13.12 47.40/13.12 max_matrix: 47.40/13.12 [1 2] 47.40/13.12 [0 1] 47.40/13.12 interpretation: 47.40/13.12 [1 0] [0] 47.40/13.12 [g](x0) = [0 0]x0 + [1], 47.40/13.12 47.40/13.12 [1 0] 47.40/13.12 [n__d](x0) = [0 0]x0, 47.40/13.12 47.40/13.12 [1 1] [1] 47.40/13.12 [h](x0) = [0 1]x0 + [0], 47.40/13.12 47.40/13.12 [1 0] 47.40/13.12 [d](x0) = [0 0]x0, 47.40/13.12 47.40/13.12 47.40/13.12 [activate](x0) = x0, 47.40/13.12 47.40/13.12 47.40/13.12 [c](x0) = x0, 47.40/13.12 47.40/13.12 [1 0] [0] 47.40/13.12 [n__g](x0) = [0 0]x0 + [1], 47.40/13.12 47.40/13.12 [1 2] [0] 47.40/13.12 [n__f](x0) = [0 0]x0 + [2], 47.40/13.12 47.40/13.12 [1 2] [0] 47.40/13.12 [f](x0) = [0 0]x0 + [2] 47.40/13.12 orientation: 47.40/13.12 [1 2] [4] [1 2] [2] 47.40/13.12 f(f(X)) = [0 0]X + [2] >= [0 0]X + [2] = c(n__f(n__g(n__f(X)))) 47.40/13.12 47.40/13.12 [1 2] [0] [1 2] [0] 47.40/13.12 f(X) = [0 0]X + [2] >= [0 0]X + [2] = n__f(X) 47.40/13.12 47.40/13.12 [1 0] [1 0] 47.40/13.12 d(X) = [0 0]X >= [0 0]X = n__d(X) 47.40/13.12 47.40/13.12 [1 1] [1] [1 0] 47.40/13.12 h(X) = [0 1]X + [0] >= [0 0]X = c(n__d(X)) 47.40/13.12 47.40/13.12 [1 0] [0] [1 0] [0] 47.40/13.12 g(X) = [0 0]X + [1] >= [0 0]X + [1] = n__g(X) 47.40/13.12 47.40/13.12 [1 0] 47.40/13.12 c(X) = X >= [0 0]X = d(activate(X)) 47.40/13.12 47.40/13.12 [1 2] [0] [1 2] [0] 47.40/13.12 activate(n__f(X)) = [0 0]X + [2] >= [0 0]X + [2] = f(activate(X)) 47.40/13.12 47.40/13.12 [1 0] [0] [1 0] [0] 47.40/13.12 activate(n__g(X)) = [0 0]X + [1] >= [0 0]X + [1] = g(X) 47.40/13.12 47.40/13.12 [1 0] [1 0] 47.40/13.12 activate(n__d(X)) = [0 0]X >= [0 0]X = d(X) 47.40/13.12 47.40/13.12 47.40/13.12 activate(X) = X >= X = X 47.40/13.12 problem: 47.40/13.12 strict: 47.40/13.12 47.40/13.12 weak: 47.40/13.12 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.12 f(X) -> n__f(X) 47.40/13.12 d(X) -> n__d(X) 47.40/13.12 h(X) -> c(n__d(X)) 47.40/13.12 g(X) -> n__g(X) 47.40/13.12 c(X) -> d(activate(X)) 47.40/13.12 activate(n__f(X)) -> f(activate(X)) 47.40/13.12 activate(n__g(X)) -> g(X) 47.40/13.12 activate(n__d(X)) -> d(X) 47.40/13.12 activate(X) -> X 47.40/13.12 Qed 47.40/13.12 47.40/13.12 strict: 47.40/13.12 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.12 weak: 47.40/13.12 f(X) -> n__f(X) 47.40/13.12 d(X) -> n__d(X) 47.40/13.12 h(X) -> c(n__d(X)) 47.40/13.12 g(X) -> n__g(X) 47.40/13.12 c(X) -> d(activate(X)) 47.40/13.12 activate(n__f(X)) -> f(activate(X)) 47.40/13.12 activate(n__g(X)) -> g(X) 47.40/13.12 activate(n__d(X)) -> d(X) 47.40/13.12 activate(X) -> X 47.40/13.12 Matrix Interpretation Processor: dim=2 47.40/13.12 47.40/13.12 max_matrix: 47.40/13.12 [1 1] 47.40/13.12 [0 1] 47.40/13.12 interpretation: 47.40/13.12 [1 1] [1] 47.40/13.12 [g](x0) = [0 0]x0 + [0], 47.40/13.12 47.40/13.12 [1 0] 47.40/13.12 [n__d](x0) = [0 0]x0, 47.40/13.12 47.40/13.12 [1 0] 47.40/13.12 [h](x0) = [0 0]x0, 47.40/13.12 47.40/13.12 [1 0] 47.40/13.12 [d](x0) = [0 0]x0, 47.40/13.12 47.40/13.12 [1 1] 47.40/13.12 [activate](x0) = [0 1]x0, 47.40/13.12 47.40/13.12 [1 1] 47.40/13.12 [c](x0) = [0 0]x0, 47.40/13.12 47.40/13.12 [1 1] [1] 47.40/13.12 [n__g](x0) = [0 0]x0 + [0], 47.40/13.12 47.40/13.12 [1 1] [2] 47.40/13.12 [n__f](x0) = [0 1]x0 + [1], 47.40/13.12 47.40/13.12 [1 1] [3] 47.40/13.12 [f](x0) = [0 1]x0 + [1] 47.40/13.12 orientation: 47.40/13.12 [1 1] [3] [1 1] [2] 47.40/13.12 f(X) = [0 1]X + [1] >= [0 1]X + [1] = n__f(X) 47.40/13.12 47.40/13.12 [1 0] [1 0] 47.40/13.12 d(X) = [0 0]X >= [0 0]X = n__d(X) 47.40/13.12 47.40/13.12 [1 0] [1 0] 47.40/13.12 h(X) = [0 0]X >= [0 0]X = c(n__d(X)) 47.40/13.12 47.40/13.12 [1 1] [1] [1 1] [1] 47.40/13.12 g(X) = [0 0]X + [0] >= [0 0]X + [0] = n__g(X) 47.40/13.12 47.40/13.12 [1 1] [1 1] 47.40/13.12 c(X) = [0 0]X >= [0 0]X = d(activate(X)) 47.40/13.12 47.40/13.12 [1 2] [3] [1 2] [3] 47.40/13.12 activate(n__f(X)) = [0 1]X + [1] >= [0 1]X + [1] = f(activate(X)) 47.40/13.12 47.40/13.12 [1 1] [1] [1 1] [1] 47.40/13.12 activate(n__g(X)) = [0 0]X + [0] >= [0 0]X + [0] = g(X) 47.40/13.12 47.40/13.12 [1 0] [1 0] 47.40/13.12 activate(n__d(X)) = [0 0]X >= [0 0]X = d(X) 47.40/13.12 47.40/13.12 [1 1] 47.40/13.12 activate(X) = [0 1]X >= X = X 47.40/13.12 47.40/13.12 [1 2] [7] [1 2] [7] 47.40/13.12 f(f(X)) = [0 1]X + [2] >= [0 0]X + [0] = c(n__f(n__g(n__f(X)))) 47.40/13.12 problem: 47.40/13.12 strict: 47.40/13.12 47.40/13.12 weak: 47.40/13.12 f(X) -> n__f(X) 47.40/13.12 d(X) -> n__d(X) 47.40/13.12 h(X) -> c(n__d(X)) 47.40/13.12 g(X) -> n__g(X) 47.40/13.12 c(X) -> d(activate(X)) 47.40/13.12 activate(n__f(X)) -> f(activate(X)) 47.40/13.12 activate(n__g(X)) -> g(X) 47.40/13.12 activate(n__d(X)) -> d(X) 47.40/13.12 activate(X) -> X 47.40/13.12 f(f(X)) -> c(n__f(n__g(n__f(X)))) 47.40/13.12 Qed 47.40/13.12 EOF