YES(?,O(n^3)) 281.93/154.58 YES(?,O(n^3)) 281.93/154.59 281.93/154.59 Problem: 281.93/154.59 a__f(0()) -> cons(0(),f(s(0()))) 281.93/154.59 a__f(s(0())) -> a__f(a__p(s(0()))) 281.93/154.59 a__p(s(0())) -> 0() 281.93/154.59 mark(f(X)) -> a__f(mark(X)) 281.93/154.59 mark(p(X)) -> a__p(mark(X)) 281.93/154.59 mark(0()) -> 0() 281.93/154.59 mark(cons(X1,X2)) -> cons(mark(X1),X2) 281.93/154.59 mark(s(X)) -> s(mark(X)) 281.93/154.59 a__f(X) -> f(X) 281.93/154.59 a__p(X) -> p(X) 281.93/154.59 281.93/154.59 Proof: 281.93/154.59 Complexity Transformation Processor: 281.93/154.59 strict: 281.93/154.59 a__f(0()) -> cons(0(),f(s(0()))) 281.93/154.59 a__f(s(0())) -> a__f(a__p(s(0()))) 281.93/154.59 a__p(s(0())) -> 0() 281.93/154.59 mark(f(X)) -> a__f(mark(X)) 281.93/154.59 mark(p(X)) -> a__p(mark(X)) 281.93/154.59 mark(0()) -> 0() 281.93/154.59 mark(cons(X1,X2)) -> cons(mark(X1),X2) 281.93/154.59 mark(s(X)) -> s(mark(X)) 281.93/154.59 a__f(X) -> f(X) 281.93/154.59 a__p(X) -> p(X) 281.93/154.59 weak: 281.93/154.59 281.93/154.59 Matrix Interpretation Processor: dim=1 281.93/154.59 281.93/154.59 max_matrix: 281.93/154.59 1 281.93/154.59 interpretation: 281.93/154.59 [p](x0) = x0, 281.93/154.59 281.93/154.59 [mark](x0) = x0 + 13, 281.93/154.59 281.93/154.59 [a__p](x0) = x0 + 11, 281.93/154.59 281.93/154.59 [cons](x0, x1) = x0 + x1 + 1, 281.93/154.59 281.93/154.59 [f](x0) = x0 + 11, 281.93/154.59 281.93/154.59 [s](x0) = x0 + 2, 281.93/154.59 281.93/154.59 [a__f](x0) = x0 + 9, 281.93/154.59 281.93/154.59 [0] = 7 281.93/154.59 orientation: 281.93/154.59 a__f(0()) = 16 >= 28 = cons(0(),f(s(0()))) 281.93/154.59 281.93/154.59 a__f(s(0())) = 18 >= 29 = a__f(a__p(s(0()))) 281.93/154.59 281.93/154.59 a__p(s(0())) = 20 >= 7 = 0() 281.93/154.59 281.93/154.59 mark(f(X)) = X + 24 >= X + 22 = a__f(mark(X)) 281.93/154.59 281.93/154.59 mark(p(X)) = X + 13 >= X + 24 = a__p(mark(X)) 281.93/154.59 281.93/154.59 mark(0()) = 20 >= 7 = 0() 281.93/154.59 281.93/154.59 mark(cons(X1,X2)) = X1 + X2 + 14 >= X1 + X2 + 14 = cons(mark(X1),X2) 281.93/154.59 281.93/154.59 mark(s(X)) = X + 15 >= X + 15 = s(mark(X)) 281.93/154.59 281.93/154.59 a__f(X) = X + 9 >= X + 11 = f(X) 281.93/154.59 281.93/154.59 a__p(X) = X + 11 >= X = p(X) 281.93/154.59 problem: 281.93/154.59 strict: 281.93/154.59 a__f(0()) -> cons(0(),f(s(0()))) 281.93/154.59 a__f(s(0())) -> a__f(a__p(s(0()))) 281.93/154.59 mark(p(X)) -> a__p(mark(X)) 281.93/154.59 mark(cons(X1,X2)) -> cons(mark(X1),X2) 281.93/154.59 mark(s(X)) -> s(mark(X)) 281.93/154.59 a__f(X) -> f(X) 281.93/154.59 weak: 281.93/154.59 a__p(s(0())) -> 0() 281.93/154.59 mark(f(X)) -> a__f(mark(X)) 281.93/154.59 mark(0()) -> 0() 281.93/154.59 a__p(X) -> p(X) 281.93/154.59 Matrix Interpretation Processor: dim=3 281.93/154.59 281.93/154.59 max_matrix: 281.93/154.59 [1 1 1] 281.93/154.59 [0 0 0] 281.93/154.59 [0 0 1] 281.93/154.59 interpretation: 281.93/154.59 [1 0 0] 281.93/154.59 [p](x0) = [0 0 0]x0 281.93/154.59 [0 0 1] , 281.93/154.59 281.93/154.59 [1 0 1] [1] 281.93/154.59 [mark](x0) = [0 0 0]x0 + [0] 281.93/154.59 [0 0 1] [0], 281.93/154.59 281.93/154.59 [1 0 0] 281.93/154.59 [a__p](x0) = [0 0 0]x0 281.93/154.59 [0 0 1] , 281.93/154.59 281.93/154.59 [1 1 0] [1 0 0] 281.93/154.59 [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 281.93/154.59 [0 0 1] [0 0 0] , 281.93/154.59 281.93/154.59 [1 0 0] 281.93/154.59 [f](x0) = [0 0 0]x0 281.93/154.59 [0 0 1] , 281.93/154.59 281.93/154.59 [1 1 1] [0] 281.93/154.59 [s](x0) = [0 0 0]x0 + [0] 281.93/154.59 [0 0 1] [1], 281.93/154.59 281.93/154.59 [1 0 0] 281.93/154.59 [a__f](x0) = [0 0 0]x0 281.93/154.59 [0 0 1] , 281.93/154.59 281.93/154.59 [0] 281.93/154.59 [0] = [0] 281.93/154.59 [0] 281.93/154.59 orientation: 281.93/154.59 [0] [0] 281.93/154.59 a__f(0()) = [0] >= [0] = cons(0(),f(s(0()))) 281.93/154.59 [0] [0] 281.93/154.59 281.93/154.59 [0] [0] 281.93/154.59 a__f(s(0())) = [0] >= [0] = a__f(a__p(s(0()))) 281.93/154.59 [1] [1] 281.93/154.59 281.93/154.59 [1 0 1] [1] [1 0 1] [1] 281.93/154.59 mark(p(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__p(mark(X)) 281.93/154.59 [0 0 1] [0] [0 0 1] [0] 281.93/154.59 281.93/154.59 [1 1 1] [1 0 0] [1] [1 0 1] [1 0 0] [1] 281.93/154.59 mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = cons(mark(X1),X2) 281.93/154.59 [0 0 1] [0 0 0] [0] [0 0 1] [0 0 0] [0] 281.93/154.59 281.93/154.59 [1 1 2] [2] [1 0 2] [1] 281.93/154.59 mark(s(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = s(mark(X)) 281.93/154.59 [0 0 1] [1] [0 0 1] [1] 281.93/154.59 281.93/154.59 [1 0 0] [1 0 0] 281.93/154.59 a__f(X) = [0 0 0]X >= [0 0 0]X = f(X) 281.93/154.59 [0 0 1] [0 0 1] 281.93/154.59 281.93/154.59 [0] [0] 281.93/154.59 a__p(s(0())) = [0] >= [0] = 0() 281.93/154.59 [1] [0] 281.93/154.59 281.93/154.59 [1 0 1] [1] [1 0 1] [1] 281.93/154.59 mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__f(mark(X)) 281.93/154.59 [0 0 1] [0] [0 0 1] [0] 281.93/154.59 281.93/154.59 [1] [0] 281.93/154.59 mark(0()) = [0] >= [0] = 0() 281.93/154.59 [0] [0] 281.93/154.59 281.93/154.59 [1 0 0] [1 0 0] 281.93/154.59 a__p(X) = [0 0 0]X >= [0 0 0]X = p(X) 281.93/154.59 [0 0 1] [0 0 1] 281.93/154.59 problem: 281.93/154.59 strict: 281.93/154.59 a__f(0()) -> cons(0(),f(s(0()))) 281.93/154.59 a__f(s(0())) -> a__f(a__p(s(0()))) 281.93/154.59 mark(p(X)) -> a__p(mark(X)) 281.93/154.59 mark(cons(X1,X2)) -> cons(mark(X1),X2) 281.93/154.59 a__f(X) -> f(X) 281.93/154.59 weak: 281.93/154.59 mark(s(X)) -> s(mark(X)) 281.93/154.59 a__p(s(0())) -> 0() 281.93/154.59 mark(f(X)) -> a__f(mark(X)) 281.93/154.59 mark(0()) -> 0() 281.93/154.59 a__p(X) -> p(X) 281.93/154.59 Splitting Processor: 281.93/154.59 strict: 281.93/154.59 mark(cons(X1,X2)) -> cons(mark(X1),X2) 281.93/154.59 weak: 281.93/154.59 mark(s(X)) -> s(mark(X)) 281.93/154.59 a__p(s(0())) -> 0() 281.93/154.59 mark(f(X)) -> a__f(mark(X)) 281.93/154.59 mark(0()) -> 0() 281.93/154.59 a__p(X) -> p(X) 281.93/154.59 a__f(0()) -> cons(0(),f(s(0()))) 281.93/154.59 a__f(s(0())) -> a__f(a__p(s(0()))) 281.93/154.59 mark(p(X)) -> a__p(mark(X)) 281.93/154.59 a__f(X) -> f(X) 281.93/154.59 Matrix Interpretation Processor: dim=4 281.93/154.59 281.93/154.59 max_matrix: 281.93/154.59 [1 1 1 1] 281.93/154.59 [0 0 1 0] 281.93/154.59 [0 0 0 0] 281.93/154.59 [0 0 0 1] 281.93/154.59 interpretation: 281.93/154.59 [1 0 0 0] 281.93/154.59 [0 0 0 0] 281.93/154.59 [p](x0) = [0 0 0 0]x0 281.93/154.59 [0 0 0 1] , 281.93/154.59 281.93/154.59 [1 0 0 1] [1] 281.93/154.59 [0 0 0 0] [0] 281.93/154.59 [mark](x0) = [0 0 0 0]x0 + [0] 281.93/154.59 [0 0 0 1] [0], 281.93/154.59 281.93/154.59 [1 0 1 0] 281.93/154.59 [0 0 1 0] 281.93/154.59 [a__p](x0) = [0 0 0 0]x0 281.93/154.59 [0 0 0 1] , 281.93/154.59 281.93/154.59 [1 0 0 0] [1 0 0 0] [0] 281.93/154.59 [0 0 0 0] [0 0 0 0] [0] 281.93/154.59 [cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0] 281.93/154.59 [0 0 0 1] [0 0 0 0] [1], 281.93/154.59 281.93/154.59 [1 1 0 1] [0] 281.93/154.59 [0 0 0 0] [0] 281.93/154.59 [f](x0) = [0 0 0 0]x0 + [0] 281.93/154.59 [0 0 0 1] [1], 281.93/154.59 281.93/154.59 [1 1 1 0] [0] 281.93/154.59 [0 0 0 0] [0] 281.93/154.59 [s](x0) = [0 0 0 0]x0 + [0] 281.93/154.59 [0 0 0 1] [1], 281.93/154.59 281.93/154.59 [1 1 0 1] [1] 281.93/154.59 [0 0 0 0] [0] 281.93/154.59 [a__f](x0) = [0 0 0 0]x0 + [0] 281.93/154.59 [0 0 0 1] [1], 281.93/154.59 281.93/154.59 [0] 281.93/154.59 [0] 281.93/154.59 [0] = [0] 281.93/154.59 [1] 281.93/154.59 orientation: 281.93/154.59 [1 0 0 1] [1 0 0 0] [2] [1 0 0 1] [1 0 0 0] [1] 281.93/154.59 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 281.93/154.59 mark(cons(X1,X2)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0] = cons(mark(X1),X2) 281.93/154.59 [0 0 0 1] [0 0 0 0] [1] [0 0 0 1] [0 0 0 0] [1] 281.93/154.59 281.93/154.59 [1 1 1 1] [2] [1 0 0 1] [1] 281.93/154.59 [0 0 0 0] [0] [0 0 0 0] [0] 281.93/154.59 mark(s(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = s(mark(X)) 281.93/154.59 [0 0 0 1] [1] [0 0 0 1] [1] 281.93/154.59 281.93/154.59 [0] [0] 281.93/154.59 [0] [0] 281.93/154.59 a__p(s(0())) = [0] >= [0] = 0() 281.93/154.59 [2] [1] 281.93/154.59 281.93/154.59 [1 1 0 2] [2] [1 0 0 2] [2] 281.93/154.59 [0 0 0 0] [0] [0 0 0 0] [0] 281.93/154.59 mark(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__f(mark(X)) 281.93/154.59 [0 0 0 1] [1] [0 0 0 1] [1] 281.93/154.59 281.93/154.59 [2] [0] 281.93/154.59 [0] [0] 281.93/154.59 mark(0()) = [0] >= [0] = 0() 281.93/154.59 [1] [1] 281.93/154.59 281.93/154.59 [1 0 1 0] [1 0 0 0] 281.93/154.59 [0 0 1 0] [0 0 0 0] 281.93/154.59 a__p(X) = [0 0 0 0]X >= [0 0 0 0]X = p(X) 281.93/154.59 [0 0 0 1] [0 0 0 1] 281.93/154.59 281.93/154.59 [2] [2] 281.93/154.59 [0] [0] 281.93/154.59 a__f(0()) = [0] >= [0] = cons(0(),f(s(0()))) 282.03/154.60 [2] [2] 282.03/154.60 282.03/154.60 [3] [3] 282.03/154.60 [0] [0] 282.03/154.60 a__f(s(0())) = [0] >= [0] = a__f(a__p(s(0()))) 282.03/154.60 [3] [3] 282.03/154.60 282.03/154.60 [1 0 0 1] [1] [1 0 0 1] [1] 282.03/154.60 [0 0 0 0] [0] [0 0 0 0] [0] 282.03/154.60 mark(p(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__p(mark(X)) 282.03/154.60 [0 0 0 1] [0] [0 0 0 1] [0] 282.03/154.60 282.03/154.60 [1 1 0 1] [1] [1 1 0 1] [0] 282.03/154.60 [0 0 0 0] [0] [0 0 0 0] [0] 282.03/154.60 a__f(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(X) 282.03/154.60 [0 0 0 1] [1] [0 0 0 1] [1] 282.03/154.60 problem: 282.03/154.60 strict: 282.03/154.60 282.03/154.60 weak: 282.03/154.60 mark(cons(X1,X2)) -> cons(mark(X1),X2) 282.03/154.60 mark(s(X)) -> s(mark(X)) 282.03/154.60 a__p(s(0())) -> 0() 282.03/154.60 mark(f(X)) -> a__f(mark(X)) 282.03/154.60 mark(0()) -> 0() 282.03/154.60 a__p(X) -> p(X) 282.03/154.60 a__f(0()) -> cons(0(),f(s(0()))) 282.03/154.60 a__f(s(0())) -> a__f(a__p(s(0()))) 282.03/154.60 mark(p(X)) -> a__p(mark(X)) 282.03/154.60 a__f(X) -> f(X) 282.03/154.60 Qed 282.03/154.60 282.03/154.60 strict: 282.03/154.60 a__f(0()) -> cons(0(),f(s(0()))) 282.03/154.60 a__f(s(0())) -> a__f(a__p(s(0()))) 282.03/154.60 mark(p(X)) -> a__p(mark(X)) 282.03/154.60 a__f(X) -> f(X) 282.03/154.60 weak: 282.03/154.60 mark(cons(X1,X2)) -> cons(mark(X1),X2) 282.03/154.60 mark(s(X)) -> s(mark(X)) 282.03/154.60 a__p(s(0())) -> 0() 282.03/154.60 mark(f(X)) -> a__f(mark(X)) 282.03/154.60 mark(0()) -> 0() 282.03/154.60 a__p(X) -> p(X) 282.03/154.60 Matrix Interpretation Processor: dim=3 282.03/154.60 282.03/154.60 max_matrix: 282.03/154.60 [1 1 1] 282.03/154.60 [0 1 1] 282.03/154.60 [0 0 1] 282.03/154.60 interpretation: 282.03/154.60 [1 0 0] [0] 282.03/154.60 [p](x0) = [0 1 0]x0 + [1] 282.03/154.60 [0 0 0] [0], 282.03/154.60 282.03/154.60 [1 1 0] 282.03/154.60 [mark](x0) = [0 1 0]x0 282.03/154.60 [0 0 1] , 282.03/154.60 282.03/154.60 [1 0 0] [0] 282.03/154.60 [a__p](x0) = [0 1 0]x0 + [1] 282.03/154.60 [0 0 0] [0], 282.03/154.60 282.03/154.60 [1 0 1] [1 0 1] 282.03/154.60 [cons](x0, x1) = [0 1 0]x0 + [0 0 1]x1 282.03/154.60 [0 0 0] [0 0 1] , 282.03/154.60 282.03/154.60 [1 0 0] 282.03/154.60 [f](x0) = [0 1 1]x0 282.03/154.60 [0 0 0] , 282.03/154.60 282.03/154.60 [1 0 0] [0] 282.03/154.60 [s](x0) = [0 1 0]x0 + [1] 282.03/154.60 [0 0 0] [1], 282.03/154.60 282.03/154.60 [1 0 0] 282.03/154.60 [a__f](x0) = [0 1 1]x0 282.03/154.60 [0 0 0] , 282.03/154.60 282.03/154.60 [0] 282.03/154.60 [0] = [1] 282.03/154.60 [0] 282.03/154.60 orientation: 282.03/154.60 [0] [0] 282.03/154.60 a__f(0()) = [1] >= [1] = cons(0(),f(s(0()))) 282.03/154.60 [0] [0] 282.03/154.60 282.03/154.60 [0] [0] 282.03/154.60 a__f(s(0())) = [3] >= [3] = a__f(a__p(s(0()))) 282.03/154.60 [0] [0] 282.03/154.60 282.03/154.60 [1 1 0] [1] [1 1 0] [0] 282.03/154.60 mark(p(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = a__p(mark(X)) 282.03/154.60 [0 0 0] [0] [0 0 0] [0] 282.03/154.60 282.03/154.60 [1 0 0] [1 0 0] 282.03/154.60 a__f(X) = [0 1 1]X >= [0 1 1]X = f(X) 282.03/154.60 [0 0 0] [0 0 0] 282.03/154.60 282.03/154.60 [1 1 1] [1 0 2] [1 1 1] [1 0 1] 282.03/154.60 mark(cons(X1,X2)) = [0 1 0]X1 + [0 0 1]X2 >= [0 1 0]X1 + [0 0 1]X2 = cons(mark(X1),X2) 282.03/154.60 [0 0 0] [0 0 1] [0 0 0] [0 0 1] 282.03/154.60 282.03/154.60 [1 1 0] [1] [1 1 0] [0] 282.03/154.60 mark(s(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = s(mark(X)) 282.03/154.60 [0 0 0] [1] [0 0 0] [1] 282.03/154.60 282.03/154.60 [0] [0] 282.03/154.60 a__p(s(0())) = [3] >= [1] = 0() 282.03/154.60 [0] [0] 282.03/154.60 282.03/154.60 [1 1 1] [1 1 0] 282.03/154.60 mark(f(X)) = [0 1 1]X >= [0 1 1]X = a__f(mark(X)) 282.03/154.60 [0 0 0] [0 0 0] 282.03/154.60 282.03/154.60 [1] [0] 282.03/154.60 mark(0()) = [1] >= [1] = 0() 282.03/154.60 [0] [0] 282.03/154.60 282.03/154.60 [1 0 0] [0] [1 0 0] [0] 282.03/154.60 a__p(X) = [0 1 0]X + [1] >= [0 1 0]X + [1] = p(X) 282.03/154.60 [0 0 0] [0] [0 0 0] [0] 282.03/154.60 problem: 282.03/154.60 strict: 282.03/154.60 a__f(0()) -> cons(0(),f(s(0()))) 282.03/154.60 a__f(s(0())) -> a__f(a__p(s(0()))) 282.03/154.60 a__f(X) -> f(X) 282.03/154.60 weak: 282.03/154.60 mark(p(X)) -> a__p(mark(X)) 282.03/154.60 mark(cons(X1,X2)) -> cons(mark(X1),X2) 282.03/154.60 mark(s(X)) -> s(mark(X)) 282.03/154.60 a__p(s(0())) -> 0() 282.03/154.60 mark(f(X)) -> a__f(mark(X)) 282.03/154.60 mark(0()) -> 0() 282.03/154.60 a__p(X) -> p(X) 282.03/154.60 Matrix Interpretation Processor: dim=3 282.03/154.60 282.03/154.60 max_matrix: 282.03/154.60 [1 1 1] 282.03/154.60 [0 1 1] 282.03/154.60 [0 0 1] 282.03/154.60 interpretation: 282.03/154.60 [1 0 0] 282.03/154.60 [p](x0) = [0 1 0]x0 282.03/154.60 [0 0 0] , 282.03/154.60 282.03/154.60 [1 1 0] 282.03/154.60 [mark](x0) = [0 1 0]x0 282.03/154.60 [0 0 1] , 282.03/154.60 282.03/154.60 [1 0 0] 282.03/154.60 [a__p](x0) = [0 1 0]x0 282.03/154.60 [0 0 0] , 282.03/154.60 282.03/154.60 [1 0 0] [1 0 0] 282.03/154.60 [cons](x0, x1) = [0 1 1]x0 + [0 0 0]x1 282.03/154.60 [0 0 0] [0 0 0] , 282.03/154.60 282.03/154.60 [1 0 0] 282.03/154.60 [f](x0) = [0 1 1]x0 282.03/154.60 [0 0 0] , 282.03/154.60 282.03/154.60 [1 0 0] [0] 282.03/154.60 [s](x0) = [0 1 1]x0 + [0] 282.03/154.60 [0 0 0] [1], 282.03/154.60 282.03/154.60 [1 0 1] 282.03/154.60 [a__f](x0) = [0 1 1]x0 282.03/154.60 [0 0 0] , 282.03/154.60 282.03/154.60 [0] 282.03/154.60 [0] = [0] 282.03/154.60 [0] 282.03/154.60 orientation: 282.03/154.60 [0] [0] 282.03/154.60 a__f(0()) = [0] >= [0] = cons(0(),f(s(0()))) 282.03/154.60 [0] [0] 282.03/154.60 282.03/154.60 [1] [0] 282.03/154.60 a__f(s(0())) = [1] >= [0] = a__f(a__p(s(0()))) 282.03/154.60 [0] [0] 282.03/154.60 282.03/154.60 [1 0 1] [1 0 0] 282.03/154.60 a__f(X) = [0 1 1]X >= [0 1 1]X = f(X) 282.03/154.60 [0 0 0] [0 0 0] 282.03/154.60 282.03/154.60 [1 1 0] [1 1 0] 282.03/154.60 mark(p(X)) = [0 1 0]X >= [0 1 0]X = a__p(mark(X)) 282.03/154.60 [0 0 0] [0 0 0] 282.03/154.60 282.03/154.60 [1 1 1] [1 0 0] [1 1 0] [1 0 0] 282.03/154.60 mark(cons(X1,X2)) = [0 1 1]X1 + [0 0 0]X2 >= [0 1 1]X1 + [0 0 0]X2 = cons(mark(X1),X2) 282.03/154.60 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 282.03/154.60 282.03/154.60 [1 1 1] [0] [1 1 0] [0] 282.03/154.60 mark(s(X)) = [0 1 1]X + [0] >= [0 1 1]X + [0] = s(mark(X)) 282.03/154.60 [0 0 0] [1] [0 0 0] [1] 282.03/154.60 282.03/154.60 [0] [0] 282.03/154.60 a__p(s(0())) = [0] >= [0] = 0() 282.03/154.60 [0] [0] 282.03/154.60 282.03/154.60 [1 1 1] [1 1 1] 282.03/154.60 mark(f(X)) = [0 1 1]X >= [0 1 1]X = a__f(mark(X)) 282.03/154.60 [0 0 0] [0 0 0] 282.03/154.60 282.03/154.60 [0] [0] 282.03/154.60 mark(0()) = [0] >= [0] = 0() 282.03/154.60 [0] [0] 282.03/154.60 282.03/154.60 [1 0 0] [1 0 0] 282.03/154.60 a__p(X) = [0 1 0]X >= [0 1 0]X = p(X) 282.03/154.60 [0 0 0] [0 0 0] 282.03/154.60 problem: 282.03/154.60 strict: 282.03/154.60 a__f(0()) -> cons(0(),f(s(0()))) 282.03/154.60 a__f(X) -> f(X) 282.03/154.60 weak: 282.03/154.60 a__f(s(0())) -> a__f(a__p(s(0()))) 282.03/154.60 mark(p(X)) -> a__p(mark(X)) 282.03/154.60 mark(cons(X1,X2)) -> cons(mark(X1),X2) 282.03/154.60 mark(s(X)) -> s(mark(X)) 282.03/154.60 a__p(s(0())) -> 0() 282.03/154.60 mark(f(X)) -> a__f(mark(X)) 282.03/154.60 mark(0()) -> 0() 282.03/154.60 a__p(X) -> p(X) 282.03/154.60 Splitting Processor: 282.03/154.60 strict: 282.03/154.60 a__f(0()) -> cons(0(),f(s(0()))) 282.03/154.60 weak: 282.03/154.60 a__f(s(0())) -> a__f(a__p(s(0()))) 282.03/154.60 mark(p(X)) -> a__p(mark(X)) 282.03/154.60 mark(cons(X1,X2)) -> cons(mark(X1),X2) 282.03/154.60 mark(s(X)) -> s(mark(X)) 282.03/154.60 a__p(s(0())) -> 0() 282.03/154.60 mark(f(X)) -> a__f(mark(X)) 282.03/154.60 mark(0()) -> 0() 282.03/154.61 a__p(X) -> p(X) 282.03/154.61 a__f(X) -> f(X) 282.03/154.61 Matrix Interpretation Processor: dim=4 282.03/154.61 282.03/154.61 max_matrix: 282.03/154.61 [1 1 1 1] 282.03/154.61 [0 1 1 1] 282.03/154.61 [0 0 1 0] 282.03/154.61 [0 0 0 0] 282.03/154.61 interpretation: 282.03/154.61 [1 0 0 0] 282.03/154.61 [0 1 1 0] 282.03/154.61 [p](x0) = [0 0 0 0]x0 282.03/154.61 [0 0 0 0] , 282.03/154.61 282.03/154.61 [1 1 0 0] [0] 282.03/154.61 [0 1 0 0] [0] 282.03/154.61 [mark](x0) = [0 0 0 0]x0 + [0] 282.03/154.61 [0 0 0 0] [1], 282.03/154.61 282.03/154.61 [1 0 0 0] [0] 282.03/154.61 [0 1 1 0] [0] 282.03/154.61 [a__p](x0) = [0 0 0 0]x0 + [0] 282.03/154.61 [0 0 0 0] [1], 282.03/154.61 282.03/154.61 [1 0 1 0] [1 0 1 1] [0] 282.03/154.61 [0 1 1 0] [0 1 1 1] [0] 282.03/154.61 [cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0] 282.03/154.61 [0 0 0 0] [0 0 0 0] [1], 282.03/154.61 282.03/154.61 [1 0 0 0] [0] 282.03/154.61 [0 1 0 0] [1] 282.03/154.61 [f](x0) = [0 0 0 0]x0 + [0] 282.03/154.61 [0 0 0 0] [0], 282.03/154.61 282.03/154.61 [1 0 0 0] 282.03/154.61 [0 1 1 0] 282.03/154.61 [s](x0) = [0 0 0 0]x0 282.03/154.61 [0 0 0 0] , 282.03/154.61 282.03/154.61 [1 0 1 0] [1] 282.03/154.61 [0 1 1 0] [1] 282.03/154.61 [a__f](x0) = [0 0 1 0]x0 + [0] 282.03/154.61 [0 0 0 0] [1], 282.03/154.61 282.03/154.61 [0] 282.03/154.61 [0] 282.03/154.61 [0] = [0] 282.03/154.61 [0] 282.03/154.61 orientation: 282.03/154.61 [1 0 1 0] [1] [1 0 0 0] [0] 282.03/154.61 [0 1 1 0] [1] [0 1 0 0] [1] 282.03/154.61 a__f(X) = [0 0 1 0]X + [0] >= [0 0 0 0]X + [0] = f(X) 282.03/154.61 [0 0 0 0] [1] [0 0 0 0] [0] 282.03/154.61 282.03/154.61 [1] [0] 282.03/154.61 [1] [1] 282.03/154.61 a__f(0()) = [0] >= [0] = cons(0(),f(s(0()))) 282.03/154.61 [1] [1] 282.03/154.61 282.03/154.61 [1] [1] 282.03/154.61 [1] [1] 282.03/154.61 a__f(s(0())) = [0] >= [0] = a__f(a__p(s(0()))) 282.03/154.61 [1] [1] 282.03/154.61 282.03/154.61 [1 1 1 0] [0] [1 1 0 0] [0] 282.03/154.61 [0 1 1 0] [0] [0 1 0 0] [0] 282.03/154.61 mark(p(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__p(mark(X)) 282.03/154.61 [0 0 0 0] [1] [0 0 0 0] [1] 282.03/154.61 282.03/154.61 [1 1 2 0] [1 1 2 2] [0] [1 1 0 0] [1 0 1 1] [0] 282.03/154.61 [0 1 1 0] [0 1 1 1] [0] [0 1 0 0] [0 1 1 1] [0] 282.03/154.61 mark(cons(X1,X2)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0] = cons(mark(X1),X2) 282.03/154.61 [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [1] 282.03/154.61 282.03/154.61 [1 1 1 0] [0] [1 1 0 0] 282.03/154.61 [0 1 1 0] [0] [0 1 0 0] 282.03/154.61 mark(s(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X = s(mark(X)) 282.03/154.61 [0 0 0 0] [1] [0 0 0 0] 282.03/154.61 282.03/154.61 [0] [0] 282.03/154.61 [0] [0] 282.03/154.61 a__p(s(0())) = [0] >= [0] = 0() 282.03/154.61 [1] [0] 282.03/154.61 282.03/154.61 [1 1 0 0] [1] [1 1 0 0] [1] 282.03/154.61 [0 1 0 0] [1] [0 1 0 0] [1] 282.03/154.61 mark(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__f(mark(X)) 282.03/154.61 [0 0 0 0] [1] [0 0 0 0] [1] 282.03/154.61 282.03/154.61 [0] [0] 282.03/154.61 [0] [0] 282.03/154.61 mark(0()) = [0] >= [0] = 0() 282.03/154.61 [1] [0] 282.03/154.61 282.03/154.61 [1 0 0 0] [0] [1 0 0 0] 282.03/154.61 [0 1 1 0] [0] [0 1 1 0] 282.03/154.61 a__p(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X = p(X) 282.03/154.61 [0 0 0 0] [1] [0 0 0 0] 282.03/154.61 problem: 282.03/154.61 strict: 282.03/154.61 282.03/154.61 weak: 282.03/154.61 a__f(X) -> f(X) 282.03/154.61 a__f(0()) -> cons(0(),f(s(0()))) 282.03/154.61 a__f(s(0())) -> a__f(a__p(s(0()))) 282.03/154.61 mark(p(X)) -> a__p(mark(X)) 282.03/154.61 mark(cons(X1,X2)) -> cons(mark(X1),X2) 282.03/154.61 mark(s(X)) -> s(mark(X)) 282.03/154.61 a__p(s(0())) -> 0() 282.03/154.61 mark(f(X)) -> a__f(mark(X)) 282.03/154.61 mark(0()) -> 0() 282.03/154.61 a__p(X) -> p(X) 282.03/154.61 Qed 282.03/154.61 282.03/154.61 strict: 282.03/154.61 a__f(X) -> f(X) 282.03/154.61 weak: 282.03/154.61 a__f(0()) -> cons(0(),f(s(0()))) 282.03/154.61 a__f(s(0())) -> a__f(a__p(s(0()))) 282.03/154.61 mark(p(X)) -> a__p(mark(X)) 282.03/154.61 mark(cons(X1,X2)) -> cons(mark(X1),X2) 282.03/154.61 mark(s(X)) -> s(mark(X)) 282.03/154.61 a__p(s(0())) -> 0() 282.03/154.61 mark(f(X)) -> a__f(mark(X)) 282.03/154.61 mark(0()) -> 0() 282.03/154.61 a__p(X) -> p(X) 282.03/154.61 Bounds Processor: 282.03/154.61 bound: 2 282.03/154.61 enrichment: match 282.03/154.61 automaton: 282.03/154.61 final states: {9} 282.03/154.61 transitions: 282.03/154.61 cons1(13,15) -> 9* 282.03/154.61 cons1(21,20) -> 9* 282.03/154.61 01() -> 16,13 282.03/154.61 f1(14) -> 15* 282.03/154.61 f1(16) -> 9* 282.03/154.61 s1(13) -> 14* 282.03/154.61 mark1(14) -> 14* 282.03/154.61 mark1(21) -> 21* 282.03/154.61 mark1(16) -> 16* 282.03/154.61 mark1(18) -> 21* 282.03/154.61 mark1(13) -> 13* 282.03/154.61 a__f1(16) -> 9* 282.03/154.61 a__p1(14) -> 16* 282.03/154.61 p1(14) -> 16* 282.03/154.61 cons2(18,20) -> 9* 282.03/154.61 a__f0(9) -> 9* 282.03/154.61 02() -> 21,18 282.03/154.61 00() -> 9* 282.03/154.61 f2(19) -> 20* 282.03/154.61 cons0(9,9) -> 9* 282.03/154.61 s2(18) -> 19* 282.03/154.61 f0(9) -> 9* 282.03/154.61 s0(9) -> 9* 282.03/154.61 a__p0(9) -> 9* 282.03/154.61 mark0(9) -> 9* 282.03/154.61 p0(9) -> 9* 282.03/154.61 problem: 282.03/154.61 strict: 282.03/154.61 282.03/154.61 weak: 282.03/154.61 a__f(0()) -> cons(0(),f(s(0()))) 282.03/154.61 a__f(s(0())) -> a__f(a__p(s(0()))) 282.03/154.61 mark(p(X)) -> a__p(mark(X)) 282.03/154.61 mark(cons(X1,X2)) -> cons(mark(X1),X2) 282.03/154.61 mark(s(X)) -> s(mark(X)) 282.03/154.61 a__p(s(0())) -> 0() 282.03/154.61 mark(f(X)) -> a__f(mark(X)) 282.03/154.61 mark(0()) -> 0() 282.03/154.61 a__p(X) -> p(X) 282.03/154.61 a__f(X) -> f(X) 282.03/154.61 Qed 282.03/154.62 EOF