YES(?,O(n^1)) 0.16/0.32 YES(?,O(n^1)) 0.16/0.32 0.16/0.32 Problem: 0.16/0.32 f(X) -> if(X,c(),n__f(true())) 0.16/0.32 if(true(),X,Y) -> X 0.16/0.32 if(false(),X,Y) -> activate(Y) 0.16/0.32 f(X) -> n__f(X) 0.16/0.32 activate(n__f(X)) -> f(X) 0.16/0.32 activate(X) -> X 0.16/0.32 0.16/0.32 Proof: 0.16/0.32 Complexity Transformation Processor: 0.16/0.32 strict: 0.16/0.32 f(X) -> if(X,c(),n__f(true())) 0.16/0.32 if(true(),X,Y) -> X 0.16/0.32 if(false(),X,Y) -> activate(Y) 0.16/0.32 f(X) -> n__f(X) 0.16/0.32 activate(n__f(X)) -> f(X) 0.16/0.32 activate(X) -> X 0.16/0.32 weak: 0.16/0.32 0.16/0.32 Matrix Interpretation Processor: dim=1 0.16/0.32 0.16/0.32 max_matrix: 0.16/0.32 1 0.16/0.32 interpretation: 0.16/0.32 [activate](x0) = x0 + 145, 0.16/0.32 0.16/0.32 [false] = 132, 0.16/0.32 0.16/0.32 [if](x0, x1, x2) = x0 + x1 + x2 + 238, 0.16/0.32 0.16/0.32 [n__f](x0) = x0 + 119, 0.16/0.32 0.16/0.32 [true] = 24, 0.16/0.32 0.16/0.32 [c] = 10, 0.16/0.32 0.16/0.32 [f](x0) = x0 0.16/0.32 orientation: 0.16/0.32 f(X) = X >= X + 391 = if(X,c(),n__f(true())) 0.16/0.32 0.16/0.32 if(true(),X,Y) = X + Y + 262 >= X = X 0.16/0.32 0.16/0.32 if(false(),X,Y) = X + Y + 370 >= Y + 145 = activate(Y) 0.16/0.32 0.16/0.32 f(X) = X >= X + 119 = n__f(X) 0.16/0.32 0.16/0.32 activate(n__f(X)) = X + 264 >= X = f(X) 0.16/0.32 0.16/0.32 activate(X) = X + 145 >= X = X 0.16/0.32 problem: 0.16/0.32 strict: 0.16/0.32 f(X) -> if(X,c(),n__f(true())) 0.16/0.32 f(X) -> n__f(X) 0.16/0.32 weak: 0.16/0.32 if(true(),X,Y) -> X 0.16/0.32 if(false(),X,Y) -> activate(Y) 0.16/0.32 activate(n__f(X)) -> f(X) 0.16/0.32 activate(X) -> X 0.16/0.32 Matrix Interpretation Processor: dim=1 0.16/0.32 0.16/0.32 max_matrix: 0.16/0.32 1 0.16/0.32 interpretation: 0.16/0.32 [activate](x0) = x0 + 1, 0.16/0.32 0.16/0.32 [false] = 32, 0.16/0.32 0.16/0.32 [if](x0, x1, x2) = x0 + x1 + x2, 0.16/0.32 0.16/0.32 [n__f](x0) = x0 + 4, 0.16/0.32 0.16/0.32 [true] = 0, 0.16/0.32 0.16/0.32 [c] = 252, 0.16/0.32 0.16/0.32 [f](x0) = x0 + 5 0.16/0.32 orientation: 0.16/0.32 f(X) = X + 5 >= X + 256 = if(X,c(),n__f(true())) 0.16/0.32 0.16/0.32 f(X) = X + 5 >= X + 4 = n__f(X) 0.16/0.32 0.16/0.32 if(true(),X,Y) = X + Y >= X = X 0.16/0.32 0.16/0.32 if(false(),X,Y) = X + Y + 32 >= Y + 1 = activate(Y) 0.16/0.32 0.16/0.32 activate(n__f(X)) = X + 5 >= X + 5 = f(X) 0.16/0.32 0.16/0.32 activate(X) = X + 1 >= X = X 0.16/0.32 problem: 0.16/0.32 strict: 0.16/0.32 f(X) -> if(X,c(),n__f(true())) 0.16/0.32 weak: 0.16/0.32 f(X) -> n__f(X) 0.16/0.32 if(true(),X,Y) -> X 0.16/0.32 if(false(),X,Y) -> activate(Y) 0.16/0.32 activate(n__f(X)) -> f(X) 0.16/0.32 activate(X) -> X 0.16/0.32 Matrix Interpretation Processor: dim=1 0.16/0.32 0.16/0.32 max_matrix: 0.16/0.32 1 0.16/0.32 interpretation: 0.16/0.32 [activate](x0) = x0 + 63, 0.16/0.32 0.16/0.32 [false] = 64, 0.16/0.32 0.16/0.32 [if](x0, x1, x2) = x0 + x1 + x2 + 9, 0.16/0.32 0.16/0.32 [n__f](x0) = x0 + 1, 0.16/0.32 0.16/0.32 [true] = 16, 0.16/0.32 0.16/0.32 [c] = 16, 0.16/0.32 0.16/0.32 [f](x0) = x0 + 64 0.16/0.32 orientation: 0.16/0.32 f(X) = X + 64 >= X + 42 = if(X,c(),n__f(true())) 0.16/0.32 0.16/0.32 f(X) = X + 64 >= X + 1 = n__f(X) 0.16/0.32 0.16/0.32 if(true(),X,Y) = X + Y + 25 >= X = X 0.16/0.32 0.16/0.32 if(false(),X,Y) = X + Y + 73 >= Y + 63 = activate(Y) 0.16/0.32 0.16/0.32 activate(n__f(X)) = X + 64 >= X + 64 = f(X) 0.16/0.32 0.16/0.32 activate(X) = X + 63 >= X = X 0.16/0.32 problem: 0.16/0.32 strict: 0.16/0.32 0.16/0.32 weak: 0.16/0.32 f(X) -> if(X,c(),n__f(true())) 0.16/0.32 f(X) -> n__f(X) 0.16/0.32 if(true(),X,Y) -> X 0.16/0.32 if(false(),X,Y) -> activate(Y) 0.16/0.32 activate(n__f(X)) -> f(X) 0.16/0.32 activate(X) -> X 0.16/0.32 Qed 0.16/0.33 EOF