YES(?,O(n^3)) 52.54/15.43 YES(?,O(n^3)) 52.54/15.44 52.54/15.44 Problem: 52.54/15.44 active(zeros()) -> mark(cons(0(),zeros())) 52.54/15.44 active(tail(cons(X,XS))) -> mark(XS) 52.54/15.44 mark(zeros()) -> active(zeros()) 52.54/15.44 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 52.54/15.44 mark(0()) -> active(0()) 52.54/15.44 mark(tail(X)) -> active(tail(mark(X))) 52.54/15.44 cons(mark(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,mark(X2)) -> cons(X1,X2) 52.54/15.44 cons(active(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,active(X2)) -> cons(X1,X2) 52.54/15.44 tail(mark(X)) -> tail(X) 52.54/15.44 tail(active(X)) -> tail(X) 52.54/15.44 52.54/15.44 Proof: 52.54/15.44 Complexity Transformation Processor: 52.54/15.44 strict: 52.54/15.44 active(zeros()) -> mark(cons(0(),zeros())) 52.54/15.44 active(tail(cons(X,XS))) -> mark(XS) 52.54/15.44 mark(zeros()) -> active(zeros()) 52.54/15.44 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 52.54/15.44 mark(0()) -> active(0()) 52.54/15.44 mark(tail(X)) -> active(tail(mark(X))) 52.54/15.44 cons(mark(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,mark(X2)) -> cons(X1,X2) 52.54/15.44 cons(active(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,active(X2)) -> cons(X1,X2) 52.54/15.44 tail(mark(X)) -> tail(X) 52.54/15.44 tail(active(X)) -> tail(X) 52.54/15.44 weak: 52.54/15.44 52.54/15.44 Matrix Interpretation Processor: dim=1 52.54/15.44 52.54/15.44 max_matrix: 52.54/15.44 1 52.54/15.44 interpretation: 52.54/15.44 [tail](x0) = x0 + 2, 52.54/15.44 52.54/15.44 [mark](x0) = x0 + 2, 52.54/15.44 52.54/15.44 [cons](x0, x1) = x0 + x1 + 1, 52.54/15.44 52.54/15.44 [0] = 10, 52.54/15.44 52.54/15.44 [active](x0) = x0 + 1, 52.54/15.44 52.54/15.44 [zeros] = 2 52.54/15.44 orientation: 52.54/15.44 active(zeros()) = 3 >= 15 = mark(cons(0(),zeros())) 52.54/15.44 52.54/15.44 active(tail(cons(X,XS))) = X + XS + 4 >= XS + 2 = mark(XS) 52.54/15.44 52.54/15.44 mark(zeros()) = 4 >= 3 = active(zeros()) 52.54/15.44 52.54/15.44 mark(cons(X1,X2)) = X1 + X2 + 3 >= X1 + X2 + 4 = active(cons(mark(X1),X2)) 52.54/15.44 52.54/15.44 mark(0()) = 12 >= 11 = active(0()) 52.54/15.44 52.54/15.44 mark(tail(X)) = X + 4 >= X + 5 = active(tail(mark(X))) 52.54/15.44 52.54/15.44 cons(mark(X1),X2) = X1 + X2 + 3 >= X1 + X2 + 1 = cons(X1,X2) 52.54/15.44 52.54/15.44 cons(X1,mark(X2)) = X1 + X2 + 3 >= X1 + X2 + 1 = cons(X1,X2) 52.54/15.44 52.54/15.44 cons(active(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = cons(X1,X2) 52.54/15.44 52.54/15.44 cons(X1,active(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = cons(X1,X2) 52.54/15.44 52.54/15.44 tail(mark(X)) = X + 4 >= X + 2 = tail(X) 52.54/15.44 52.54/15.44 tail(active(X)) = X + 3 >= X + 2 = tail(X) 52.54/15.44 problem: 52.54/15.44 strict: 52.54/15.44 active(zeros()) -> mark(cons(0(),zeros())) 52.54/15.44 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 52.54/15.44 mark(tail(X)) -> active(tail(mark(X))) 52.54/15.44 weak: 52.54/15.44 active(tail(cons(X,XS))) -> mark(XS) 52.54/15.44 mark(zeros()) -> active(zeros()) 52.54/15.44 mark(0()) -> active(0()) 52.54/15.44 cons(mark(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,mark(X2)) -> cons(X1,X2) 52.54/15.44 cons(active(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,active(X2)) -> cons(X1,X2) 52.54/15.44 tail(mark(X)) -> tail(X) 52.54/15.44 tail(active(X)) -> tail(X) 52.54/15.44 Splitting Processor: 52.54/15.44 strict: 52.54/15.44 mark(tail(X)) -> active(tail(mark(X))) 52.54/15.44 weak: 52.54/15.44 active(tail(cons(X,XS))) -> mark(XS) 52.54/15.44 mark(zeros()) -> active(zeros()) 52.54/15.44 mark(0()) -> active(0()) 52.54/15.44 cons(mark(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,mark(X2)) -> cons(X1,X2) 52.54/15.44 cons(active(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,active(X2)) -> cons(X1,X2) 52.54/15.44 tail(mark(X)) -> tail(X) 52.54/15.44 tail(active(X)) -> tail(X) 52.54/15.44 active(zeros()) -> mark(cons(0(),zeros())) 52.54/15.44 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 52.54/15.44 Matrix Interpretation Processor: dim=3 52.54/15.44 52.54/15.44 max_matrix: 52.54/15.44 [1 0 1] 52.54/15.44 [0 0 1] 52.54/15.44 [0 0 1] 52.54/15.44 interpretation: 52.54/15.44 [1 0 0] [0] 52.54/15.44 [tail](x0) = [0 0 0]x0 + [0] 52.54/15.44 [0 0 1] [1], 52.54/15.44 52.54/15.44 [1 0 1] 52.54/15.44 [mark](x0) = [0 0 1]x0 52.54/15.44 [0 0 1] , 52.54/15.44 52.54/15.44 [1 0 0] [1 0 1] 52.54/15.44 [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 52.54/15.44 [0 0 1] [0 0 1] , 52.54/15.44 52.54/15.44 [0] 52.54/15.44 [0] = [0] 52.54/15.44 [0], 52.54/15.44 52.54/15.44 [1 0 0] 52.54/15.44 [active](x0) = [0 0 1]x0 52.54/15.44 [0 0 1] , 52.54/15.44 52.54/15.44 [0] 52.54/15.44 [zeros] = [0] 52.54/15.44 [0] 52.54/15.44 orientation: 52.54/15.44 [1 0 1] [1] [1 0 1] [0] 52.54/15.44 mark(tail(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = active(tail(mark(X))) 52.54/15.44 [0 0 1] [1] [0 0 1] [1] 52.54/15.44 52.54/15.44 [1 0 0] [1 0 1] [0] [1 0 1] 52.54/15.44 active(tail(cons(X,XS))) = [0 0 1]X + [0 0 1]XS + [1] >= [0 0 1]XS = mark(XS) 52.54/15.44 [0 0 1] [0 0 1] [1] [0 0 1] 52.54/15.44 52.54/15.44 [0] [0] 52.54/15.44 mark(zeros()) = [0] >= [0] = active(zeros()) 52.54/15.44 [0] [0] 52.54/15.44 52.54/15.44 [0] [0] 52.54/15.44 mark(0()) = [0] >= [0] = active(0()) 52.54/15.44 [0] [0] 52.54/15.44 52.54/15.44 [1 0 1] [1 0 1] [1 0 0] [1 0 1] 52.54/15.44 cons(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 52.54/15.44 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 52.54/15.44 52.54/15.44 [1 0 0] [1 0 2] [1 0 0] [1 0 1] 52.54/15.44 cons(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 52.54/15.44 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 52.54/15.44 52.54/15.44 [1 0 0] [1 0 1] [1 0 0] [1 0 1] 52.54/15.44 cons(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 52.54/15.44 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 52.54/15.44 52.54/15.44 [1 0 0] [1 0 1] [1 0 0] [1 0 1] 52.54/15.44 cons(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 52.54/15.44 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 52.54/15.44 52.54/15.44 [1 0 1] [0] [1 0 0] [0] 52.54/15.44 tail(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = tail(X) 52.54/15.44 [0 0 1] [1] [0 0 1] [1] 52.54/15.44 52.54/15.44 [1 0 0] [0] [1 0 0] [0] 52.54/15.44 tail(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = tail(X) 52.54/15.44 [0 0 1] [1] [0 0 1] [1] 52.54/15.44 52.54/15.44 [0] [0] 52.54/15.44 active(zeros()) = [0] >= [0] = mark(cons(0(),zeros())) 52.54/15.44 [0] [0] 52.54/15.44 52.54/15.44 [1 0 1] [1 0 2] [1 0 1] [1 0 1] 52.54/15.44 mark(cons(X1,X2)) = [0 0 1]X1 + [0 0 1]X2 >= [0 0 1]X1 + [0 0 1]X2 = active(cons(mark(X1),X2)) 52.54/15.44 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 52.54/15.44 problem: 52.54/15.44 strict: 52.54/15.44 52.54/15.44 weak: 52.54/15.44 mark(tail(X)) -> active(tail(mark(X))) 52.54/15.44 active(tail(cons(X,XS))) -> mark(XS) 52.54/15.44 mark(zeros()) -> active(zeros()) 52.54/15.44 mark(0()) -> active(0()) 52.54/15.44 cons(mark(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,mark(X2)) -> cons(X1,X2) 52.54/15.44 cons(active(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,active(X2)) -> cons(X1,X2) 52.54/15.44 tail(mark(X)) -> tail(X) 52.54/15.44 tail(active(X)) -> tail(X) 52.54/15.44 active(zeros()) -> mark(cons(0(),zeros())) 52.54/15.44 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 52.54/15.44 Qed 52.54/15.44 52.54/15.44 strict: 52.54/15.44 active(zeros()) -> mark(cons(0(),zeros())) 52.54/15.44 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 52.54/15.44 weak: 52.54/15.44 mark(tail(X)) -> active(tail(mark(X))) 52.54/15.44 active(tail(cons(X,XS))) -> mark(XS) 52.54/15.44 mark(zeros()) -> active(zeros()) 52.54/15.44 mark(0()) -> active(0()) 52.54/15.44 cons(mark(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,mark(X2)) -> cons(X1,X2) 52.54/15.44 cons(active(X1),X2) -> cons(X1,X2) 52.54/15.44 cons(X1,active(X2)) -> cons(X1,X2) 52.54/15.44 tail(mark(X)) -> tail(X) 52.54/15.44 tail(active(X)) -> tail(X) 52.54/15.44 Matrix Interpretation Processor: dim=4 52.54/15.44 52.54/15.44 max_matrix: 52.54/15.44 [1 1 0 1] 52.54/15.44 [0 0 1 1] 52.54/15.44 [0 0 1 1] 52.54/15.44 [0 0 0 0] 52.54/15.44 interpretation: 52.54/15.44 [1 1 0 1] [0] 52.54/15.44 [0 0 1 1] [0] 52.54/15.44 [tail](x0) = [0 0 1 1]x0 + [1] 52.54/15.44 [0 0 0 0] [1], 52.54/15.44 52.54/15.44 [1 1 0 1] 52.54/15.44 [0 0 0 0] 52.54/15.44 [mark](x0) = [0 0 1 1]x0 52.54/15.44 [0 0 0 0] , 52.54/15.44 52.54/15.44 [1 1 0 1] [1 1 0 0] 52.54/15.44 [0 0 0 0] [0 0 0 0] 52.54/15.44 [cons](x0, x1) = [0 0 0 0]x0 + [0 0 1 1]x1 52.54/15.44 [0 0 0 0] [0 0 0 0] , 52.54/15.44 52.54/15.44 [0] 52.54/15.45 [0] 52.54/15.45 [0] = [0] 52.54/15.45 [0], 52.54/15.45 52.54/15.45 [1 1 0 1] 52.54/15.45 [0 0 0 0] 52.54/15.45 [active](x0) = [0 0 1 1]x0 52.54/15.45 [0 0 0 0] , 52.54/15.45 52.54/15.45 [0] 52.54/15.45 [0] 52.54/15.45 [zeros] = [0] 52.54/15.45 [1] 52.54/15.45 orientation: 52.54/15.45 [1] [0] 52.54/15.45 [0] [0] 52.54/15.45 active(zeros()) = [1] >= [1] = mark(cons(0(),zeros())) 52.54/15.45 [0] [0] 52.54/15.45 52.54/15.45 [1 1 0 1] [1 1 0 0] [1 1 0 1] [1 1 0 0] 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 mark(cons(X1,X2)) = [0 0 0 0]X1 + [0 0 1 1]X2 >= [0 0 0 0]X1 + [0 0 1 1]X2 = active(cons(mark(X1),X2)) 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 52.54/15.45 [1 1 1 2] [1] [1 1 1 2] [1] 52.54/15.45 [0 0 0 0] [0] [0 0 0 0] [0] 52.54/15.45 mark(tail(X)) = [0 0 1 1]X + [2] >= [0 0 1 1]X + [2] = active(tail(mark(X))) 52.54/15.45 [0 0 0 0] [0] [0 0 0 0] [0] 52.54/15.45 52.54/15.45 [1 1 0 1] [1 1 1 1] [1] [1 1 0 1] 52.54/15.45 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 52.54/15.45 active(tail(cons(X,XS))) = [0 0 0 0]X + [0 0 1 1]XS + [2] >= [0 0 1 1]XS = mark(XS) 52.54/15.45 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 52.54/15.45 52.54/15.45 [1] [1] 52.54/15.45 [0] [0] 52.54/15.45 mark(zeros()) = [1] >= [1] = active(zeros()) 52.54/15.45 [0] [0] 52.54/15.45 52.54/15.45 [0] [0] 52.54/15.45 [0] [0] 52.54/15.45 mark(0()) = [0] >= [0] = active(0()) 52.54/15.45 [0] [0] 52.54/15.45 52.54/15.45 [1 1 0 1] [1 1 0 0] [1 1 0 1] [1 1 0 0] 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 cons(mark(X1),X2) = [0 0 0 0]X1 + [0 0 1 1]X2 >= [0 0 0 0]X1 + [0 0 1 1]X2 = cons(X1,X2) 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 52.54/15.45 [1 1 0 1] [1 1 0 1] [1 1 0 1] [1 1 0 0] 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 cons(X1,mark(X2)) = [0 0 0 0]X1 + [0 0 1 1]X2 >= [0 0 0 0]X1 + [0 0 1 1]X2 = cons(X1,X2) 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 52.54/15.45 [1 1 0 1] [1 1 0 0] [1 1 0 1] [1 1 0 0] 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 cons(active(X1),X2) = [0 0 0 0]X1 + [0 0 1 1]X2 >= [0 0 0 0]X1 + [0 0 1 1]X2 = cons(X1,X2) 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 52.54/15.45 [1 1 0 1] [1 1 0 1] [1 1 0 1] [1 1 0 0] 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 cons(X1,active(X2)) = [0 0 0 0]X1 + [0 0 1 1]X2 >= [0 0 0 0]X1 + [0 0 1 1]X2 = cons(X1,X2) 52.54/15.45 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 52.54/15.45 52.54/15.45 [1 1 0 1] [0] [1 1 0 1] [0] 52.54/15.45 [0 0 1 1] [0] [0 0 1 1] [0] 52.54/15.45 tail(mark(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = tail(X) 52.54/15.45 [0 0 0 0] [1] [0 0 0 0] [1] 52.54/15.45 52.54/15.45 [1 1 0 1] [0] [1 1 0 1] [0] 52.54/15.45 [0 0 1 1] [0] [0 0 1 1] [0] 52.54/15.45 tail(active(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = tail(X) 52.54/15.46 [0 0 0 0] [1] [0 0 0 0] [1] 52.54/15.46 problem: 52.54/15.46 strict: 52.54/15.46 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 52.54/15.46 weak: 52.54/15.46 active(zeros()) -> mark(cons(0(),zeros())) 52.54/15.46 mark(tail(X)) -> active(tail(mark(X))) 52.54/15.46 active(tail(cons(X,XS))) -> mark(XS) 52.54/15.46 mark(zeros()) -> active(zeros()) 52.54/15.46 mark(0()) -> active(0()) 52.54/15.46 cons(mark(X1),X2) -> cons(X1,X2) 52.54/15.46 cons(X1,mark(X2)) -> cons(X1,X2) 52.54/15.46 cons(active(X1),X2) -> cons(X1,X2) 52.54/15.46 cons(X1,active(X2)) -> cons(X1,X2) 52.54/15.46 tail(mark(X)) -> tail(X) 52.54/15.46 tail(active(X)) -> tail(X) 52.54/15.46 Matrix Interpretation Processor: dim=4 52.54/15.46 52.54/15.46 max_matrix: 52.54/15.46 [1 1 1 1] 52.54/15.46 [0 1 1 2] 52.54/15.46 [0 0 1 1] 52.54/15.46 [0 0 0 0] 52.54/15.46 interpretation: 52.54/15.46 [1 1 1 1] [0] 52.54/15.46 [0 1 1 2] [2] 52.54/15.46 [tail](x0) = [0 0 1 1]x0 + [0] 52.54/15.46 [0 0 0 0] [0], 52.54/15.46 52.54/15.46 [1 1 0 1] 52.54/15.46 [0 1 0 1] 52.54/15.46 [mark](x0) = [0 0 1 1]x0 52.54/15.46 [0 0 0 0] , 52.54/15.46 52.54/15.46 [1 1 0 1] [1 0 0 0] [0] 52.54/15.46 [0 1 1 2] [0 1 0 0] [1] 52.54/15.46 [cons](x0, x1) = [0 0 0 0]x0 + [0 0 1 1]x1 + [0] 52.54/15.46 [0 0 0 0] [0 0 0 0] [0], 52.54/15.46 52.54/15.46 [0] 52.54/15.46 [0] 52.54/15.46 [0] = [0] 52.54/15.46 [0], 52.54/15.46 52.54/15.46 [1 0 0 1] 52.54/15.46 [0 1 0 1] 52.54/15.46 [active](x0) = [0 0 1 1]x0 52.54/15.46 [0 0 0 0] , 52.54/15.46 52.54/15.46 [0] 52.54/15.46 [0] 52.54/15.46 [zeros] = [1] 52.54/15.46 [1] 52.54/15.46 orientation: 52.54/15.46 [1 2 1 3] [1 1 0 0] [1] [1 2 0 2] [1 0 0 0] [0] 52.54/15.46 [0 1 1 2] [0 1 0 0] [1] [0 1 1 2] [0 1 0 0] [1] 52.54/15.46 mark(cons(X1,X2)) = [0 0 0 0]X1 + [0 0 1 1]X2 + [0] >= [0 0 0 0]X1 + [0 0 1 1]X2 + [0] = active(cons(mark(X1),X2)) 52.54/15.46 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 52.54/15.46 52.54/15.46 [1] [1] 52.54/15.46 [1] [1] 52.54/15.46 active(zeros()) = [2] >= [2] = mark(cons(0(),zeros())) 52.54/15.46 [0] [0] 52.54/15.46 52.54/15.46 [1 2 2 3] [2] [1 2 1 3] [0] 52.54/15.46 [0 1 1 2] [2] [0 1 1 2] [2] 52.54/15.46 mark(tail(X)) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = active(tail(mark(X))) 52.54/15.46 [0 0 0 0] [0] [0 0 0 0] [0] 52.54/15.46 52.54/15.46 [1 2 1 3] [1 1 1 1] [1] [1 1 0 1] 52.54/15.46 [0 1 1 2] [0 1 1 1] [3] [0 1 0 1] 52.54/15.46 active(tail(cons(X,XS))) = [0 0 0 0]X + [0 0 1 1]XS + [0] >= [0 0 1 1]XS = mark(XS) 52.54/15.46 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 52.54/15.46 52.54/15.46 [1] [1] 52.54/15.46 [1] [1] 52.54/15.46 mark(zeros()) = [2] >= [2] = active(zeros()) 52.54/15.46 [0] [0] 52.54/15.46 52.54/15.46 [0] [0] 52.54/15.46 [0] [0] 52.54/15.46 mark(0()) = [0] >= [0] = active(0()) 52.54/15.46 [0] [0] 52.54/15.46 52.54/15.46 [1 2 0 2] [1 0 0 0] [0] [1 1 0 1] [1 0 0 0] [0] 52.54/15.46 [0 1 1 2] [0 1 0 0] [1] [0 1 1 2] [0 1 0 0] [1] 52.54/15.46 cons(mark(X1),X2) = [0 0 0 0]X1 + [0 0 1 1]X2 + [0] >= [0 0 0 0]X1 + [0 0 1 1]X2 + [0] = cons(X1,X2) 52.54/15.46 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 52.54/15.46 52.54/15.46 [1 1 0 1] [1 1 0 1] [0] [1 1 0 1] [1 0 0 0] [0] 52.54/15.46 [0 1 1 2] [0 1 0 1] [1] [0 1 1 2] [0 1 0 0] [1] 52.54/15.46 cons(X1,mark(X2)) = [0 0 0 0]X1 + [0 0 1 1]X2 + [0] >= [0 0 0 0]X1 + [0 0 1 1]X2 + [0] = cons(X1,X2) 52.54/15.46 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 52.54/15.46 52.54/15.46 [1 1 0 2] [1 0 0 0] [0] [1 1 0 1] [1 0 0 0] [0] 52.54/15.46 [0 1 1 2] [0 1 0 0] [1] [0 1 1 2] [0 1 0 0] [1] 52.54/15.46 cons(active(X1),X2) = [0 0 0 0]X1 + [0 0 1 1]X2 + [0] >= [0 0 0 0]X1 + [0 0 1 1]X2 + [0] = cons(X1,X2) 52.54/15.46 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 52.54/15.46 52.54/15.46 [1 1 0 1] [1 0 0 1] [0] [1 1 0 1] [1 0 0 0] [0] 52.54/15.46 [0 1 1 2] [0 1 0 1] [1] [0 1 1 2] [0 1 0 0] [1] 52.54/15.46 cons(X1,active(X2)) = [0 0 0 0]X1 + [0 0 1 1]X2 + [0] >= [0 0 0 0]X1 + [0 0 1 1]X2 + [0] = cons(X1,X2) 52.54/15.46 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 52.54/15.46 52.54/15.46 [1 2 1 3] [0] [1 1 1 1] [0] 52.54/15.46 [0 1 1 2] [2] [0 1 1 2] [2] 52.54/15.46 tail(mark(X)) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = tail(X) 52.54/15.46 [0 0 0 0] [0] [0 0 0 0] [0] 52.54/15.46 52.54/15.46 [1 1 1 3] [0] [1 1 1 1] [0] 52.54/15.46 [0 1 1 2] [2] [0 1 1 2] [2] 52.54/15.46 tail(active(X)) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = tail(X) 52.54/15.46 [0 0 0 0] [0] [0 0 0 0] [0] 52.54/15.46 problem: 52.54/15.46 strict: 52.54/15.46 52.54/15.46 weak: 52.54/15.46 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 52.54/15.46 active(zeros()) -> mark(cons(0(),zeros())) 52.54/15.46 mark(tail(X)) -> active(tail(mark(X))) 52.54/15.46 active(tail(cons(X,XS))) -> mark(XS) 52.54/15.46 mark(zeros()) -> active(zeros()) 52.54/15.46 mark(0()) -> active(0()) 52.54/15.46 cons(mark(X1),X2) -> cons(X1,X2) 52.54/15.46 cons(X1,mark(X2)) -> cons(X1,X2) 52.54/15.46 cons(active(X1),X2) -> cons(X1,X2) 52.54/15.46 cons(X1,active(X2)) -> cons(X1,X2) 52.54/15.46 tail(mark(X)) -> tail(X) 52.54/15.46 tail(active(X)) -> tail(X) 52.54/15.46 Qed 52.54/15.47 EOF