YES(?,O(n^3)) 194.12/76.18 YES(?,O(n^3)) 194.12/76.19 194.12/76.19 Problem: 194.12/76.19 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.12/76.19 active(f(s(0()))) -> mark(f(p(s(0())))) 194.12/76.19 active(p(s(0()))) -> mark(0()) 194.12/76.19 mark(f(X)) -> active(f(mark(X))) 194.12/76.19 mark(0()) -> active(0()) 194.12/76.19 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.12/76.19 mark(s(X)) -> active(s(mark(X))) 194.12/76.19 mark(p(X)) -> active(p(mark(X))) 194.12/76.19 f(mark(X)) -> f(X) 194.12/76.19 f(active(X)) -> f(X) 194.12/76.19 cons(mark(X1),X2) -> cons(X1,X2) 194.12/76.19 cons(X1,mark(X2)) -> cons(X1,X2) 194.12/76.19 cons(active(X1),X2) -> cons(X1,X2) 194.12/76.19 cons(X1,active(X2)) -> cons(X1,X2) 194.12/76.19 s(mark(X)) -> s(X) 194.12/76.19 s(active(X)) -> s(X) 194.12/76.19 p(mark(X)) -> p(X) 194.12/76.19 p(active(X)) -> p(X) 194.12/76.19 194.12/76.19 Proof: 194.12/76.19 Complexity Transformation Processor: 194.12/76.19 strict: 194.12/76.19 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.12/76.19 active(f(s(0()))) -> mark(f(p(s(0())))) 194.12/76.19 active(p(s(0()))) -> mark(0()) 194.12/76.19 mark(f(X)) -> active(f(mark(X))) 194.12/76.19 mark(0()) -> active(0()) 194.12/76.19 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.12/76.19 mark(s(X)) -> active(s(mark(X))) 194.12/76.19 mark(p(X)) -> active(p(mark(X))) 194.12/76.19 f(mark(X)) -> f(X) 194.12/76.19 f(active(X)) -> f(X) 194.12/76.19 cons(mark(X1),X2) -> cons(X1,X2) 194.12/76.19 cons(X1,mark(X2)) -> cons(X1,X2) 194.12/76.19 cons(active(X1),X2) -> cons(X1,X2) 194.12/76.19 cons(X1,active(X2)) -> cons(X1,X2) 194.12/76.19 s(mark(X)) -> s(X) 194.12/76.19 s(active(X)) -> s(X) 194.12/76.19 p(mark(X)) -> p(X) 194.12/76.19 p(active(X)) -> p(X) 194.12/76.19 weak: 194.12/76.19 194.12/76.19 Matrix Interpretation Processor: dim=1 194.12/76.19 194.12/76.19 max_matrix: 194.12/76.19 1 194.12/76.19 interpretation: 194.12/76.19 [p](x0) = x0 + 160, 194.12/76.19 194.12/76.19 [mark](x0) = x0, 194.12/76.19 194.12/76.19 [cons](x0, x1) = x0 + x1 + 122, 194.12/76.19 194.12/76.19 [s](x0) = x0 + 96, 194.12/76.19 194.12/76.19 [active](x0) = x0 + 12, 194.12/76.19 194.12/76.19 [f](x0) = x0 + 68, 194.12/76.19 194.12/76.19 [0] = 0 194.12/76.19 orientation: 194.12/76.19 active(f(0())) = 80 >= 286 = mark(cons(0(),f(s(0())))) 194.12/76.19 194.12/76.19 active(f(s(0()))) = 176 >= 324 = mark(f(p(s(0())))) 194.12/76.19 194.12/76.19 active(p(s(0()))) = 268 >= 0 = mark(0()) 194.12/76.19 194.12/76.19 mark(f(X)) = X + 68 >= X + 80 = active(f(mark(X))) 194.12/76.19 194.12/76.19 mark(0()) = 0 >= 12 = active(0()) 194.12/76.19 194.12/76.19 mark(cons(X1,X2)) = X1 + X2 + 122 >= X1 + X2 + 134 = active(cons(mark(X1),X2)) 194.12/76.19 194.12/76.19 mark(s(X)) = X + 96 >= X + 108 = active(s(mark(X))) 194.12/76.19 194.12/76.19 mark(p(X)) = X + 160 >= X + 172 = active(p(mark(X))) 194.12/76.19 194.12/76.19 f(mark(X)) = X + 68 >= X + 68 = f(X) 194.12/76.19 194.12/76.19 f(active(X)) = X + 80 >= X + 68 = f(X) 194.12/76.19 194.12/76.19 cons(mark(X1),X2) = X1 + X2 + 122 >= X1 + X2 + 122 = cons(X1,X2) 194.12/76.19 194.12/76.19 cons(X1,mark(X2)) = X1 + X2 + 122 >= X1 + X2 + 122 = cons(X1,X2) 194.12/76.19 194.12/76.19 cons(active(X1),X2) = X1 + X2 + 134 >= X1 + X2 + 122 = cons(X1,X2) 194.12/76.19 194.12/76.19 cons(X1,active(X2)) = X1 + X2 + 134 >= X1 + X2 + 122 = cons(X1,X2) 194.12/76.19 194.12/76.19 s(mark(X)) = X + 96 >= X + 96 = s(X) 194.12/76.19 194.12/76.19 s(active(X)) = X + 108 >= X + 96 = s(X) 194.12/76.19 194.12/76.19 p(mark(X)) = X + 160 >= X + 160 = p(X) 194.12/76.19 194.12/76.19 p(active(X)) = X + 172 >= X + 160 = p(X) 194.12/76.19 problem: 194.12/76.19 strict: 194.12/76.19 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.12/76.19 active(f(s(0()))) -> mark(f(p(s(0())))) 194.12/76.19 mark(f(X)) -> active(f(mark(X))) 194.12/76.19 mark(0()) -> active(0()) 194.12/76.19 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.12/76.19 mark(s(X)) -> active(s(mark(X))) 194.12/76.19 mark(p(X)) -> active(p(mark(X))) 194.12/76.19 f(mark(X)) -> f(X) 194.12/76.19 cons(mark(X1),X2) -> cons(X1,X2) 194.12/76.19 cons(X1,mark(X2)) -> cons(X1,X2) 194.12/76.19 s(mark(X)) -> s(X) 194.12/76.19 p(mark(X)) -> p(X) 194.12/76.19 weak: 194.12/76.19 active(p(s(0()))) -> mark(0()) 194.12/76.19 f(active(X)) -> f(X) 194.12/76.19 cons(active(X1),X2) -> cons(X1,X2) 194.12/76.19 cons(X1,active(X2)) -> cons(X1,X2) 194.12/76.19 s(active(X)) -> s(X) 194.12/76.19 p(active(X)) -> p(X) 194.12/76.19 Matrix Interpretation Processor: dim=1 194.12/76.19 194.12/76.19 max_matrix: 194.12/76.19 1 194.12/76.19 interpretation: 194.12/76.19 [p](x0) = x0 + 2, 194.12/76.19 194.12/76.19 [mark](x0) = x0 + 9, 194.12/76.19 194.12/76.19 [cons](x0, x1) = x0 + x1 + 1, 194.12/76.19 194.12/76.19 [s](x0) = x0 + 7, 194.12/76.19 194.12/76.19 [active](x0) = x0, 194.12/76.19 194.12/76.19 [f](x0) = x0 + 3, 194.12/76.19 194.12/76.19 [0] = 0 194.12/76.19 orientation: 194.12/76.19 active(f(0())) = 3 >= 20 = mark(cons(0(),f(s(0())))) 194.12/76.19 194.12/76.19 active(f(s(0()))) = 10 >= 21 = mark(f(p(s(0())))) 194.12/76.19 194.12/76.19 mark(f(X)) = X + 12 >= X + 12 = active(f(mark(X))) 194.12/76.19 194.12/76.19 mark(0()) = 9 >= 0 = active(0()) 194.12/76.19 194.12/76.19 mark(cons(X1,X2)) = X1 + X2 + 10 >= X1 + X2 + 10 = active(cons(mark(X1),X2)) 194.12/76.19 194.12/76.19 mark(s(X)) = X + 16 >= X + 16 = active(s(mark(X))) 194.12/76.19 194.12/76.19 mark(p(X)) = X + 11 >= X + 11 = active(p(mark(X))) 194.12/76.19 194.12/76.19 f(mark(X)) = X + 12 >= X + 3 = f(X) 194.12/76.19 194.12/76.19 cons(mark(X1),X2) = X1 + X2 + 10 >= X1 + X2 + 1 = cons(X1,X2) 194.12/76.19 194.12/76.19 cons(X1,mark(X2)) = X1 + X2 + 10 >= X1 + X2 + 1 = cons(X1,X2) 194.12/76.19 194.12/76.19 s(mark(X)) = X + 16 >= X + 7 = s(X) 194.12/76.19 194.12/76.19 p(mark(X)) = X + 11 >= X + 2 = p(X) 194.12/76.19 194.12/76.19 active(p(s(0()))) = 9 >= 9 = mark(0()) 194.12/76.19 194.12/76.19 f(active(X)) = X + 3 >= X + 3 = f(X) 194.12/76.19 194.12/76.19 cons(active(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = cons(X1,X2) 194.12/76.19 194.12/76.19 cons(X1,active(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = cons(X1,X2) 194.12/76.19 194.12/76.19 s(active(X)) = X + 7 >= X + 7 = s(X) 194.12/76.19 194.12/76.19 p(active(X)) = X + 2 >= X + 2 = p(X) 194.12/76.19 problem: 194.12/76.19 strict: 194.12/76.19 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.12/76.19 active(f(s(0()))) -> mark(f(p(s(0())))) 194.12/76.19 mark(f(X)) -> active(f(mark(X))) 194.12/76.19 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.12/76.19 mark(s(X)) -> active(s(mark(X))) 194.12/76.19 mark(p(X)) -> active(p(mark(X))) 194.12/76.19 weak: 194.12/76.19 mark(0()) -> active(0()) 194.12/76.19 f(mark(X)) -> f(X) 194.12/76.19 cons(mark(X1),X2) -> cons(X1,X2) 194.12/76.19 cons(X1,mark(X2)) -> cons(X1,X2) 194.12/76.19 s(mark(X)) -> s(X) 194.12/76.19 p(mark(X)) -> p(X) 194.12/76.19 active(p(s(0()))) -> mark(0()) 194.12/76.19 f(active(X)) -> f(X) 194.12/76.19 cons(active(X1),X2) -> cons(X1,X2) 194.12/76.19 cons(X1,active(X2)) -> cons(X1,X2) 194.12/76.19 s(active(X)) -> s(X) 194.12/76.19 p(active(X)) -> p(X) 194.12/76.19 Matrix Interpretation Processor: dim=3 194.12/76.19 194.12/76.19 max_matrix: 194.12/76.19 [1 0 1] 194.12/76.19 [0 1 0] 194.12/76.19 [0 0 0] 194.12/76.19 interpretation: 194.12/76.19 [1 0 1] 194.12/76.19 [p](x0) = [0 1 0]x0 194.12/76.19 [0 0 0] , 194.12/76.19 194.12/76.19 [1 0 1] 194.12/76.19 [mark](x0) = [0 1 0]x0 194.12/76.19 [0 0 0] , 194.12/76.19 194.12/76.19 [1 0 1] [1 0 0] [0] 194.12/76.19 [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1] 194.12/76.19 [0 0 0] [0 0 0] [0], 194.12/76.19 194.12/76.19 [1 0 1] [0] 194.12/76.19 [s](x0) = [0 1 0]x0 + [1] 194.12/76.19 [0 0 0] [0], 194.12/76.19 194.12/76.19 [1 0 1] 194.12/76.19 [active](x0) = [0 1 0]x0 194.12/76.19 [0 0 0] , 194.12/76.19 194.12/76.19 [1 0 1] [0] 194.12/76.19 [f](x0) = [0 1 0]x0 + [0] 194.12/76.19 [0 0 0] [1], 194.12/76.19 194.12/76.19 [0] 194.12/76.19 [0] = [1] 194.12/76.19 [0] 194.12/76.19 orientation: 194.12/76.19 [1] [0] 194.12/76.19 active(f(0())) = [1] >= [1] = mark(cons(0(),f(s(0())))) 194.12/76.19 [0] [0] 194.12/76.19 194.12/76.19 [1] [1] 194.12/76.19 active(f(s(0()))) = [2] >= [2] = mark(f(p(s(0())))) 194.12/76.19 [0] [0] 194.12/76.19 194.12/76.19 [1 0 1] [1] [1 0 1] [1] 194.12/76.19 mark(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = active(f(mark(X))) 194.12/76.19 [0 0 0] [0] [0 0 0] [0] 194.12/76.19 194.12/76.19 [1 0 1] [1 0 0] [0] [1 0 1] [1 0 0] [0] 194.12/76.19 mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = active(cons(mark(X1),X2)) 194.12/76.19 [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] 194.12/76.19 194.12/76.19 [1 0 1] [0] [1 0 1] [0] 194.12/76.19 mark(s(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = active(s(mark(X))) 194.12/76.19 [0 0 0] [0] [0 0 0] [0] 194.12/76.19 194.12/76.19 [1 0 1] [1 0 1] 194.12/76.19 mark(p(X)) = [0 1 0]X >= [0 1 0]X = active(p(mark(X))) 194.12/76.19 [0 0 0] [0 0 0] 194.12/76.19 194.12/76.19 [0] [0] 194.12/76.19 mark(0()) = [1] >= [1] = active(0()) 194.12/76.19 [0] [0] 194.12/76.19 194.12/76.19 [1 0 1] [0] [1 0 1] [0] 194.12/76.19 f(mark(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(X) 194.12/76.19 [0 0 0] [1] [0 0 0] [1] 194.12/76.19 194.12/76.19 [1 0 1] [1 0 0] [0] [1 0 1] [1 0 0] [0] 194.12/76.19 cons(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = cons(X1,X2) 194.12/76.19 [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] 194.12/76.19 194.12/76.19 [1 0 1] [1 0 1] [0] [1 0 1] [1 0 0] [0] 194.22/76.20 cons(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = cons(X1,X2) 194.22/76.20 [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] 194.22/76.20 194.22/76.20 [1 0 1] [0] [1 0 1] [0] 194.22/76.20 s(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = s(X) 194.22/76.20 [0 0 0] [0] [0 0 0] [0] 194.22/76.20 194.22/76.20 [1 0 1] [1 0 1] 194.22/76.20 p(mark(X)) = [0 1 0]X >= [0 1 0]X = p(X) 194.22/76.20 [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [0] [0] 194.22/76.20 active(p(s(0()))) = [2] >= [1] = mark(0()) 194.22/76.20 [0] [0] 194.22/76.20 194.22/76.20 [1 0 1] [0] [1 0 1] [0] 194.22/76.20 f(active(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(X) 194.22/76.20 [0 0 0] [1] [0 0 0] [1] 194.22/76.20 194.22/76.20 [1 0 1] [1 0 0] [0] [1 0 1] [1 0 0] [0] 194.22/76.20 cons(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = cons(X1,X2) 194.22/76.20 [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] 194.22/76.20 194.22/76.20 [1 0 1] [1 0 1] [0] [1 0 1] [1 0 0] [0] 194.22/76.20 cons(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [1] = cons(X1,X2) 194.22/76.20 [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] 194.22/76.20 194.22/76.20 [1 0 1] [0] [1 0 1] [0] 194.22/76.20 s(active(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = s(X) 194.22/76.20 [0 0 0] [0] [0 0 0] [0] 194.22/76.20 194.22/76.20 [1 0 1] [1 0 1] 194.22/76.20 p(active(X)) = [0 1 0]X >= [0 1 0]X = p(X) 194.22/76.20 [0 0 0] [0 0 0] 194.22/76.20 problem: 194.22/76.20 strict: 194.22/76.20 active(f(s(0()))) -> mark(f(p(s(0())))) 194.22/76.20 mark(f(X)) -> active(f(mark(X))) 194.22/76.20 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.22/76.20 mark(s(X)) -> active(s(mark(X))) 194.22/76.20 mark(p(X)) -> active(p(mark(X))) 194.22/76.20 weak: 194.22/76.20 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.22/76.20 mark(0()) -> active(0()) 194.22/76.20 f(mark(X)) -> f(X) 194.22/76.20 cons(mark(X1),X2) -> cons(X1,X2) 194.22/76.20 cons(X1,mark(X2)) -> cons(X1,X2) 194.22/76.20 s(mark(X)) -> s(X) 194.22/76.20 p(mark(X)) -> p(X) 194.22/76.20 active(p(s(0()))) -> mark(0()) 194.22/76.20 f(active(X)) -> f(X) 194.22/76.20 cons(active(X1),X2) -> cons(X1,X2) 194.22/76.20 cons(X1,active(X2)) -> cons(X1,X2) 194.22/76.20 s(active(X)) -> s(X) 194.22/76.20 p(active(X)) -> p(X) 194.22/76.20 Matrix Interpretation Processor: dim=3 194.22/76.20 194.22/76.20 max_matrix: 194.22/76.20 [1 1 0] 194.22/76.20 [0 0 1] 194.22/76.20 [0 0 1] 194.22/76.20 interpretation: 194.22/76.20 [1 1 0] 194.22/76.20 [p](x0) = [0 0 0]x0 194.22/76.20 [0 0 0] , 194.22/76.20 194.22/76.20 [1 1 0] 194.22/76.20 [mark](x0) = [0 0 0]x0 194.22/76.20 [0 0 1] , 194.22/76.20 194.22/76.20 [1 1 0] [1 0 0] 194.22/76.20 [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 194.22/76.20 [0 0 0] [0 0 0] , 194.22/76.20 194.22/76.20 [1 1 0] [0] 194.22/76.20 [s](x0) = [0 0 0]x0 + [0] 194.22/76.20 [0 0 0] [1], 194.22/76.20 194.22/76.20 [1 1 0] 194.22/76.20 [active](x0) = [0 0 0]x0 194.22/76.20 [0 0 1] , 194.22/76.20 194.22/76.20 [1 1 0] 194.22/76.20 [f](x0) = [0 0 1]x0 194.22/76.20 [0 0 0] , 194.22/76.20 194.22/76.20 [0] 194.22/76.20 [0] = [0] 194.22/76.20 [0] 194.22/76.20 orientation: 194.22/76.20 [1] [0] 194.22/76.20 active(f(s(0()))) = [0] >= [0] = mark(f(p(s(0())))) 194.22/76.20 [0] [0] 194.22/76.20 194.22/76.20 [1 1 1] [1 1 1] 194.22/76.20 mark(f(X)) = [0 0 0]X >= [0 0 0]X = active(f(mark(X))) 194.22/76.20 [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [1 1 0] [1 0 0] [1 1 0] [1 0 0] 194.22/76.20 mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = active(cons(mark(X1),X2)) 194.22/76.20 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [1 1 0] [0] [1 1 0] [0] 194.22/76.20 mark(s(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(s(mark(X))) 194.22/76.20 [0 0 0] [1] [0 0 0] [1] 194.22/76.20 194.22/76.20 [1 1 0] [1 1 0] 194.22/76.20 mark(p(X)) = [0 0 0]X >= [0 0 0]X = active(p(mark(X))) 194.22/76.20 [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [0] [0] 194.22/76.20 active(f(0())) = [0] >= [0] = mark(cons(0(),f(s(0())))) 194.22/76.20 [0] [0] 194.22/76.20 194.22/76.20 [0] [0] 194.22/76.20 mark(0()) = [0] >= [0] = active(0()) 194.22/76.20 [0] [0] 194.22/76.20 194.22/76.20 [1 1 0] [1 1 0] 194.22/76.20 f(mark(X)) = [0 0 1]X >= [0 0 1]X = f(X) 194.22/76.20 [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [1 1 0] [1 0 0] [1 1 0] [1 0 0] 194.22/76.20 cons(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.20 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [1 1 0] [1 1 0] [1 1 0] [1 0 0] 194.22/76.20 cons(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.20 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [1 1 0] [0] [1 1 0] [0] 194.22/76.20 s(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = s(X) 194.22/76.20 [0 0 0] [1] [0 0 0] [1] 194.22/76.20 194.22/76.20 [1 1 0] [1 1 0] 194.22/76.20 p(mark(X)) = [0 0 0]X >= [0 0 0]X = p(X) 194.22/76.20 [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [0] [0] 194.22/76.20 active(p(s(0()))) = [0] >= [0] = mark(0()) 194.22/76.20 [0] [0] 194.22/76.20 194.22/76.20 [1 1 0] [1 1 0] 194.22/76.20 f(active(X)) = [0 0 1]X >= [0 0 1]X = f(X) 194.22/76.20 [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [1 1 0] [1 0 0] [1 1 0] [1 0 0] 194.22/76.20 cons(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.20 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [1 1 0] [1 1 0] [1 1 0] [1 0 0] 194.22/76.20 cons(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.20 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.20 194.22/76.20 [1 1 0] [0] [1 1 0] [0] 194.22/76.20 s(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = s(X) 194.22/76.20 [0 0 0] [1] [0 0 0] [1] 194.22/76.20 194.22/76.20 [1 1 0] [1 1 0] 194.22/76.20 p(active(X)) = [0 0 0]X >= [0 0 0]X = p(X) 194.22/76.20 [0 0 0] [0 0 0] 194.22/76.20 problem: 194.22/76.20 strict: 194.22/76.20 mark(f(X)) -> active(f(mark(X))) 194.22/76.20 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.22/76.20 mark(s(X)) -> active(s(mark(X))) 194.22/76.20 mark(p(X)) -> active(p(mark(X))) 194.22/76.20 weak: 194.22/76.20 active(f(s(0()))) -> mark(f(p(s(0())))) 194.22/76.20 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.22/76.20 mark(0()) -> active(0()) 194.22/76.20 f(mark(X)) -> f(X) 194.22/76.20 cons(mark(X1),X2) -> cons(X1,X2) 194.22/76.20 cons(X1,mark(X2)) -> cons(X1,X2) 194.22/76.20 s(mark(X)) -> s(X) 194.22/76.20 p(mark(X)) -> p(X) 194.22/76.20 active(p(s(0()))) -> mark(0()) 194.22/76.20 f(active(X)) -> f(X) 194.22/76.20 cons(active(X1),X2) -> cons(X1,X2) 194.22/76.20 cons(X1,active(X2)) -> cons(X1,X2) 194.22/76.20 s(active(X)) -> s(X) 194.22/76.20 p(active(X)) -> p(X) 194.22/76.20 Matrix Interpretation Processor: dim=3 194.22/76.20 194.22/76.20 max_matrix: 194.22/76.20 [1 1 1] 194.22/76.20 [0 1 1] 194.22/76.20 [0 0 1] 194.22/76.20 interpretation: 194.22/76.20 [1 0 0] [0] 194.22/76.20 [p](x0) = [0 1 0]x0 + [1] 194.22/76.20 [0 0 0] [0], 194.22/76.20 194.22/76.20 [1 1 0] 194.22/76.20 [mark](x0) = [0 1 0]x0 194.22/76.21 [0 0 1] , 194.22/76.21 194.22/76.21 [1 0 0] [1 0 0] 194.22/76.21 [cons](x0, x1) = [0 1 0]x0 + [0 0 0]x1 194.22/76.21 [0 0 0] [0 0 0] , 194.22/76.21 194.22/76.21 [1 0 0] [0] 194.22/76.21 [s](x0) = [0 1 1]x0 + [1] 194.22/76.21 [0 0 0] [1], 194.22/76.21 194.22/76.21 [1 0 1] 194.22/76.21 [active](x0) = [0 1 0]x0 194.22/76.21 [0 0 1] , 194.22/76.21 194.22/76.21 [1 0 1] [0] 194.22/76.21 [f](x0) = [0 1 1]x0 + [1] 194.22/76.21 [0 0 1] [1], 194.22/76.21 194.22/76.21 [0] 194.22/76.21 [0] = [0] 194.22/76.21 [0] 194.22/76.21 orientation: 194.22/76.21 [1 1 2] [1] [1 1 2] [1] 194.22/76.21 mark(f(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = active(f(mark(X))) 194.22/76.21 [0 0 1] [1] [0 0 1] [1] 194.22/76.21 194.22/76.21 [1 1 0] [1 0 0] [1 1 0] [1 0 0] 194.22/76.21 mark(cons(X1,X2)) = [0 1 0]X1 + [0 0 0]X2 >= [0 1 0]X1 + [0 0 0]X2 = active(cons(mark(X1),X2)) 194.22/76.21 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.21 194.22/76.21 [1 1 1] [1] [1 1 0] [1] 194.22/76.21 mark(s(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = active(s(mark(X))) 194.22/76.21 [0 0 0] [1] [0 0 0] [1] 194.22/76.21 194.22/76.21 [1 1 0] [1] [1 1 0] [0] 194.22/76.21 mark(p(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = active(p(mark(X))) 194.22/76.21 [0 0 0] [0] [0 0 0] [0] 194.22/76.21 194.22/76.21 [3] [3] 194.22/76.21 active(f(s(0()))) = [3] >= [3] = mark(f(p(s(0())))) 194.22/76.21 [2] [1] 194.22/76.21 194.22/76.21 [1] [1] 194.22/76.21 active(f(0())) = [1] >= [0] = mark(cons(0(),f(s(0())))) 194.22/76.21 [1] [0] 194.22/76.21 194.22/76.21 [0] [0] 194.22/76.21 mark(0()) = [0] >= [0] = active(0()) 194.22/76.21 [0] [0] 194.22/76.21 194.22/76.21 [1 1 1] [0] [1 0 1] [0] 194.22/76.21 f(mark(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = f(X) 194.22/76.21 [0 0 1] [1] [0 0 1] [1] 194.22/76.21 194.22/76.21 [1 1 0] [1 0 0] [1 0 0] [1 0 0] 194.22/76.21 cons(mark(X1),X2) = [0 1 0]X1 + [0 0 0]X2 >= [0 1 0]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.21 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.21 194.22/76.21 [1 0 0] [1 1 0] [1 0 0] [1 0 0] 194.22/76.21 cons(X1,mark(X2)) = [0 1 0]X1 + [0 0 0]X2 >= [0 1 0]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.21 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.21 194.22/76.21 [1 1 0] [0] [1 0 0] [0] 194.22/76.21 s(mark(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = s(X) 194.22/76.21 [0 0 0] [1] [0 0 0] [1] 194.22/76.21 194.22/76.21 [1 1 0] [0] [1 0 0] [0] 194.22/76.21 p(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = p(X) 194.22/76.21 [0 0 0] [0] [0 0 0] [0] 194.22/76.21 194.22/76.21 [0] [0] 194.22/76.21 active(p(s(0()))) = [2] >= [0] = mark(0()) 194.22/76.21 [0] [0] 194.22/76.21 194.22/76.21 [1 0 2] [0] [1 0 1] [0] 194.22/76.21 f(active(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = f(X) 194.22/76.21 [0 0 1] [1] [0 0 1] [1] 194.22/76.21 194.22/76.21 [1 0 1] [1 0 0] [1 0 0] [1 0 0] 194.22/76.21 cons(active(X1),X2) = [0 1 0]X1 + [0 0 0]X2 >= [0 1 0]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.21 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.21 194.22/76.21 [1 0 0] [1 0 1] [1 0 0] [1 0 0] 194.22/76.21 cons(X1,active(X2)) = [0 1 0]X1 + [0 0 0]X2 >= [0 1 0]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.22 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.22 194.22/76.22 [1 0 1] [0] [1 0 0] [0] 194.22/76.22 s(active(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = s(X) 194.22/76.22 [0 0 0] [1] [0 0 0] [1] 194.22/76.22 194.22/76.22 [1 0 1] [0] [1 0 0] [0] 194.22/76.22 p(active(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = p(X) 194.22/76.22 [0 0 0] [0] [0 0 0] [0] 194.22/76.22 problem: 194.22/76.22 strict: 194.22/76.22 mark(f(X)) -> active(f(mark(X))) 194.22/76.22 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.22/76.22 mark(s(X)) -> active(s(mark(X))) 194.22/76.22 weak: 194.22/76.22 mark(p(X)) -> active(p(mark(X))) 194.22/76.22 active(f(s(0()))) -> mark(f(p(s(0())))) 194.22/76.22 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.22/76.22 mark(0()) -> active(0()) 194.22/76.22 f(mark(X)) -> f(X) 194.22/76.22 cons(mark(X1),X2) -> cons(X1,X2) 194.22/76.22 cons(X1,mark(X2)) -> cons(X1,X2) 194.22/76.22 s(mark(X)) -> s(X) 194.22/76.22 p(mark(X)) -> p(X) 194.22/76.22 active(p(s(0()))) -> mark(0()) 194.22/76.22 f(active(X)) -> f(X) 194.22/76.22 cons(active(X1),X2) -> cons(X1,X2) 194.22/76.22 cons(X1,active(X2)) -> cons(X1,X2) 194.22/76.22 s(active(X)) -> s(X) 194.22/76.22 p(active(X)) -> p(X) 194.22/76.22 Matrix Interpretation Processor: dim=3 194.22/76.22 194.22/76.22 max_matrix: 194.22/76.22 [1 1 1] 194.22/76.22 [0 0 0] 194.22/76.22 [0 0 1] 194.22/76.22 interpretation: 194.22/76.22 [1 0 0] 194.22/76.22 [p](x0) = [0 0 0]x0 194.22/76.22 [0 0 1] , 194.22/76.22 194.22/76.22 [1 0 1] 194.22/76.22 [mark](x0) = [0 0 0]x0 194.22/76.22 [0 0 1] , 194.22/76.22 194.22/76.22 [1 0 1] [1 0 0] [0] 194.22/76.22 [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0] 194.22/76.22 [0 0 1] [0 0 0] [1], 194.22/76.22 194.22/76.22 [1 0 0] 194.22/76.22 [s](x0) = [0 0 0]x0 194.22/76.22 [0 0 1] , 194.22/76.22 194.22/76.22 [1 1 0] 194.22/76.22 [active](x0) = [0 0 0]x0 194.22/76.22 [0 0 1] , 194.22/76.22 194.22/76.22 [1 0 0] [0] 194.22/76.22 [f](x0) = [0 0 0]x0 + [1] 194.22/76.22 [0 0 1] [1], 194.22/76.22 194.22/76.22 [0] 194.22/76.22 [0] = [0] 194.22/76.22 [0] 194.22/76.22 orientation: 194.22/76.22 [1 0 1] [1] [1 0 1] [1] 194.22/76.22 mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(f(mark(X))) 194.22/76.22 [0 0 1] [1] [0 0 1] [1] 194.22/76.22 194.22/76.22 [1 0 2] [1 0 0] [1] [1 0 2] [1 0 0] [0] 194.22/76.22 mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = active(cons(mark(X1),X2)) 194.22/76.22 [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] 194.22/76.22 194.22/76.22 [1 0 1] [1 0 1] 194.22/76.22 mark(s(X)) = [0 0 0]X >= [0 0 0]X = active(s(mark(X))) 194.22/76.22 [0 0 1] [0 0 1] 194.22/76.22 194.22/76.22 [1 0 1] [1 0 1] 194.22/76.22 mark(p(X)) = [0 0 0]X >= [0 0 0]X = active(p(mark(X))) 194.22/76.22 [0 0 1] [0 0 1] 194.22/76.22 194.22/76.22 [1] [1] 194.22/76.22 active(f(s(0()))) = [0] >= [0] = mark(f(p(s(0())))) 194.22/76.22 [1] [1] 194.22/76.22 194.22/76.22 [1] [1] 194.22/76.22 active(f(0())) = [0] >= [0] = mark(cons(0(),f(s(0())))) 194.22/76.22 [1] [1] 194.22/76.22 194.22/76.22 [0] [0] 194.22/76.22 mark(0()) = [0] >= [0] = active(0()) 194.22/76.22 [0] [0] 194.22/76.22 194.22/76.22 [1 0 1] [0] [1 0 0] [0] 194.22/76.22 f(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = f(X) 194.22/76.22 [0 0 1] [1] [0 0 1] [1] 194.22/76.22 194.22/76.22 [1 0 2] [1 0 0] [0] [1 0 1] [1 0 0] [0] 194.22/76.22 cons(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = cons(X1,X2) 194.22/76.22 [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] 194.22/76.22 194.22/76.22 [1 0 1] [1 0 1] [0] [1 0 1] [1 0 0] [0] 194.22/76.22 cons(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = cons(X1,X2) 194.22/76.22 [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] 194.22/76.22 194.22/76.22 [1 0 1] [1 0 0] 194.22/76.22 s(mark(X)) = [0 0 0]X >= [0 0 0]X = s(X) 194.22/76.22 [0 0 1] [0 0 1] 194.22/76.22 194.22/76.22 [1 0 1] [1 0 0] 194.22/76.22 p(mark(X)) = [0 0 0]X >= [0 0 0]X = p(X) 194.22/76.22 [0 0 1] [0 0 1] 194.22/76.22 194.22/76.22 [0] [0] 194.22/76.22 active(p(s(0()))) = [0] >= [0] = mark(0()) 194.22/76.22 [0] [0] 194.22/76.22 194.22/76.22 [1 1 0] [0] [1 0 0] [0] 194.22/76.22 f(active(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = f(X) 194.22/76.22 [0 0 1] [1] [0 0 1] [1] 194.22/76.22 194.22/76.22 [1 1 1] [1 0 0] [0] [1 0 1] [1 0 0] [0] 194.22/76.22 cons(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = cons(X1,X2) 194.22/76.22 [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] 194.22/76.22 194.22/76.22 [1 0 1] [1 1 0] [0] [1 0 1] [1 0 0] [0] 194.22/76.22 cons(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = cons(X1,X2) 194.22/76.22 [0 0 1] [0 0 0] [1] [0 0 1] [0 0 0] [1] 194.22/76.22 194.22/76.22 [1 1 0] [1 0 0] 194.22/76.22 s(active(X)) = [0 0 0]X >= [0 0 0]X = s(X) 194.22/76.22 [0 0 1] [0 0 1] 194.22/76.22 194.22/76.22 [1 1 0] [1 0 0] 194.22/76.22 p(active(X)) = [0 0 0]X >= [0 0 0]X = p(X) 194.22/76.22 [0 0 1] [0 0 1] 194.22/76.22 problem: 194.22/76.22 strict: 194.22/76.22 mark(f(X)) -> active(f(mark(X))) 194.22/76.22 mark(s(X)) -> active(s(mark(X))) 194.22/76.22 weak: 194.22/76.22 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.22/76.22 mark(p(X)) -> active(p(mark(X))) 194.22/76.22 active(f(s(0()))) -> mark(f(p(s(0())))) 194.22/76.22 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.22/76.22 mark(0()) -> active(0()) 194.22/76.22 f(mark(X)) -> f(X) 194.22/76.22 cons(mark(X1),X2) -> cons(X1,X2) 194.22/76.22 cons(X1,mark(X2)) -> cons(X1,X2) 194.22/76.22 s(mark(X)) -> s(X) 194.22/76.22 p(mark(X)) -> p(X) 194.22/76.22 active(p(s(0()))) -> mark(0()) 194.22/76.22 f(active(X)) -> f(X) 194.22/76.22 cons(active(X1),X2) -> cons(X1,X2) 194.22/76.22 cons(X1,active(X2)) -> cons(X1,X2) 194.22/76.22 s(active(X)) -> s(X) 194.22/76.22 p(active(X)) -> p(X) 194.22/76.22 Matrix Interpretation Processor: dim=4 194.22/76.22 194.22/76.22 max_matrix: 194.22/76.22 [1 1 1 1] 194.22/76.22 [0 1 0 0] 194.22/76.22 [0 0 1 0] 194.22/76.22 [0 0 0 0] 194.22/76.22 interpretation: 194.22/76.22 [1 0 0 0] 194.22/76.22 [0 0 0 0] 194.22/76.22 [p](x0) = [0 0 1 0]x0 194.22/76.22 [0 0 0 0] , 194.22/76.22 194.22/76.22 [1 0 1 0] 194.22/76.22 [0 1 0 0] 194.22/76.22 [mark](x0) = [0 0 1 0]x0 194.22/76.22 [0 0 0 0] , 194.22/76.22 194.22/76.22 [1 0 0 0] [1 0 0 0] 194.22/76.22 [0 0 0 0] [0 0 0 0] 194.22/76.22 [cons](x0, x1) = [0 0 1 0]x0 + [0 0 0 0]x1 194.22/76.22 [0 0 0 0] [0 0 0 0] , 194.22/76.22 194.22/76.22 [1 0 1 0] [0] 194.22/76.22 [0 0 0 0] [1] 194.22/76.22 [s](x0) = [0 0 1 0]x0 + [1] 194.22/76.22 [0 0 0 0] [0], 194.22/76.22 194.22/76.22 [1 0 0 1] 194.22/76.22 [0 1 0 0] 194.22/76.22 [active](x0) = [0 0 1 0]x0 194.22/76.22 [0 0 0 0] , 194.22/76.22 194.22/76.22 [1 1 0 0] [0] 194.22/76.22 [0 0 0 0] [0] 194.22/76.22 [f](x0) = [0 0 1 0]x0 + [1] 194.22/76.22 [0 0 0 0] [1], 194.22/76.22 194.22/76.22 [0] 194.22/76.23 [0] 194.22/76.23 [0] = [0] 194.22/76.23 [0] 194.22/76.23 orientation: 194.22/76.23 [1 1 1 0] [1] [1 1 1 0] [1] 194.22/76.23 [0 0 0 0] [0] [0 0 0 0] [0] 194.22/76.23 mark(f(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = active(f(mark(X))) 194.22/76.23 [0 0 0 0] [0] [0 0 0 0] [0] 194.22/76.23 194.22/76.23 [1 0 2 0] [1] [1 0 2 0] [0] 194.22/76.23 [0 0 0 0] [1] [0 0 0 0] [1] 194.22/76.23 mark(s(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = active(s(mark(X))) 194.22/76.23 [0 0 0 0] [0] [0 0 0 0] [0] 194.22/76.23 194.22/76.23 [1 0 1 0] [1 0 0 0] [1 0 1 0] [1 0 0 0] 194.22/76.23 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.23 mark(cons(X1,X2)) = [0 0 1 0]X1 + [0 0 0 0]X2 >= [0 0 1 0]X1 + [0 0 0 0]X2 = active(cons(mark(X1),X2)) 194.22/76.23 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.23 194.22/76.23 [1 0 1 0] [1 0 1 0] 194.22/76.23 [0 0 0 0] [0 0 0 0] 194.22/76.23 mark(p(X)) = [0 0 1 0]X >= [0 0 1 0]X = active(p(mark(X))) 194.22/76.23 [0 0 0 0] [0 0 0 0] 194.22/76.23 194.22/76.23 [2] [2] 194.22/76.23 [0] [0] 194.22/76.23 active(f(s(0()))) = [2] >= [2] = mark(f(p(s(0())))) 194.22/76.23 [0] [0] 194.22/76.23 194.22/76.23 [1] [1] 194.22/76.23 [0] [0] 194.22/76.23 active(f(0())) = [1] >= [0] = mark(cons(0(),f(s(0())))) 194.22/76.23 [0] [0] 194.22/76.23 194.22/76.23 [0] [0] 194.22/76.23 [0] [0] 194.22/76.23 mark(0()) = [0] >= [0] = active(0()) 194.22/76.23 [0] [0] 194.22/76.23 194.22/76.23 [1 1 1 0] [0] [1 1 0 0] [0] 194.22/76.23 [0 0 0 0] [0] [0 0 0 0] [0] 194.22/76.23 f(mark(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = f(X) 194.22/76.23 [0 0 0 0] [1] [0 0 0 0] [1] 194.22/76.23 194.22/76.23 [1 0 1 0] [1 0 0 0] [1 0 0 0] [1 0 0 0] 194.22/76.23 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.23 cons(mark(X1),X2) = [0 0 1 0]X1 + [0 0 0 0]X2 >= [0 0 1 0]X1 + [0 0 0 0]X2 = cons(X1,X2) 194.22/76.23 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.23 194.22/76.23 [1 0 0 0] [1 0 1 0] [1 0 0 0] [1 0 0 0] 194.22/76.23 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.23 cons(X1,mark(X2)) = [0 0 1 0]X1 + [0 0 0 0]X2 >= [0 0 1 0]X1 + [0 0 0 0]X2 = cons(X1,X2) 194.22/76.23 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.23 194.22/76.23 [1 0 2 0] [0] [1 0 1 0] [0] 194.22/76.23 [0 0 0 0] [1] [0 0 0 0] [1] 194.22/76.23 s(mark(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = s(X) 194.22/76.23 [0 0 0 0] [0] [0 0 0 0] [0] 194.22/76.23 194.22/76.23 [1 0 1 0] [1 0 0 0] 194.22/76.23 [0 0 0 0] [0 0 0 0] 194.22/76.23 p(mark(X)) = [0 0 1 0]X >= [0 0 1 0]X = p(X) 194.22/76.23 [0 0 0 0] [0 0 0 0] 194.22/76.23 194.22/76.23 [0] [0] 194.22/76.23 [0] [0] 194.22/76.23 active(p(s(0()))) = [1] >= [0] = mark(0()) 194.22/76.23 [0] [0] 194.22/76.23 194.22/76.23 [1 1 0 1] [0] [1 1 0 0] [0] 194.22/76.24 [0 0 0 0] [0] [0 0 0 0] [0] 194.22/76.24 f(active(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = f(X) 194.22/76.24 [0 0 0 0] [1] [0 0 0 0] [1] 194.22/76.24 194.22/76.24 [1 0 0 1] [1 0 0 0] [1 0 0 0] [1 0 0 0] 194.22/76.24 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.24 cons(active(X1),X2) = [0 0 1 0]X1 + [0 0 0 0]X2 >= [0 0 1 0]X1 + [0 0 0 0]X2 = cons(X1,X2) 194.22/76.24 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.24 194.22/76.24 [1 0 0 0] [1 0 0 1] [1 0 0 0] [1 0 0 0] 194.22/76.24 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.24 cons(X1,active(X2)) = [0 0 1 0]X1 + [0 0 0 0]X2 >= [0 0 1 0]X1 + [0 0 0 0]X2 = cons(X1,X2) 194.22/76.24 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 194.22/76.24 194.22/76.24 [1 0 1 1] [0] [1 0 1 0] [0] 194.22/76.24 [0 0 0 0] [1] [0 0 0 0] [1] 194.22/76.24 s(active(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = s(X) 194.22/76.24 [0 0 0 0] [0] [0 0 0 0] [0] 194.22/76.24 194.22/76.24 [1 0 0 1] [1 0 0 0] 194.22/76.24 [0 0 0 0] [0 0 0 0] 194.22/76.24 p(active(X)) = [0 0 1 0]X >= [0 0 1 0]X = p(X) 194.22/76.24 [0 0 0 0] [0 0 0 0] 194.22/76.24 problem: 194.22/76.24 strict: 194.22/76.24 mark(f(X)) -> active(f(mark(X))) 194.22/76.24 weak: 194.22/76.24 mark(s(X)) -> active(s(mark(X))) 194.22/76.24 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.22/76.24 mark(p(X)) -> active(p(mark(X))) 194.22/76.24 active(f(s(0()))) -> mark(f(p(s(0())))) 194.22/76.24 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.22/76.24 mark(0()) -> active(0()) 194.22/76.24 f(mark(X)) -> f(X) 194.22/76.24 cons(mark(X1),X2) -> cons(X1,X2) 194.22/76.24 cons(X1,mark(X2)) -> cons(X1,X2) 194.22/76.24 s(mark(X)) -> s(X) 194.22/76.24 p(mark(X)) -> p(X) 194.22/76.24 active(p(s(0()))) -> mark(0()) 194.22/76.24 f(active(X)) -> f(X) 194.22/76.24 cons(active(X1),X2) -> cons(X1,X2) 194.22/76.24 cons(X1,active(X2)) -> cons(X1,X2) 194.22/76.24 s(active(X)) -> s(X) 194.22/76.24 p(active(X)) -> p(X) 194.22/76.24 Matrix Interpretation Processor: dim=3 194.22/76.24 194.22/76.24 max_matrix: 194.22/76.24 [1 1 1] 194.22/76.24 [0 1 1] 194.22/76.24 [0 0 1] 194.22/76.24 interpretation: 194.22/76.24 [1 0 0] 194.22/76.24 [p](x0) = [0 1 1]x0 194.22/76.24 [0 0 0] , 194.22/76.24 194.22/76.24 [1 1 1] 194.22/76.24 [mark](x0) = [0 1 0]x0 194.22/76.24 [0 0 1] , 194.22/76.24 194.22/76.24 [1 0 1] [1 0 0] 194.22/76.24 [cons](x0, x1) = [0 1 1]x0 + [0 0 0]x1 194.22/76.24 [0 0 0] [0 0 0] , 194.22/76.24 194.22/76.24 [1 0 0] [0] 194.22/76.24 [s](x0) = [0 1 1]x0 + [0] 194.22/76.24 [0 0 1] [1], 194.22/76.24 194.22/76.24 [1 0 1] 194.22/76.24 [active](x0) = [0 1 0]x0 194.22/76.24 [0 0 1] , 194.22/76.24 194.22/76.24 [1 0 1] [0] 194.22/76.24 [f](x0) = [0 1 1]x0 + [1] 194.22/76.24 [0 0 1] [1], 194.22/76.24 194.22/76.24 [0] 194.22/76.24 [0] = [0] 194.22/76.24 [0] 194.22/76.24 orientation: 194.22/76.24 [1 1 3] [2] [1 1 3] [1] 194.22/76.24 mark(f(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = active(f(mark(X))) 194.22/76.24 [0 0 1] [1] [0 0 1] [1] 194.22/76.24 194.22/76.24 [1 1 2] [1] [1 1 2] [1] 194.22/76.24 mark(s(X)) = [0 1 1]X + [0] >= [0 1 1]X + [0] = active(s(mark(X))) 194.22/76.24 [0 0 1] [1] [0 0 1] [1] 194.22/76.24 194.22/76.24 [1 1 2] [1 0 0] [1 1 2] [1 0 0] 194.22/76.24 mark(cons(X1,X2)) = [0 1 1]X1 + [0 0 0]X2 >= [0 1 1]X1 + [0 0 0]X2 = active(cons(mark(X1),X2)) 194.22/76.24 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.24 194.22/76.24 [1 1 1] [1 1 1] 194.22/76.24 mark(p(X)) = [0 1 1]X >= [0 1 1]X = active(p(mark(X))) 194.22/76.24 [0 0 0] [0 0 0] 194.22/76.24 194.22/76.24 [3] [3] 194.22/76.24 active(f(s(0()))) = [2] >= [2] = mark(f(p(s(0())))) 194.22/76.24 [2] [1] 194.22/76.24 194.22/76.24 [1] [1] 194.22/76.24 active(f(0())) = [1] >= [0] = mark(cons(0(),f(s(0())))) 194.22/76.24 [1] [0] 194.22/76.24 194.22/76.24 [0] [0] 194.22/76.24 mark(0()) = [0] >= [0] = active(0()) 194.22/76.24 [0] [0] 194.22/76.24 194.22/76.24 [1 1 2] [0] [1 0 1] [0] 194.22/76.24 f(mark(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = f(X) 194.22/76.24 [0 0 1] [1] [0 0 1] [1] 194.22/76.24 194.22/76.24 [1 1 2] [1 0 0] [1 0 1] [1 0 0] 194.22/76.24 cons(mark(X1),X2) = [0 1 1]X1 + [0 0 0]X2 >= [0 1 1]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.24 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.24 194.22/76.24 [1 0 1] [1 1 1] [1 0 1] [1 0 0] 194.22/76.24 cons(X1,mark(X2)) = [0 1 1]X1 + [0 0 0]X2 >= [0 1 1]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.24 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.24 194.22/76.24 [1 1 1] [0] [1 0 0] [0] 194.22/76.24 s(mark(X)) = [0 1 1]X + [0] >= [0 1 1]X + [0] = s(X) 194.22/76.24 [0 0 1] [1] [0 0 1] [1] 194.22/76.24 194.22/76.24 [1 1 1] [1 0 0] 194.22/76.24 p(mark(X)) = [0 1 1]X >= [0 1 1]X = p(X) 194.22/76.24 [0 0 0] [0 0 0] 194.22/76.24 194.22/76.24 [0] [0] 194.22/76.24 active(p(s(0()))) = [1] >= [0] = mark(0()) 194.22/76.24 [0] [0] 194.22/76.24 194.22/76.24 [1 0 2] [0] [1 0 1] [0] 194.22/76.24 f(active(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = f(X) 194.22/76.24 [0 0 1] [1] [0 0 1] [1] 194.22/76.24 194.22/76.24 [1 0 2] [1 0 0] [1 0 1] [1 0 0] 194.22/76.24 cons(active(X1),X2) = [0 1 1]X1 + [0 0 0]X2 >= [0 1 1]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.24 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.24 194.22/76.24 [1 0 1] [1 0 1] [1 0 1] [1 0 0] 194.22/76.24 cons(X1,active(X2)) = [0 1 1]X1 + [0 0 0]X2 >= [0 1 1]X1 + [0 0 0]X2 = cons(X1,X2) 194.22/76.24 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 194.22/76.24 194.22/76.24 [1 0 1] [0] [1 0 0] [0] 194.22/76.24 s(active(X)) = [0 1 1]X + [0] >= [0 1 1]X + [0] = s(X) 194.22/76.24 [0 0 1] [1] [0 0 1] [1] 194.22/76.24 194.22/76.24 [1 0 1] [1 0 0] 194.22/76.24 p(active(X)) = [0 1 1]X >= [0 1 1]X = p(X) 194.22/76.24 [0 0 0] [0 0 0] 194.22/76.24 problem: 194.22/76.24 strict: 194.22/76.24 194.22/76.24 weak: 194.22/76.24 mark(f(X)) -> active(f(mark(X))) 194.22/76.24 mark(s(X)) -> active(s(mark(X))) 194.22/76.24 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 194.22/76.24 mark(p(X)) -> active(p(mark(X))) 194.22/76.24 active(f(s(0()))) -> mark(f(p(s(0())))) 194.22/76.24 active(f(0())) -> mark(cons(0(),f(s(0())))) 194.22/76.24 mark(0()) -> active(0()) 194.22/76.24 f(mark(X)) -> f(X) 194.22/76.24 cons(mark(X1),X2) -> cons(X1,X2) 194.22/76.24 cons(X1,mark(X2)) -> cons(X1,X2) 194.22/76.24 s(mark(X)) -> s(X) 194.22/76.24 p(mark(X)) -> p(X) 194.22/76.24 active(p(s(0()))) -> mark(0()) 194.22/76.24 f(active(X)) -> f(X) 194.22/76.24 cons(active(X1),X2) -> cons(X1,X2) 194.22/76.24 cons(X1,active(X2)) -> cons(X1,X2) 194.22/76.24 s(active(X)) -> s(X) 194.22/76.24 p(active(X)) -> p(X) 194.22/76.24 Qed 194.22/76.25 EOF