YES(?,O(n^2)) 19.84/8.66 YES(?,O(n^2)) 19.84/8.66 19.84/8.66 Problem: 19.84/8.66 a__zeros() -> cons(0(),zeros()) 19.84/8.66 a__tail(cons(X,XS)) -> mark(XS) 19.84/8.66 mark(zeros()) -> a__zeros() 19.84/8.66 mark(tail(X)) -> a__tail(mark(X)) 19.84/8.66 mark(cons(X1,X2)) -> cons(mark(X1),X2) 19.84/8.66 mark(0()) -> 0() 19.84/8.66 a__zeros() -> zeros() 19.84/8.66 a__tail(X) -> tail(X) 19.84/8.66 19.84/8.66 Proof: 19.84/8.66 Complexity Transformation Processor: 19.84/8.66 strict: 19.84/8.66 a__zeros() -> cons(0(),zeros()) 19.84/8.66 a__tail(cons(X,XS)) -> mark(XS) 19.84/8.66 mark(zeros()) -> a__zeros() 19.84/8.66 mark(tail(X)) -> a__tail(mark(X)) 19.84/8.66 mark(cons(X1,X2)) -> cons(mark(X1),X2) 19.84/8.66 mark(0()) -> 0() 19.84/8.66 a__zeros() -> zeros() 19.84/8.66 a__tail(X) -> tail(X) 19.84/8.66 weak: 19.84/8.66 19.84/8.66 Matrix Interpretation Processor: dim=1 19.84/8.66 19.84/8.66 max_matrix: 19.84/8.66 1 19.84/8.66 interpretation: 19.84/8.66 [tail](x0) = x0 + 32, 19.84/8.66 19.84/8.66 [mark](x0) = x0 + 228, 19.84/8.66 19.84/8.66 [a__tail](x0) = x0 + 191, 19.84/8.66 19.84/8.66 [cons](x0, x1) = x0 + x1 + 1, 19.84/8.66 19.84/8.66 [zeros] = 6, 19.84/8.66 19.84/8.66 [0] = 28, 19.84/8.66 19.84/8.66 [a__zeros] = 0 19.84/8.66 orientation: 19.84/8.66 a__zeros() = 0 >= 35 = cons(0(),zeros()) 19.84/8.66 19.84/8.66 a__tail(cons(X,XS)) = X + XS + 192 >= XS + 228 = mark(XS) 19.84/8.66 19.84/8.66 mark(zeros()) = 234 >= 0 = a__zeros() 19.84/8.66 19.84/8.66 mark(tail(X)) = X + 260 >= X + 419 = a__tail(mark(X)) 19.84/8.66 19.84/8.66 mark(cons(X1,X2)) = X1 + X2 + 229 >= X1 + X2 + 229 = cons(mark(X1),X2) 19.84/8.66 19.84/8.66 mark(0()) = 256 >= 28 = 0() 19.84/8.66 19.84/8.66 a__zeros() = 0 >= 6 = zeros() 19.84/8.66 19.84/8.66 a__tail(X) = X + 191 >= X + 32 = tail(X) 19.84/8.66 problem: 19.84/8.66 strict: 19.84/8.66 a__zeros() -> cons(0(),zeros()) 19.84/8.66 a__tail(cons(X,XS)) -> mark(XS) 19.84/8.66 mark(tail(X)) -> a__tail(mark(X)) 19.84/8.66 mark(cons(X1,X2)) -> cons(mark(X1),X2) 19.84/8.66 a__zeros() -> zeros() 19.84/8.66 weak: 19.84/8.66 mark(zeros()) -> a__zeros() 19.84/8.66 mark(0()) -> 0() 19.84/8.66 a__tail(X) -> tail(X) 19.84/8.66 Matrix Interpretation Processor: dim=1 19.84/8.66 19.84/8.66 max_matrix: 19.84/8.66 1 19.84/8.66 interpretation: 19.84/8.66 [tail](x0) = x0 + 5, 19.84/8.66 19.84/8.66 [mark](x0) = x0, 19.84/8.66 19.84/8.66 [a__tail](x0) = x0 + 5, 19.84/8.66 19.84/8.66 [cons](x0, x1) = x0 + x1 + 36, 19.84/8.66 19.84/8.66 [zeros] = 8, 19.84/8.66 19.84/8.66 [0] = 17, 19.84/8.66 19.84/8.66 [a__zeros] = 8 19.84/8.66 orientation: 19.84/8.66 a__zeros() = 8 >= 61 = cons(0(),zeros()) 19.84/8.66 19.84/8.66 a__tail(cons(X,XS)) = X + XS + 41 >= XS = mark(XS) 19.84/8.66 19.84/8.66 mark(tail(X)) = X + 5 >= X + 5 = a__tail(mark(X)) 19.84/8.66 19.84/8.66 mark(cons(X1,X2)) = X1 + X2 + 36 >= X1 + X2 + 36 = cons(mark(X1),X2) 19.84/8.66 19.84/8.66 a__zeros() = 8 >= 8 = zeros() 19.84/8.66 19.84/8.66 mark(zeros()) = 8 >= 8 = a__zeros() 19.84/8.66 19.84/8.66 mark(0()) = 17 >= 17 = 0() 19.84/8.66 19.84/8.66 a__tail(X) = X + 5 >= X + 5 = tail(X) 19.84/8.66 problem: 19.84/8.66 strict: 19.84/8.66 a__zeros() -> cons(0(),zeros()) 19.84/8.66 mark(tail(X)) -> a__tail(mark(X)) 19.84/8.66 mark(cons(X1,X2)) -> cons(mark(X1),X2) 19.84/8.66 a__zeros() -> zeros() 19.84/8.66 weak: 19.84/8.66 a__tail(cons(X,XS)) -> mark(XS) 19.84/8.66 mark(zeros()) -> a__zeros() 19.84/8.66 mark(0()) -> 0() 19.84/8.66 a__tail(X) -> tail(X) 19.84/8.66 Matrix Interpretation Processor: dim=1 19.84/8.66 19.84/8.66 max_matrix: 19.84/8.66 1 19.84/8.66 interpretation: 19.84/8.66 [tail](x0) = x0, 19.84/8.66 19.84/8.66 [mark](x0) = x0 + 128, 19.84/8.66 19.84/8.66 [a__tail](x0) = x0, 19.84/8.66 19.84/8.66 [cons](x0, x1) = x0 + x1 + 128, 19.84/8.66 19.84/8.66 [zeros] = 66, 19.84/8.66 19.84/8.66 [0] = 0, 19.84/8.66 19.84/8.66 [a__zeros] = 194 19.84/8.66 orientation: 19.84/8.66 a__zeros() = 194 >= 194 = cons(0(),zeros()) 19.84/8.66 19.84/8.66 mark(tail(X)) = X + 128 >= X + 128 = a__tail(mark(X)) 19.84/8.66 19.84/8.66 mark(cons(X1,X2)) = X1 + X2 + 256 >= X1 + X2 + 256 = cons(mark(X1),X2) 19.84/8.66 19.84/8.66 a__zeros() = 194 >= 66 = zeros() 19.84/8.66 19.84/8.66 a__tail(cons(X,XS)) = X + XS + 128 >= XS + 128 = mark(XS) 19.84/8.66 19.84/8.66 mark(zeros()) = 194 >= 194 = a__zeros() 19.84/8.66 19.84/8.66 mark(0()) = 128 >= 0 = 0() 19.84/8.66 19.84/8.66 a__tail(X) = X >= X = tail(X) 19.84/8.66 problem: 19.84/8.66 strict: 19.84/8.66 a__zeros() -> cons(0(),zeros()) 19.84/8.66 mark(tail(X)) -> a__tail(mark(X)) 19.84/8.66 mark(cons(X1,X2)) -> cons(mark(X1),X2) 19.84/8.66 weak: 19.84/8.66 a__zeros() -> zeros() 19.84/8.66 a__tail(cons(X,XS)) -> mark(XS) 19.84/8.66 mark(zeros()) -> a__zeros() 19.84/8.66 mark(0()) -> 0() 19.84/8.66 a__tail(X) -> tail(X) 19.84/8.66 Matrix Interpretation Processor: dim=1 19.84/8.66 19.84/8.66 max_matrix: 19.84/8.66 1 19.84/8.66 interpretation: 19.84/8.66 [tail](x0) = x0 + 1, 19.84/8.66 19.84/8.66 [mark](x0) = x0 + 2, 19.84/8.66 19.84/8.66 [a__tail](x0) = x0 + 1, 19.84/8.66 19.84/8.66 [cons](x0, x1) = x0 + x1 + 1, 19.84/8.66 19.84/8.66 [zeros] = 6, 19.84/8.66 19.84/8.66 [0] = 0, 19.84/8.66 19.84/8.66 [a__zeros] = 8 19.84/8.66 orientation: 19.84/8.66 a__zeros() = 8 >= 7 = cons(0(),zeros()) 19.84/8.67 19.84/8.67 mark(tail(X)) = X + 3 >= X + 3 = a__tail(mark(X)) 19.84/8.67 19.84/8.67 mark(cons(X1,X2)) = X1 + X2 + 3 >= X1 + X2 + 3 = cons(mark(X1),X2) 19.84/8.67 19.84/8.67 a__zeros() = 8 >= 6 = zeros() 19.84/8.67 19.84/8.67 a__tail(cons(X,XS)) = X + XS + 2 >= XS + 2 = mark(XS) 19.84/8.67 19.84/8.67 mark(zeros()) = 8 >= 8 = a__zeros() 19.84/8.67 19.84/8.67 mark(0()) = 2 >= 0 = 0() 19.84/8.67 19.84/8.67 a__tail(X) = X + 1 >= X + 1 = tail(X) 19.84/8.67 problem: 19.84/8.67 strict: 19.84/8.67 mark(tail(X)) -> a__tail(mark(X)) 19.84/8.67 mark(cons(X1,X2)) -> cons(mark(X1),X2) 19.84/8.67 weak: 19.84/8.67 a__zeros() -> cons(0(),zeros()) 19.84/8.67 a__zeros() -> zeros() 19.84/8.67 a__tail(cons(X,XS)) -> mark(XS) 19.84/8.67 mark(zeros()) -> a__zeros() 19.84/8.67 mark(0()) -> 0() 19.84/8.67 a__tail(X) -> tail(X) 19.84/8.67 Matrix Interpretation Processor: dim=2 19.84/8.67 19.84/8.67 max_matrix: 19.84/8.67 [1 4] 19.84/8.67 [0 1] 19.84/8.67 interpretation: 19.84/8.67 [1 4] [1] 19.84/8.67 [tail](x0) = [0 1]x0 + [1], 19.84/8.67 19.84/8.67 [1 4] 19.84/8.67 [mark](x0) = [0 1]x0, 19.84/8.67 19.84/8.67 [1 4] [4] 19.84/8.67 [a__tail](x0) = [0 1]x0 + [1], 19.84/8.67 19.84/8.67 19.84/8.67 [cons](x0, x1) = x0 + x1, 19.84/8.67 19.84/8.67 [0] 19.84/8.67 [zeros] = [3], 19.84/8.67 19.84/8.67 [1] 19.84/8.67 [0] = [0], 19.84/8.67 19.84/8.67 [1] 19.84/8.67 [a__zeros] = [3] 19.84/8.67 orientation: 19.84/8.67 [1 8] [5] [1 8] [4] 19.84/8.67 mark(tail(X)) = [0 1]X + [1] >= [0 1]X + [1] = a__tail(mark(X)) 19.84/8.67 19.84/8.67 [1 4] [1 4] [1 4] 19.84/8.67 mark(cons(X1,X2)) = [0 1]X1 + [0 1]X2 >= [0 1]X1 + X2 = cons(mark(X1),X2) 19.84/8.67 19.84/8.67 [1] [1] 19.84/8.67 a__zeros() = [3] >= [3] = cons(0(),zeros()) 19.84/8.67 19.84/8.67 [1] [0] 19.84/8.67 a__zeros() = [3] >= [3] = zeros() 19.84/8.67 19.84/8.67 [1 4] [1 4] [4] [1 4] 19.84/8.67 a__tail(cons(X,XS)) = [0 1]X + [0 1]XS + [1] >= [0 1]XS = mark(XS) 19.84/8.67 19.84/8.67 [12] [1] 19.84/8.67 mark(zeros()) = [3 ] >= [3] = a__zeros() 19.84/8.67 19.84/8.67 [1] [1] 19.84/8.67 mark(0()) = [0] >= [0] = 0() 19.84/8.67 19.84/8.67 [1 4] [4] [1 4] [1] 19.84/8.67 a__tail(X) = [0 1]X + [1] >= [0 1]X + [1] = tail(X) 19.84/8.67 problem: 19.84/8.67 strict: 19.84/8.67 mark(cons(X1,X2)) -> cons(mark(X1),X2) 19.84/8.67 weak: 19.84/8.67 mark(tail(X)) -> a__tail(mark(X)) 19.84/8.67 a__zeros() -> cons(0(),zeros()) 19.84/8.67 a__zeros() -> zeros() 19.84/8.67 a__tail(cons(X,XS)) -> mark(XS) 19.84/8.67 mark(zeros()) -> a__zeros() 19.84/8.67 mark(0()) -> 0() 19.84/8.67 a__tail(X) -> tail(X) 19.84/8.67 Matrix Interpretation Processor: dim=4 19.84/8.67 19.84/8.67 max_matrix: 19.84/8.67 [1 1 0 1] 19.84/8.67 [0 0 0 0] 19.84/8.67 [0 0 0 1] 19.84/8.67 [0 0 0 1] 19.84/8.67 interpretation: 19.84/8.67 [1 0 0 0] [0] 19.84/8.67 [0 0 0 0] [0] 19.84/8.67 [tail](x0) = [0 0 0 1]x0 + [0] 19.84/8.67 [0 0 0 1] [1], 19.84/8.67 19.84/8.67 [1 0 0 1] [1] 19.84/8.67 [0 0 0 0] [0] 19.84/8.67 [mark](x0) = [0 0 0 1]x0 + [0] 19.84/8.67 [0 0 0 1] [1], 19.84/8.67 19.84/8.67 [1 0 0 0] [1] 19.84/8.67 [0 0 0 0] [0] 19.84/8.67 [a__tail](x0) = [0 0 0 1]x0 + [0] 19.84/8.67 [0 0 0 1] [1], 19.84/8.67 19.84/8.67 [1 0 0 0] [1 1 0 1] [0] 19.84/8.67 [0 0 0 0] [0 0 0 0] [0] 19.84/8.67 [cons](x0, x1) = [0 0 0 1]x0 + [0 0 0 0]x1 + [0] 19.84/8.67 [0 0 0 1] [0 0 0 1] [1], 19.84/8.67 19.84/8.67 [0] 19.84/8.67 [0] 19.84/8.67 [zeros] = [0] 19.84/8.67 [0], 19.84/8.67 19.84/8.67 [1] 19.84/8.67 [0] 19.84/8.67 [0] = [0] 19.84/8.67 [0], 19.84/8.67 19.84/8.67 [1] 19.84/8.67 [0] 19.84/8.67 [a__zeros] = [0] 19.84/8.67 [1] 19.84/8.67 orientation: 19.84/8.67 [1 0 0 1] [1 1 0 2] [2] [1 0 0 1] [1 1 0 1] [1] 19.84/8.67 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 19.84/8.67 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) 19.84/8.67 [0 0 0 1] [0 0 0 1] [2] [0 0 0 1] [0 0 0 1] [2] 19.84/8.67 19.84/8.67 [1 0 0 1] [2] [1 0 0 1] [2] 19.84/8.67 [0 0 0 0] [0] [0 0 0 0] [0] 19.84/8.67 mark(tail(X)) = [0 0 0 1]X + [1] >= [0 0 0 1]X + [1] = a__tail(mark(X)) 19.84/8.67 [0 0 0 1] [2] [0 0 0 1] [2] 19.84/8.67 19.84/8.67 [1] [1] 19.84/8.67 [0] [0] 19.84/8.67 a__zeros() = [0] >= [0] = cons(0(),zeros()) 19.84/8.67 [1] [1] 19.84/8.67 19.84/8.67 [1] [0] 19.84/8.67 [0] [0] 19.84/8.67 a__zeros() = [0] >= [0] = zeros() 19.84/8.67 [1] [0] 19.84/8.67 19.84/8.67 [1 0 0 0] [1 1 0 1] [1] [1 0 0 1] [1] 19.84/8.67 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 19.84/8.67 a__tail(cons(X,XS)) = [0 0 0 1]X + [0 0 0 1]XS + [1] >= [0 0 0 1]XS + [0] = mark(XS) 19.84/8.67 [0 0 0 1] [0 0 0 1] [2] [0 0 0 1] [1] 19.84/8.67 19.84/8.67 [1] [1] 19.84/8.67 [0] [0] 19.84/8.67 mark(zeros()) = [0] >= [0] = a__zeros() 19.84/8.67 [1] [1] 19.84/8.67 19.84/8.67 [2] [1] 19.84/8.67 [0] [0] 19.84/8.67 mark(0()) = [0] >= [0] = 0() 19.84/8.67 [1] [0] 19.84/8.67 19.84/8.67 [1 0 0 0] [1] [1 0 0 0] [0] 19.84/8.67 [0 0 0 0] [0] [0 0 0 0] [0] 19.84/8.67 a__tail(X) = [0 0 0 1]X + [0] >= [0 0 0 1]X + [0] = tail(X) 19.84/8.67 [0 0 0 1] [1] [0 0 0 1] [1] 19.84/8.67 problem: 19.84/8.67 strict: 19.84/8.67 19.84/8.67 weak: 19.84/8.67 mark(cons(X1,X2)) -> cons(mark(X1),X2) 19.84/8.67 mark(tail(X)) -> a__tail(mark(X)) 19.84/8.67 a__zeros() -> cons(0(),zeros()) 19.84/8.67 a__zeros() -> zeros() 19.84/8.67 a__tail(cons(X,XS)) -> mark(XS) 19.84/8.67 mark(zeros()) -> a__zeros() 19.84/8.67 mark(0()) -> 0() 19.84/8.67 a__tail(X) -> tail(X) 19.84/8.67 Qed 19.84/8.68 EOF