YES(?,O(n^2)) 24.25/10.00 YES(?,O(n^2)) 24.25/10.00 24.25/10.00 Problem: 24.25/10.00 a__zeros() -> cons(0(),zeros()) 24.25/10.00 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.00 mark(zeros()) -> a__zeros() 24.25/10.00 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.00 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.00 mark(0()) -> 0() 24.25/10.00 a__zeros() -> zeros() 24.25/10.00 a__tail(X) -> tail(X) 24.25/10.00 24.25/10.00 Proof: 24.25/10.00 Complexity Transformation Processor: 24.25/10.00 strict: 24.25/10.00 a__zeros() -> cons(0(),zeros()) 24.25/10.00 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.00 mark(zeros()) -> a__zeros() 24.25/10.00 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.00 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.00 mark(0()) -> 0() 24.25/10.00 a__zeros() -> zeros() 24.25/10.00 a__tail(X) -> tail(X) 24.25/10.00 weak: 24.25/10.00 24.25/10.00 Matrix Interpretation Processor: dim=1 24.25/10.00 24.25/10.00 max_matrix: 24.25/10.00 1 24.25/10.00 interpretation: 24.25/10.00 [tail](x0) = x0 + 32, 24.25/10.00 24.25/10.00 [mark](x0) = x0 + 228, 24.25/10.00 24.25/10.00 [a__tail](x0) = x0 + 191, 24.25/10.00 24.25/10.00 [cons](x0, x1) = x0 + x1 + 1, 24.25/10.00 24.25/10.00 [zeros] = 6, 24.25/10.00 24.25/10.00 [0] = 28, 24.25/10.00 24.25/10.00 [a__zeros] = 0 24.25/10.00 orientation: 24.25/10.00 a__zeros() = 0 >= 35 = cons(0(),zeros()) 24.25/10.00 24.25/10.00 a__tail(cons(X,XS)) = X + XS + 192 >= XS + 228 = mark(XS) 24.25/10.00 24.25/10.00 mark(zeros()) = 234 >= 0 = a__zeros() 24.25/10.00 24.25/10.00 mark(tail(X)) = X + 260 >= X + 419 = a__tail(mark(X)) 24.25/10.00 24.25/10.00 mark(cons(X1,X2)) = X1 + X2 + 229 >= X1 + X2 + 229 = cons(mark(X1),X2) 24.25/10.00 24.25/10.00 mark(0()) = 256 >= 28 = 0() 24.25/10.00 24.25/10.00 a__zeros() = 0 >= 6 = zeros() 24.25/10.00 24.25/10.00 a__tail(X) = X + 191 >= X + 32 = tail(X) 24.25/10.00 problem: 24.25/10.00 strict: 24.25/10.00 a__zeros() -> cons(0(),zeros()) 24.25/10.00 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.00 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.00 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.00 a__zeros() -> zeros() 24.25/10.00 weak: 24.25/10.00 mark(zeros()) -> a__zeros() 24.25/10.00 mark(0()) -> 0() 24.25/10.00 a__tail(X) -> tail(X) 24.25/10.00 Matrix Interpretation Processor: dim=1 24.25/10.00 24.25/10.00 max_matrix: 24.25/10.00 1 24.25/10.00 interpretation: 24.25/10.00 [tail](x0) = x0 + 5, 24.25/10.00 24.25/10.00 [mark](x0) = x0, 24.25/10.00 24.25/10.00 [a__tail](x0) = x0 + 5, 24.25/10.00 24.25/10.00 [cons](x0, x1) = x0 + x1 + 36, 24.25/10.00 24.25/10.00 [zeros] = 8, 24.25/10.00 24.25/10.00 [0] = 17, 24.25/10.00 24.25/10.00 [a__zeros] = 8 24.25/10.00 orientation: 24.25/10.00 a__zeros() = 8 >= 61 = cons(0(),zeros()) 24.25/10.00 24.25/10.00 a__tail(cons(X,XS)) = X + XS + 41 >= XS = mark(XS) 24.25/10.00 24.25/10.00 mark(tail(X)) = X + 5 >= X + 5 = a__tail(mark(X)) 24.25/10.00 24.25/10.00 mark(cons(X1,X2)) = X1 + X2 + 36 >= X1 + X2 + 36 = cons(mark(X1),X2) 24.25/10.00 24.25/10.00 a__zeros() = 8 >= 8 = zeros() 24.25/10.00 24.25/10.00 mark(zeros()) = 8 >= 8 = a__zeros() 24.25/10.00 24.25/10.00 mark(0()) = 17 >= 17 = 0() 24.25/10.00 24.25/10.00 a__tail(X) = X + 5 >= X + 5 = tail(X) 24.25/10.00 problem: 24.25/10.00 strict: 24.25/10.00 a__zeros() -> cons(0(),zeros()) 24.25/10.00 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.00 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.00 a__zeros() -> zeros() 24.25/10.00 weak: 24.25/10.00 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.00 mark(zeros()) -> a__zeros() 24.25/10.00 mark(0()) -> 0() 24.25/10.00 a__tail(X) -> tail(X) 24.25/10.00 Matrix Interpretation Processor: dim=1 24.25/10.00 24.25/10.00 max_matrix: 24.25/10.00 1 24.25/10.00 interpretation: 24.25/10.00 [tail](x0) = x0, 24.25/10.00 24.25/10.00 [mark](x0) = x0 + 8, 24.25/10.00 24.25/10.00 [a__tail](x0) = x0 + 7, 24.25/10.00 24.25/10.00 [cons](x0, x1) = x0 + x1 + 1, 24.25/10.00 24.25/10.00 [zeros] = 0, 24.25/10.00 24.25/10.00 [0] = 0, 24.25/10.00 24.25/10.00 [a__zeros] = 8 24.25/10.00 orientation: 24.25/10.00 a__zeros() = 8 >= 1 = cons(0(),zeros()) 24.25/10.00 24.25/10.00 mark(tail(X)) = X + 8 >= X + 15 = a__tail(mark(X)) 24.25/10.00 24.25/10.00 mark(cons(X1,X2)) = X1 + X2 + 9 >= X1 + X2 + 9 = cons(mark(X1),X2) 24.25/10.00 24.25/10.00 a__zeros() = 8 >= 0 = zeros() 24.25/10.00 24.25/10.00 a__tail(cons(X,XS)) = X + XS + 8 >= XS + 8 = mark(XS) 24.25/10.00 24.25/10.00 mark(zeros()) = 8 >= 8 = a__zeros() 24.25/10.00 24.25/10.00 mark(0()) = 8 >= 0 = 0() 24.25/10.00 24.25/10.00 a__tail(X) = X + 7 >= X = tail(X) 24.25/10.00 problem: 24.25/10.00 strict: 24.25/10.00 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.00 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.00 weak: 24.25/10.00 a__zeros() -> cons(0(),zeros()) 24.25/10.00 a__zeros() -> zeros() 24.25/10.00 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.00 mark(zeros()) -> a__zeros() 24.25/10.00 mark(0()) -> 0() 24.25/10.00 a__tail(X) -> tail(X) 24.25/10.00 Splitting Processor: 24.25/10.00 strict: 24.25/10.00 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.00 weak: 24.25/10.00 a__zeros() -> cons(0(),zeros()) 24.25/10.00 a__zeros() -> zeros() 24.25/10.00 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.00 mark(zeros()) -> a__zeros() 24.25/10.00 mark(0()) -> 0() 24.25/10.00 a__tail(X) -> tail(X) 24.25/10.00 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.00 Bounds Processor: 24.25/10.00 bound: 1 24.25/10.00 enrichment: match 24.25/10.01 automaton: 24.25/10.01 final states: {7,6,5} 24.25/10.01 transitions: 24.25/10.01 a__tail1(9) -> 10* 24.25/10.01 mark1(25) -> 31* 24.25/10.01 mark1(17) -> 10* 24.25/10.01 mark1(2) -> 10* 24.25/10.01 mark1(24) -> 25* 24.25/10.01 mark1(4) -> 10* 24.25/10.01 mark1(16) -> 17* 24.25/10.01 mark1(1) -> 10* 24.25/10.01 mark1(28) -> 10* 24.25/10.01 mark1(18) -> 19* 24.25/10.01 mark1(8) -> 9* 24.25/10.01 mark1(3) -> 10* 24.25/10.01 cons1(19,2) -> 9* 24.25/10.01 cons1(9,2) -> 9* 24.25/10.01 cons1(19,4) -> 9* 24.25/10.01 cons1(9,4) -> 9* 24.25/10.01 cons1(25,1) -> 9* 24.25/10.01 cons1(25,3) -> 9* 24.25/10.01 cons1(10,1) -> 10* 24.25/10.01 cons1(10,3) -> 10* 24.25/10.01 cons1(29,28) -> 6* 24.25/10.01 cons1(25,17) -> 7* 24.25/10.01 cons1(10,17) -> 10* 24.25/10.01 cons1(31,28) -> 10* 24.25/10.01 cons1(9,1) -> 9* 24.25/10.01 cons1(9,3) -> 9* 24.25/10.01 cons1(25,2) -> 9* 24.25/10.01 cons1(25,4) -> 9* 24.25/10.01 cons1(10,2) -> 10* 24.25/10.01 cons1(10,4) -> 10* 24.25/10.01 cons1(25,28) -> 17,5 24.25/10.01 cons1(17,2) -> 9* 24.25/10.01 cons1(17,4) -> 9* 24.25/10.01 tail1(9) -> 10* 24.25/10.01 01() -> 31,10,25,29 24.25/10.01 a__zeros1() -> 10,17 24.25/10.01 zeros1() -> 10,17,28 24.25/10.01 mark0(2) -> 7,5 24.25/10.01 mark0(4) -> 7,5 24.25/10.01 mark0(1) -> 7,5 24.25/10.01 mark0(3) -> 7,5 24.25/10.01 tail0(2) -> 7,1 24.25/10.01 tail0(4) -> 7,1 24.25/10.01 tail0(1) -> 7,1 24.25/10.01 tail0(3) -> 7,1 24.25/10.01 a__tail0(2) -> 7* 24.25/10.01 a__tail0(4) -> 7* 24.25/10.01 a__tail0(1) -> 7* 24.25/10.01 a__tail0(3) -> 7* 24.25/10.01 a__zeros0() -> 7,5,6 24.25/10.01 cons0(3,1) -> 2* 24.25/10.01 cons0(3,3) -> 2* 24.25/10.01 cons0(4,2) -> 2* 24.25/10.01 cons0(4,4) -> 2* 24.25/10.01 cons0(5,1) -> 7,5 24.25/10.01 cons0(5,3) -> 7,5 24.25/10.01 cons0(1,2) -> 2* 24.25/10.01 cons0(1,4) -> 2* 24.25/10.01 cons0(2,1) -> 2* 24.25/10.01 cons0(2,3) -> 2* 24.25/10.01 cons0(3,2) -> 2* 24.25/10.01 cons0(3,4) -> 2* 24.25/10.01 cons0(4,1) -> 2* 24.25/10.01 cons0(4,3) -> 2* 24.25/10.01 cons0(5,2) -> 7,5 24.25/10.01 cons0(5,4) -> 7,5 24.25/10.01 cons0(1,1) -> 2* 24.25/10.01 cons0(1,3) -> 2* 24.25/10.01 cons0(2,2) -> 2* 24.25/10.01 cons0(2,4) -> 2* 24.25/10.01 00() -> 7,5,3 24.25/10.01 zeros0() -> 7,5,6,4 24.25/10.01 1 -> 18* 24.25/10.01 2 -> 8* 24.25/10.01 3 -> 24* 24.25/10.01 4 -> 16* 24.25/10.01 10 -> 7,19,5 24.25/10.01 17 -> 9* 24.25/10.01 19 -> 9* 24.25/10.01 25 -> 9* 24.25/10.01 problem: 24.25/10.01 strict: 24.25/10.01 24.25/10.01 weak: 24.25/10.01 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.01 a__zeros() -> cons(0(),zeros()) 24.25/10.01 a__zeros() -> zeros() 24.25/10.01 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.01 mark(zeros()) -> a__zeros() 24.25/10.01 mark(0()) -> 0() 24.25/10.01 a__tail(X) -> tail(X) 24.25/10.01 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.01 Qed 24.25/10.01 24.25/10.01 strict: 24.25/10.01 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.01 weak: 24.25/10.01 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.01 a__zeros() -> cons(0(),zeros()) 24.25/10.01 a__zeros() -> zeros() 24.25/10.01 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.01 mark(zeros()) -> a__zeros() 24.25/10.01 mark(0()) -> 0() 24.25/10.01 a__tail(X) -> tail(X) 24.25/10.01 Matrix Interpretation Processor: dim=4 24.25/10.01 24.25/10.01 max_matrix: 24.25/10.01 [1 1 0 1] 24.25/10.01 [0 0 0 0] 24.25/10.01 [0 0 0 1] 24.25/10.01 [0 0 0 1] 24.25/10.01 interpretation: 24.25/10.01 [1 0 0 0] [0] 24.25/10.01 [0 0 0 0] [0] 24.25/10.01 [tail](x0) = [0 0 0 1]x0 + [0] 24.25/10.01 [0 0 0 1] [1], 24.25/10.01 24.25/10.01 [1 0 0 1] [1] 24.25/10.01 [0 0 0 0] [0] 24.25/10.01 [mark](x0) = [0 0 0 1]x0 + [0] 24.25/10.01 [0 0 0 1] [1], 24.25/10.01 24.25/10.01 [1 0 0 0] [1] 24.25/10.01 [0 0 0 0] [0] 24.25/10.01 [a__tail](x0) = [0 0 0 1]x0 + [0] 24.25/10.01 [0 0 0 1] [1], 24.25/10.01 24.25/10.01 [1 0 0 0] [1 1 0 1] [0] 24.25/10.01 [0 0 0 0] [0 0 0 0] [0] 24.25/10.01 [cons](x0, x1) = [0 0 0 1]x0 + [0 0 0 0]x1 + [0] 24.25/10.01 [0 0 0 1] [0 0 0 1] [1], 24.25/10.01 24.25/10.01 [0] 24.25/10.01 [0] 24.25/10.01 [zeros] = [0] 24.25/10.01 [0], 24.25/10.01 24.25/10.01 [1] 24.25/10.01 [0] 24.25/10.01 [0] = [0] 24.25/10.01 [0], 24.25/10.01 24.25/10.01 [1] 24.25/10.01 [0] 24.25/10.01 [a__zeros] = [0] 24.25/10.01 [1] 24.25/10.01 orientation: 24.25/10.01 [1 0 0 1] [1 1 0 2] [2] [1 0 0 1] [1 1 0 1] [1] 24.25/10.01 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 24.25/10.01 mark(cons(X1,X2)) = [0 0 0 1]X1 + [0 0 0 1]X2 + [1] >= [0 0 0 1]X1 + [0 0 0 0]X2 + [1] = cons(mark(X1),X2) 24.25/10.01 [0 0 0 1] [0 0 0 1] [2] [0 0 0 1] [0 0 0 1] [2] 24.25/10.01 24.25/10.01 [1 0 0 1] [2] [1 0 0 1] [2] 24.25/10.01 [0 0 0 0] [0] [0 0 0 0] [0] 24.25/10.01 mark(tail(X)) = [0 0 0 1]X + [1] >= [0 0 0 1]X + [1] = a__tail(mark(X)) 24.25/10.01 [0 0 0 1] [2] [0 0 0 1] [2] 24.25/10.01 24.25/10.01 [1] [1] 24.25/10.01 [0] [0] 24.25/10.01 a__zeros() = [0] >= [0] = cons(0(),zeros()) 24.25/10.01 [1] [1] 24.25/10.01 24.25/10.01 [1] [0] 24.25/10.01 [0] [0] 24.25/10.01 a__zeros() = [0] >= [0] = zeros() 24.25/10.01 [1] [0] 24.25/10.01 24.25/10.01 [1 0 0 0] [1 1 0 1] [1] [1 0 0 1] [1] 24.25/10.01 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 24.25/10.01 a__tail(cons(X,XS)) = [0 0 0 1]X + [0 0 0 1]XS + [1] >= [0 0 0 1]XS + [0] = mark(XS) 24.25/10.01 [0 0 0 1] [0 0 0 1] [2] [0 0 0 1] [1] 24.25/10.01 24.25/10.01 [1] [1] 24.25/10.01 [0] [0] 24.25/10.01 mark(zeros()) = [0] >= [0] = a__zeros() 24.25/10.01 [1] [1] 24.25/10.01 24.25/10.01 [2] [1] 24.25/10.01 [0] [0] 24.25/10.01 mark(0()) = [0] >= [0] = 0() 24.25/10.01 [1] [0] 24.25/10.01 24.25/10.01 [1 0 0 0] [1] [1 0 0 0] [0] 24.25/10.01 [0 0 0 0] [0] [0 0 0 0] [0] 24.25/10.01 a__tail(X) = [0 0 0 1]X + [0] >= [0 0 0 1]X + [0] = tail(X) 24.25/10.01 [0 0 0 1] [1] [0 0 0 1] [1] 24.25/10.01 problem: 24.25/10.01 strict: 24.25/10.01 24.25/10.01 weak: 24.25/10.01 mark(cons(X1,X2)) -> cons(mark(X1),X2) 24.25/10.01 mark(tail(X)) -> a__tail(mark(X)) 24.25/10.01 a__zeros() -> cons(0(),zeros()) 24.25/10.01 a__zeros() -> zeros() 24.25/10.01 a__tail(cons(X,XS)) -> mark(XS) 24.25/10.01 mark(zeros()) -> a__zeros() 24.25/10.01 mark(0()) -> 0() 24.25/10.01 a__tail(X) -> tail(X) 24.25/10.01 Qed 24.25/10.02 EOF