Problem: f(X) -> if(X,c(),n__f(true())) if(true(),X,Y) -> X if(false(),X,Y) -> activate(Y) f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X Proof: Complexity Transformation Processor: strict: f(X) -> if(X,c(),n__f(true())) if(true(),X,Y) -> X if(false(),X,Y) -> activate(Y) f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [activate](x0) = x0 + 1, [false] = 0, [if](x0, x1, x2) = x0 + x1 + x2 + 15, [n__f](x0) = x0 + 7, [true] = 1, [c] = 2, [f](x0) = x0 orientation: f(X) = X >= X + 25 = if(X,c(),n__f(true())) if(true(),X,Y) = X + Y + 16 >= X = X if(false(),X,Y) = X + Y + 15 >= Y + 1 = activate(Y) f(X) = X >= X + 7 = n__f(X) activate(n__f(X)) = X + 8 >= X = f(X) activate(X) = X + 1 >= X = X problem: strict: f(X) -> if(X,c(),n__f(true())) f(X) -> n__f(X) weak: if(true(),X,Y) -> X if(false(),X,Y) -> activate(Y) activate(n__f(X)) -> f(X) activate(X) -> X Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [activate](x0) = x0 + 2, [false] = 8, [if](x0, x1, x2) = x0 + x1 + x2, [n__f](x0) = x0 + 1, [true] = 0, [c] = 8, [f](x0) = x0 + 3 orientation: f(X) = X + 3 >= X + 9 = if(X,c(),n__f(true())) f(X) = X + 3 >= X + 1 = n__f(X) if(true(),X,Y) = X + Y >= X = X if(false(),X,Y) = X + Y + 8 >= Y + 2 = activate(Y) activate(n__f(X)) = X + 3 >= X + 3 = f(X) activate(X) = X + 2 >= X = X problem: strict: f(X) -> if(X,c(),n__f(true())) weak: f(X) -> n__f(X) if(true(),X,Y) -> X if(false(),X,Y) -> activate(Y) activate(n__f(X)) -> f(X) activate(X) -> X Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [activate](x0) = x0 + 1, [false] = 1, [if](x0, x1, x2) = x0 + x1 + x2, [n__f](x0) = x0 + 4, [true] = 0, [c] = 0, [f](x0) = x0 + 5 orientation: f(X) = X + 5 >= X + 4 = if(X,c(),n__f(true())) f(X) = X + 5 >= X + 4 = n__f(X) if(true(),X,Y) = X + Y >= X = X if(false(),X,Y) = X + Y + 1 >= Y + 1 = activate(Y) activate(n__f(X)) = X + 5 >= X + 5 = f(X) activate(X) = X + 1 >= X = X problem: strict: weak: f(X) -> if(X,c(),n__f(true())) f(X) -> n__f(X) if(true(),X,Y) -> X if(false(),X,Y) -> activate(Y) activate(n__f(X)) -> f(X) activate(X) -> X Qed