YES(?,O(n^1)) 100.01/26.17 YES(?,O(n^1)) 100.01/26.18 100.01/26.18 Problem: 100.01/26.18 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.01/26.18 active(b()) -> mark(a()) 100.01/26.18 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.01/26.18 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.01/26.18 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.01/26.18 proper(a()) -> ok(a()) 100.01/26.18 proper(b()) -> ok(b()) 100.01/26.18 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.01/26.18 top(mark(X)) -> top(proper(X)) 100.01/26.18 top(ok(X)) -> top(active(X)) 100.01/26.18 100.01/26.18 Proof: 100.01/26.18 Complexity Transformation Processor: 100.01/26.18 strict: 100.01/26.18 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.01/26.18 active(b()) -> mark(a()) 100.01/26.18 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.01/26.18 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.01/26.18 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.01/26.18 proper(a()) -> ok(a()) 100.01/26.18 proper(b()) -> ok(b()) 100.01/26.18 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.01/26.18 top(mark(X)) -> top(proper(X)) 100.01/26.18 top(ok(X)) -> top(active(X)) 100.01/26.18 weak: 100.01/26.18 100.01/26.18 Matrix Interpretation Processor: dim=1 100.01/26.18 100.01/26.18 max_matrix: 100.01/26.18 1 100.01/26.18 interpretation: 100.01/26.18 [top](x0) = x0 + 6, 100.01/26.18 100.01/26.18 [ok](x0) = x0 + 1, 100.01/26.18 100.01/26.18 [proper](x0) = x0 + 5, 100.01/26.18 100.01/26.18 [mark](x0) = x0 + 2, 100.01/26.18 100.01/26.18 [b] = 7, 100.01/26.18 100.01/26.18 [active](x0) = x0, 100.01/26.18 100.01/26.18 [f](x0, x1, x2) = x0 + x1 + x2 + 13, 100.01/26.18 100.01/26.18 [a] = 8 100.01/26.18 orientation: 100.01/26.18 active(f(a(),X,X)) = 2X + 21 >= X + 29 = mark(f(X,b(),b())) 100.01/26.18 100.01/26.18 active(b()) = 7 >= 10 = mark(a()) 100.01/26.18 100.01/26.18 active(f(X1,X2,X3)) = X1 + X2 + X3 + 13 >= X1 + X2 + X3 + 13 = f(X1,active(X2),X3) 100.01/26.18 100.01/26.18 f(X1,mark(X2),X3) = X1 + X2 + X3 + 15 >= X1 + X2 + X3 + 15 = mark(f(X1,X2,X3)) 100.01/26.18 100.01/26.18 proper(f(X1,X2,X3)) = X1 + X2 + X3 + 18 >= X1 + X2 + X3 + 28 = f(proper(X1),proper(X2),proper(X3)) 100.01/26.18 100.01/26.18 proper(a()) = 13 >= 9 = ok(a()) 100.01/26.18 100.01/26.18 proper(b()) = 12 >= 8 = ok(b()) 100.01/26.18 100.01/26.18 f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 16 >= X1 + X2 + X3 + 14 = ok(f(X1,X2,X3)) 100.01/26.18 100.01/26.18 top(mark(X)) = X + 8 >= X + 11 = top(proper(X)) 100.01/26.18 100.01/26.18 top(ok(X)) = X + 7 >= X + 6 = top(active(X)) 100.01/26.18 problem: 100.01/26.18 strict: 100.01/26.18 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.01/26.18 active(b()) -> mark(a()) 100.01/26.18 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.01/26.18 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.01/26.18 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.01/26.18 top(mark(X)) -> top(proper(X)) 100.01/26.18 weak: 100.01/26.18 proper(a()) -> ok(a()) 100.01/26.18 proper(b()) -> ok(b()) 100.01/26.18 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.01/26.18 top(ok(X)) -> top(active(X)) 100.01/26.18 Matrix Interpretation Processor: dim=1 100.01/26.18 100.01/26.18 max_matrix: 100.01/26.18 1 100.01/26.18 interpretation: 100.01/26.18 [top](x0) = x0, 100.01/26.18 100.01/26.18 [ok](x0) = x0, 100.01/26.18 100.01/26.18 [proper](x0) = x0, 100.01/26.18 100.01/26.18 [mark](x0) = x0 + 1, 100.01/26.18 100.01/26.18 [b] = 3, 100.01/26.18 100.01/26.18 [active](x0) = x0, 100.01/26.18 100.01/26.18 [f](x0, x1, x2) = x0 + x1 + x2 + 5, 100.01/26.18 100.01/26.18 [a] = 0 100.01/26.18 orientation: 100.01/26.18 active(f(a(),X,X)) = 2X + 5 >= X + 12 = mark(f(X,b(),b())) 100.01/26.18 100.01/26.18 active(b()) = 3 >= 1 = mark(a()) 100.01/26.18 100.01/26.18 active(f(X1,X2,X3)) = X1 + X2 + X3 + 5 >= X1 + X2 + X3 + 5 = f(X1,active(X2),X3) 100.01/26.18 100.01/26.18 f(X1,mark(X2),X3) = X1 + X2 + X3 + 6 >= X1 + X2 + X3 + 6 = mark(f(X1,X2,X3)) 100.01/26.18 100.01/26.18 proper(f(X1,X2,X3)) = X1 + X2 + X3 + 5 >= X1 + X2 + X3 + 5 = f(proper(X1),proper(X2),proper(X3)) 100.01/26.18 100.01/26.18 top(mark(X)) = X + 1 >= X = top(proper(X)) 100.01/26.18 100.01/26.18 proper(a()) = 0 >= 0 = ok(a()) 100.01/26.18 100.01/26.18 proper(b()) = 3 >= 3 = ok(b()) 100.01/26.18 100.01/26.18 f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 5 >= X1 + X2 + X3 + 5 = ok(f(X1,X2,X3)) 100.01/26.18 100.01/26.18 top(ok(X)) = X >= X = top(active(X)) 100.01/26.18 problem: 100.01/26.18 strict: 100.01/26.18 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.01/26.18 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.01/26.18 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.01/26.18 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.01/26.18 weak: 100.01/26.18 active(b()) -> mark(a()) 100.01/26.18 top(mark(X)) -> top(proper(X)) 100.01/26.18 proper(a()) -> ok(a()) 100.01/26.18 proper(b()) -> ok(b()) 100.01/26.18 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.01/26.18 top(ok(X)) -> top(active(X)) 100.01/26.18 Splitting Processor: 100.01/26.18 strict: 100.01/26.18 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.01/26.18 weak: 100.01/26.18 active(b()) -> mark(a()) 100.01/26.18 top(mark(X)) -> top(proper(X)) 100.01/26.18 proper(a()) -> ok(a()) 100.01/26.18 proper(b()) -> ok(b()) 100.01/26.18 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.01/26.18 top(ok(X)) -> top(active(X)) 100.01/26.18 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.01/26.18 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.01/26.18 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.01/26.18 Splitting Processor: 100.01/26.18 strict: 100.01/26.18 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.01/26.18 weak: 100.01/26.18 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.01/26.18 active(b()) -> mark(a()) 100.01/26.18 top(mark(X)) -> top(proper(X)) 100.01/26.18 proper(a()) -> ok(a()) 100.01/26.18 proper(b()) -> ok(b()) 100.01/26.18 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.01/26.18 top(ok(X)) -> top(active(X)) 100.01/26.18 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.01/26.18 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.01/26.18 Bounds Processor: 100.01/26.18 bound: 0 100.01/26.18 enrichment: match 100.01/26.18 automaton: 100.01/26.18 final states: {11,9,8,7,6,5} 100.01/26.18 transitions: 100.01/26.18 active0(2) -> 5* 100.01/26.18 active0(9) -> 5* 100.01/26.18 active0(4) -> 5* 100.01/26.18 active0(11) -> 5* 100.01/26.18 active0(1) -> 5* 100.01/26.18 active0(3) -> 5* 100.01/26.18 f0(3,4,2) -> 7* 100.01/26.18 f0(3,2,11) -> 7* 100.01/26.18 f0(3,4,11) -> 7* 100.01/26.18 f0(11,1,4) -> 7* 100.01/26.18 f0(1,1,4) -> 7* 100.01/26.18 f0(11,3,4) -> 7* 100.01/26.19 f0(1,3,4) -> 7* 100.01/26.19 f0(11,2,9) -> 7* 100.01/26.19 f0(1,2,9) -> 7* 100.01/26.19 f0(11,4,9) -> 7* 100.01/26.19 f0(11,9,4) -> 7* 100.01/26.19 f0(1,4,9) -> 7* 100.01/26.19 f0(1,9,4) -> 7* 100.01/26.19 f0(11,11,4) -> 7* 100.01/26.19 f0(11,1,1) -> 7* 100.01/26.19 f0(9,1,2) -> 7* 100.01/26.19 f0(4,1,2) -> 7* 100.01/26.19 f0(1,11,4) -> 7* 100.01/26.19 f0(1,1,1) -> 7* 100.01/26.19 f0(11,3,1) -> 7* 100.01/26.19 f0(9,3,2) -> 7* 100.01/26.19 f0(4,3,2) -> 7* 100.01/26.19 f0(1,3,1) -> 7* 100.01/26.19 f0(9,1,11) -> 7* 100.01/26.19 f0(4,1,11) -> 7* 100.01/26.19 f0(9,3,11) -> 7* 100.01/26.19 f0(4,3,11) -> 7* 100.01/26.19 f0(11,9,1) -> 7* 100.01/26.19 f0(9,9,2) -> 7* 100.01/26.19 f0(4,9,2) -> 7* 100.01/26.19 f0(1,9,1) -> 7* 100.01/26.19 f0(11,11,1) -> 7* 100.01/26.19 f0(9,11,2) -> 7* 100.01/26.19 f0(4,11,2) -> 7* 100.01/26.19 f0(1,11,1) -> 7* 100.01/26.19 f0(2,2,4) -> 7* 100.01/26.19 f0(9,9,11) -> 7* 100.01/26.19 f0(4,9,11) -> 7* 100.01/26.19 f0(2,4,4) -> 7* 100.01/26.19 f0(9,11,11) -> 7* 100.01/26.19 f0(11,2,3) -> 7* 100.01/26.19 f0(4,11,11) -> 7* 100.01/26.19 f0(2,1,9) -> 7* 100.01/26.19 f0(1,2,3) -> 7* 100.01/26.19 f0(11,4,3) -> 7* 100.01/26.19 f0(2,3,9) -> 7* 100.01/26.19 f0(1,4,3) -> 7* 100.01/26.19 f0(2,2,1) -> 7* 100.01/26.19 f0(2,9,9) -> 7* 100.01/26.19 f0(2,4,1) -> 7* 100.01/26.19 f0(2,11,9) -> 7* 100.01/26.19 f0(3,1,4) -> 7* 100.01/26.19 f0(3,3,4) -> 7* 100.01/26.19 f0(2,1,3) -> 7* 100.01/26.19 f0(3,2,9) -> 7* 100.01/26.19 f0(2,3,3) -> 7* 100.01/26.19 f0(3,4,9) -> 7* 100.01/26.19 f0(3,9,4) -> 7* 100.01/26.19 f0(11,1,2) -> 7* 100.01/26.19 f0(3,11,4) -> 7* 100.01/26.19 f0(3,1,1) -> 7* 100.01/26.19 f0(1,1,2) -> 7* 100.01/26.19 f0(11,3,2) -> 7* 100.01/26.19 f0(3,3,1) -> 7* 100.01/26.19 f0(1,3,2) -> 7* 100.01/26.19 f0(11,1,11) -> 7* 100.01/26.19 f0(2,9,3) -> 7* 100.01/26.19 f0(11,3,11) -> 7* 100.01/26.19 f0(1,1,11) -> 7* 100.01/26.19 f0(2,11,3) -> 7* 100.01/26.19 f0(11,9,2) -> 7* 100.01/26.19 f0(1,3,11) -> 7* 100.01/26.19 f0(3,9,1) -> 7* 100.01/26.19 f0(1,9,2) -> 7* 100.01/26.19 f0(11,11,2) -> 7* 100.01/26.19 f0(9,2,4) -> 7* 100.01/26.19 f0(3,11,1) -> 7* 100.01/26.19 f0(1,11,2) -> 7* 100.01/26.19 f0(4,2,4) -> 7* 100.01/26.19 f0(11,9,11) -> 7* 100.01/26.19 f0(9,4,4) -> 7* 100.01/26.19 f0(4,4,4) -> 7* 100.01/26.19 f0(11,11,11) -> 7* 100.01/26.19 f0(1,9,11) -> 7* 100.01/26.19 f0(9,1,9) -> 7* 100.01/26.19 f0(4,1,9) -> 7* 100.01/26.19 f0(1,11,11) -> 7* 100.01/26.19 f0(9,3,9) -> 7* 100.01/26.19 f0(3,2,3) -> 7* 100.01/26.19 f0(4,3,9) -> 7* 100.01/26.19 f0(3,4,3) -> 7* 100.01/26.19 f0(9,2,1) -> 7* 100.01/26.19 f0(4,2,1) -> 7* 100.01/26.19 f0(2,2,2) -> 7* 100.01/26.19 f0(9,9,9) -> 7* 100.01/26.19 f0(9,4,1) -> 7* 100.01/26.19 f0(4,9,9) -> 7* 100.01/26.19 f0(4,4,1) -> 7* 100.01/26.19 f0(2,4,2) -> 7* 100.01/26.19 f0(9,11,9) -> 7* 100.01/26.19 f0(4,11,9) -> 7* 100.01/26.19 f0(2,2,11) -> 7* 100.01/26.19 f0(2,4,11) -> 7* 100.01/26.19 f0(9,1,3) -> 7* 100.01/26.19 f0(4,1,3) -> 7* 100.01/26.19 f0(9,3,3) -> 7* 100.01/26.19 f0(4,3,3) -> 7* 100.01/26.19 f0(3,1,2) -> 7* 100.01/26.19 f0(9,9,3) -> 7* 100.01/26.19 f0(3,3,2) -> 7* 100.01/26.19 f0(4,9,3) -> 7* 100.01/26.19 f0(9,11,3) -> 7* 100.01/26.19 f0(3,1,11) -> 7* 100.01/26.19 f0(4,11,3) -> 7* 100.01/26.19 f0(3,3,11) -> 7* 100.01/26.19 f0(3,9,2) -> 7* 100.01/26.19 f0(11,2,4) -> 7* 100.01/26.19 f0(3,11,2) -> 7* 100.01/26.19 f0(1,2,4) -> 7* 100.01/26.19 f0(11,4,4) -> 7* 100.01/26.19 f0(3,9,11) -> 7* 100.01/26.19 f0(11,1,9) -> 7* 100.01/26.19 f0(1,4,4) -> 7* 100.01/26.19 f0(3,11,11) -> 7* 100.01/26.19 f0(1,1,9) -> 7* 100.01/26.19 f0(11,3,9) -> 7* 100.01/26.19 f0(1,3,9) -> 7* 100.01/26.19 f0(11,2,1) -> 7* 100.01/26.19 f0(9,2,2) -> 7* 100.01/26.19 f0(4,2,2) -> 7* 100.01/26.19 f0(11,9,9) -> 7* 100.01/26.19 f0(1,2,1) -> 7* 100.01/26.19 f0(11,4,1) -> 7* 100.01/26.19 f0(9,4,2) -> 7* 100.01/26.19 f0(4,4,2) -> 7* 100.01/26.19 f0(1,9,9) -> 7* 100.01/26.19 f0(11,11,9) -> 7* 100.01/26.19 f0(1,4,1) -> 7* 100.01/26.19 f0(9,2,11) -> 7* 100.01/26.19 f0(1,11,9) -> 7* 100.01/26.19 f0(4,2,11) -> 7* 100.01/26.19 f0(9,4,11) -> 7* 100.01/26.19 f0(4,4,11) -> 7* 100.01/26.19 f0(2,1,4) -> 7* 100.01/26.19 f0(2,3,4) -> 7* 100.01/26.19 f0(11,1,3) -> 7* 100.01/26.19 f0(1,1,3) -> 7* 100.01/26.19 f0(11,3,3) -> 7* 100.01/26.19 f0(2,2,9) -> 7* 100.01/26.19 f0(1,3,3) -> 7* 100.01/26.19 f0(2,4,9) -> 7* 100.01/26.19 f0(2,9,4) -> 7* 100.01/26.19 f0(2,11,4) -> 7* 100.01/26.19 f0(2,1,1) -> 7* 100.01/26.19 f0(11,9,3) -> 7* 100.01/26.19 f0(2,3,1) -> 7* 100.01/26.19 f0(1,9,3) -> 7* 100.01/26.19 f0(11,11,3) -> 7* 100.01/26.19 f0(1,11,3) -> 7* 100.01/26.19 f0(2,9,1) -> 7* 100.01/26.19 f0(2,11,1) -> 7* 100.01/26.19 f0(3,2,4) -> 7* 100.01/26.19 f0(3,4,4) -> 7* 100.01/26.19 f0(3,1,9) -> 7* 100.01/26.19 f0(2,2,3) -> 7* 100.01/26.19 f0(3,3,9) -> 7* 100.01/26.19 f0(2,4,3) -> 7* 100.01/26.19 f0(11,2,2) -> 7* 100.01/26.19 f0(3,2,1) -> 7* 100.01/26.19 f0(1,2,2) -> 7* 100.01/26.19 f0(11,4,2) -> 7* 100.01/26.19 f0(3,9,9) -> 7* 100.01/26.19 f0(3,4,1) -> 7* 100.01/26.19 f0(1,4,2) -> 7* 100.01/26.19 f0(11,2,11) -> 7* 100.01/26.19 f0(3,11,9) -> 7* 100.01/26.19 f0(1,2,11) -> 7* 100.01/26.19 f0(11,4,11) -> 7* 100.01/26.19 f0(1,4,11) -> 7* 100.01/26.19 f0(9,1,4) -> 7* 100.01/26.19 f0(4,1,4) -> 7* 100.01/26.19 f0(9,3,4) -> 7* 100.01/26.19 f0(4,3,4) -> 7* 100.01/26.19 f0(9,2,9) -> 7* 100.01/26.19 f0(3,1,3) -> 7* 100.01/26.19 f0(4,2,9) -> 7* 100.01/26.19 f0(9,4,9) -> 7* 100.01/26.19 f0(9,9,4) -> 7* 100.01/26.19 f0(3,3,3) -> 7* 100.01/26.19 f0(4,4,9) -> 7* 100.01/26.19 f0(4,9,4) -> 7* 100.01/26.19 f0(9,11,4) -> 7* 100.01/26.19 f0(9,1,1) -> 7* 100.01/26.19 f0(4,11,4) -> 7* 100.01/26.19 f0(4,1,1) -> 7* 100.01/26.19 f0(2,1,2) -> 7* 100.01/26.19 f0(9,3,1) -> 7* 100.01/26.19 f0(4,3,1) -> 7* 100.01/26.19 f0(2,3,2) -> 7* 100.01/26.19 f0(3,9,3) -> 7* 100.01/26.19 f0(2,1,11) -> 7* 100.01/26.19 f0(3,11,3) -> 7* 100.01/26.19 f0(2,3,11) -> 7* 100.01/26.19 f0(9,9,1) -> 7* 100.01/26.19 f0(4,9,1) -> 7* 100.01/26.19 f0(2,9,2) -> 7* 100.01/26.19 f0(9,11,1) -> 7* 100.01/26.19 f0(4,11,1) -> 7* 100.01/26.19 f0(2,11,2) -> 7* 100.01/26.19 f0(2,9,11) -> 7* 100.01/26.19 f0(9,2,3) -> 7* 100.01/26.19 f0(2,11,11) -> 7* 100.01/26.19 f0(4,2,3) -> 7* 100.01/26.19 f0(9,4,3) -> 7* 100.01/26.19 f0(4,4,3) -> 7* 100.01/26.19 f0(3,2,2) -> 7* 100.01/26.19 proper0(2) -> 6* 100.01/26.19 proper0(9) -> 6* 100.01/26.19 proper0(4) -> 6* 100.01/26.19 proper0(11) -> 6* 100.01/26.19 proper0(1) -> 6* 100.01/26.19 proper0(3) -> 6* 100.01/26.19 mark0(7) -> 7* 100.01/26.19 mark0(2) -> 9*,5,1 100.01/26.19 mark0(9) -> 1* 100.01/26.19 mark0(4) -> 1* 100.01/26.19 mark0(11) -> 1* 100.01/26.19 mark0(1) -> 1* 100.01/26.19 mark0(3) -> 1* 100.01/26.19 a0() -> 2* 100.01/26.19 b0() -> 3* 100.01/26.19 top0(5) -> 8* 100.01/26.19 top0(2) -> 8* 100.01/26.19 top0(9) -> 8* 100.01/26.19 top0(4) -> 8* 100.01/26.19 top0(11) -> 8* 100.01/26.19 top0(6) -> 8* 100.01/26.19 top0(1) -> 8* 100.01/26.19 top0(3) -> 8* 100.01/26.19 ok0(7) -> 7* 100.01/26.19 ok0(2) -> 11*,6,4 100.01/26.19 ok0(9) -> 4* 100.01/26.19 ok0(4) -> 4* 100.01/26.19 ok0(11) -> 4* 100.01/26.19 ok0(1) -> 4* 100.01/26.19 ok0(3) -> 11*,6,4 100.01/26.19 problem: 100.01/26.19 strict: 100.01/26.19 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.01/26.19 weak: 100.01/26.19 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.01/26.19 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.01/26.19 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.01/26.19 active(b()) -> mark(a()) 100.01/26.19 top(mark(X)) -> top(proper(X)) 100.01/26.19 proper(a()) -> ok(a()) 100.01/26.19 proper(b()) -> ok(b()) 100.01/26.19 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.01/26.19 top(ok(X)) -> top(active(X)) 100.01/26.19 Bounds Processor: 100.01/26.19 bound: 0 100.01/26.19 enrichment: match 100.01/26.19 automaton: 100.01/26.19 final states: {11,9,8,7,6,5} 100.01/26.19 transitions: 100.01/26.19 active0(2) -> 6* 100.01/26.19 active0(9) -> 6* 100.01/26.19 active0(4) -> 6* 100.01/26.19 active0(11) -> 6* 100.01/26.19 active0(1) -> 6* 100.01/26.19 active0(3) -> 6* 100.01/26.19 f0(3,4,2) -> 7* 100.01/26.19 f0(3,2,11) -> 7* 100.01/26.19 f0(3,4,11) -> 7* 100.01/26.19 f0(11,1,4) -> 7* 100.01/26.19 f0(1,1,4) -> 7* 100.01/26.19 f0(11,3,4) -> 7* 100.01/26.19 f0(1,3,4) -> 7* 100.01/26.19 f0(11,2,9) -> 7* 100.01/26.19 f0(1,2,9) -> 7* 100.01/26.19 f0(11,4,9) -> 7* 100.01/26.19 f0(11,9,4) -> 7* 100.01/26.19 f0(1,4,9) -> 7* 100.01/26.19 f0(1,9,4) -> 7* 100.01/26.19 f0(11,11,4) -> 7* 100.01/26.19 f0(11,1,1) -> 7* 100.01/26.19 f0(9,1,2) -> 7* 100.01/26.19 f0(4,1,2) -> 7* 100.01/26.19 f0(1,11,4) -> 7* 100.01/26.19 f0(1,1,1) -> 7* 100.01/26.19 f0(11,3,1) -> 7* 100.01/26.19 f0(9,3,2) -> 7* 100.01/26.19 f0(4,3,2) -> 7* 100.01/26.19 f0(1,3,1) -> 7* 100.01/26.19 f0(9,1,11) -> 7* 100.01/26.19 f0(4,1,11) -> 7* 100.01/26.19 f0(9,3,11) -> 7* 100.01/26.19 f0(4,3,11) -> 7* 100.01/26.19 f0(11,9,1) -> 7* 100.01/26.19 f0(9,9,2) -> 7* 100.01/26.19 f0(4,9,2) -> 7* 100.01/26.19 f0(1,9,1) -> 7* 100.01/26.19 f0(11,11,1) -> 7* 100.01/26.19 f0(9,11,2) -> 7* 100.01/26.19 f0(4,11,2) -> 7* 100.01/26.19 f0(1,11,1) -> 7* 100.01/26.19 f0(2,2,4) -> 7* 100.01/26.19 f0(9,9,11) -> 7* 100.01/26.19 f0(4,9,11) -> 7* 100.01/26.19 f0(2,4,4) -> 7* 100.01/26.19 f0(9,11,11) -> 7* 100.01/26.19 f0(11,2,3) -> 7* 100.01/26.19 f0(4,11,11) -> 7* 100.01/26.19 f0(2,1,9) -> 7* 100.01/26.19 f0(1,2,3) -> 7* 100.01/26.19 f0(11,4,3) -> 7* 100.01/26.19 f0(2,3,9) -> 7* 100.01/26.19 f0(1,4,3) -> 7* 100.01/26.19 f0(2,2,1) -> 7* 100.01/26.19 f0(2,9,9) -> 7* 100.01/26.19 f0(2,4,1) -> 7* 100.01/26.19 f0(2,11,9) -> 7* 100.01/26.19 f0(3,1,4) -> 7* 100.01/26.19 f0(3,3,4) -> 7* 100.01/26.19 f0(2,1,3) -> 7* 100.01/26.19 f0(3,2,9) -> 7* 100.01/26.19 f0(2,3,3) -> 7* 100.01/26.19 f0(3,4,9) -> 7* 100.01/26.19 f0(3,9,4) -> 7* 100.01/26.19 f0(11,1,2) -> 7* 100.01/26.19 f0(3,11,4) -> 7* 100.01/26.19 f0(3,1,1) -> 7* 100.01/26.19 f0(1,1,2) -> 7* 100.01/26.19 f0(11,3,2) -> 7* 100.01/26.19 f0(3,3,1) -> 7* 100.01/26.19 f0(1,3,2) -> 7* 100.01/26.19 f0(11,1,11) -> 7* 100.01/26.19 f0(2,9,3) -> 7* 100.01/26.19 f0(11,3,11) -> 7* 100.01/26.19 f0(1,1,11) -> 7* 100.01/26.19 f0(2,11,3) -> 7* 100.01/26.19 f0(11,9,2) -> 7* 100.01/26.19 f0(1,3,11) -> 7* 100.01/26.19 f0(3,9,1) -> 7* 100.01/26.19 f0(1,9,2) -> 7* 100.01/26.19 f0(11,11,2) -> 7* 100.01/26.19 f0(9,2,4) -> 7* 100.01/26.19 f0(3,11,1) -> 7* 100.01/26.19 f0(1,11,2) -> 7* 100.01/26.19 f0(4,2,4) -> 7* 100.01/26.19 f0(11,9,11) -> 7* 100.01/26.19 f0(9,4,4) -> 7* 100.01/26.19 f0(4,4,4) -> 7* 100.01/26.19 f0(11,11,11) -> 7* 100.01/26.19 f0(1,9,11) -> 7* 100.01/26.19 f0(9,1,9) -> 7* 100.01/26.19 f0(4,1,9) -> 7* 100.01/26.19 f0(1,11,11) -> 7* 100.01/26.19 f0(9,3,9) -> 7* 100.01/26.19 f0(3,2,3) -> 7* 100.01/26.19 f0(4,3,9) -> 7* 100.01/26.19 f0(3,4,3) -> 7* 100.01/26.19 f0(9,2,1) -> 7* 100.01/26.19 f0(4,2,1) -> 7* 100.01/26.19 f0(2,2,2) -> 7* 100.01/26.19 f0(9,9,9) -> 7* 100.01/26.19 f0(9,4,1) -> 7* 100.01/26.19 f0(4,9,9) -> 7* 100.01/26.19 f0(4,4,1) -> 7* 100.01/26.19 f0(2,4,2) -> 7* 100.01/26.19 f0(9,11,9) -> 7* 100.01/26.19 f0(4,11,9) -> 7* 100.01/26.19 f0(2,2,11) -> 7* 100.01/26.19 f0(2,4,11) -> 7* 100.01/26.19 f0(9,1,3) -> 7* 100.01/26.19 f0(4,1,3) -> 7* 100.01/26.19 f0(9,3,3) -> 7* 100.01/26.19 f0(4,3,3) -> 7* 100.01/26.19 f0(3,1,2) -> 7* 100.01/26.19 f0(9,9,3) -> 7* 100.01/26.19 f0(3,3,2) -> 7* 100.01/26.19 f0(4,9,3) -> 7* 100.01/26.19 f0(9,11,3) -> 7* 100.01/26.19 f0(3,1,11) -> 7* 100.01/26.19 f0(4,11,3) -> 7* 100.01/26.19 f0(3,3,11) -> 7* 100.01/26.19 f0(3,9,2) -> 7* 100.01/26.19 f0(11,2,4) -> 7* 100.01/26.19 f0(3,11,2) -> 7* 100.01/26.19 f0(1,2,4) -> 7* 100.01/26.19 f0(11,4,4) -> 7* 100.01/26.19 f0(3,9,11) -> 7* 100.01/26.19 f0(11,1,9) -> 7* 100.01/26.19 f0(1,4,4) -> 7* 100.01/26.19 f0(3,11,11) -> 7* 100.01/26.19 f0(1,1,9) -> 7* 100.01/26.19 f0(11,3,9) -> 7* 100.01/26.19 f0(1,3,9) -> 7* 100.01/26.19 f0(11,2,1) -> 7* 100.01/26.19 f0(9,2,2) -> 7* 100.01/26.19 f0(4,2,2) -> 7* 100.01/26.19 f0(11,9,9) -> 7* 100.01/26.19 f0(1,2,1) -> 7* 100.01/26.19 f0(11,4,1) -> 7* 100.01/26.19 f0(9,4,2) -> 7* 100.01/26.19 f0(4,4,2) -> 7* 100.01/26.19 f0(1,9,9) -> 7* 100.01/26.19 f0(11,11,9) -> 7* 100.01/26.19 f0(1,4,1) -> 7* 100.01/26.19 f0(9,2,11) -> 7* 100.01/26.19 f0(1,11,9) -> 7* 100.01/26.19 f0(4,2,11) -> 7* 100.01/26.19 f0(9,4,11) -> 7* 100.01/26.19 f0(4,4,11) -> 7* 100.01/26.19 f0(2,1,4) -> 7* 100.01/26.19 f0(2,3,4) -> 7* 100.01/26.19 f0(11,1,3) -> 7* 100.01/26.19 f0(1,1,3) -> 7* 100.01/26.19 f0(11,3,3) -> 7* 100.01/26.19 f0(2,2,9) -> 7* 100.01/26.19 f0(1,3,3) -> 7* 100.01/26.19 f0(2,4,9) -> 7* 100.01/26.19 f0(2,9,4) -> 7* 100.01/26.19 f0(2,11,4) -> 7* 100.01/26.19 f0(2,1,1) -> 7* 100.01/26.19 f0(11,9,3) -> 7* 100.01/26.19 f0(2,3,1) -> 7* 100.01/26.19 f0(1,9,3) -> 7* 100.01/26.19 f0(11,11,3) -> 7* 100.01/26.19 f0(1,11,3) -> 7* 100.01/26.19 f0(2,9,1) -> 7* 100.01/26.19 f0(2,11,1) -> 7* 100.01/26.19 f0(3,2,4) -> 7* 100.01/26.19 f0(3,4,4) -> 7* 100.01/26.19 f0(3,1,9) -> 7* 100.01/26.19 f0(2,2,3) -> 7* 100.01/26.19 f0(3,3,9) -> 7* 100.11/26.20 f0(2,4,3) -> 7* 100.11/26.20 f0(11,2,2) -> 7* 100.11/26.20 f0(3,2,1) -> 7* 100.11/26.20 f0(1,2,2) -> 7* 100.11/26.20 f0(11,4,2) -> 7* 100.11/26.20 f0(3,9,9) -> 7* 100.11/26.20 f0(3,4,1) -> 7* 100.11/26.20 f0(1,4,2) -> 7* 100.11/26.20 f0(11,2,11) -> 7* 100.11/26.20 f0(3,11,9) -> 7* 100.11/26.20 f0(1,2,11) -> 7* 100.11/26.20 f0(11,4,11) -> 7* 100.11/26.20 f0(1,4,11) -> 7* 100.11/26.20 f0(9,1,4) -> 7* 100.11/26.20 f0(4,1,4) -> 7* 100.11/26.20 f0(9,3,4) -> 7* 100.11/26.20 f0(4,3,4) -> 7* 100.11/26.20 f0(9,2,9) -> 7* 100.11/26.20 f0(3,1,3) -> 7* 100.11/26.20 f0(4,2,9) -> 7* 100.11/26.20 f0(9,4,9) -> 7* 100.11/26.20 f0(9,9,4) -> 7* 100.11/26.20 f0(3,3,3) -> 7* 100.11/26.20 f0(4,4,9) -> 7* 100.11/26.20 f0(4,9,4) -> 7* 100.11/26.20 f0(9,11,4) -> 7* 100.11/26.20 f0(9,1,1) -> 7* 100.11/26.20 f0(4,11,4) -> 7* 100.11/26.20 f0(4,1,1) -> 7* 100.11/26.20 f0(2,1,2) -> 7* 100.11/26.20 f0(9,3,1) -> 7* 100.11/26.20 f0(4,3,1) -> 7* 100.11/26.20 f0(2,3,2) -> 7* 100.11/26.20 f0(3,9,3) -> 7* 100.11/26.20 f0(2,1,11) -> 7* 100.11/26.20 f0(3,11,3) -> 7* 100.11/26.20 f0(2,3,11) -> 7* 100.11/26.20 f0(9,9,1) -> 7* 100.11/26.20 f0(4,9,1) -> 7* 100.11/26.20 f0(2,9,2) -> 7* 100.11/26.20 f0(9,11,1) -> 7* 100.11/26.20 f0(4,11,1) -> 7* 100.11/26.20 f0(2,11,2) -> 7* 100.11/26.20 f0(2,9,11) -> 7* 100.11/26.20 f0(9,2,3) -> 7* 100.11/26.20 f0(2,11,11) -> 7* 100.11/26.20 f0(4,2,3) -> 7* 100.11/26.20 f0(9,4,3) -> 7* 100.11/26.20 f0(4,4,3) -> 7* 100.11/26.20 f0(3,2,2) -> 7* 100.11/26.20 proper0(2) -> 5* 100.11/26.20 proper0(9) -> 5* 100.11/26.20 proper0(4) -> 5* 100.11/26.20 proper0(11) -> 5* 100.11/26.20 proper0(1) -> 5* 100.11/26.20 proper0(3) -> 5* 100.11/26.20 mark0(7) -> 7* 100.11/26.20 mark0(2) -> 9*,6,1 100.11/26.20 mark0(9) -> 1* 100.11/26.20 mark0(4) -> 1* 100.11/26.20 mark0(11) -> 1* 100.11/26.20 mark0(1) -> 1* 100.11/26.20 mark0(3) -> 1* 100.11/26.20 a0() -> 2* 100.11/26.20 b0() -> 3* 100.11/26.20 top0(5) -> 8* 100.11/26.20 top0(2) -> 8* 100.11/26.20 top0(9) -> 8* 100.11/26.20 top0(4) -> 8* 100.11/26.20 top0(11) -> 8* 100.11/26.20 top0(6) -> 8* 100.11/26.20 top0(1) -> 8* 100.11/26.20 top0(3) -> 8* 100.11/26.20 ok0(7) -> 7* 100.11/26.20 ok0(2) -> 11*,5,4 100.11/26.20 ok0(9) -> 4* 100.11/26.20 ok0(4) -> 4* 100.11/26.20 ok0(11) -> 4* 100.11/26.20 ok0(1) -> 4* 100.11/26.20 ok0(3) -> 11*,5,4 100.11/26.20 problem: 100.11/26.20 strict: 100.11/26.20 100.11/26.20 weak: 100.11/26.20 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.11/26.20 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.11/26.20 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.11/26.20 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.11/26.20 active(b()) -> mark(a()) 100.11/26.20 top(mark(X)) -> top(proper(X)) 100.11/26.20 proper(a()) -> ok(a()) 100.11/26.20 proper(b()) -> ok(b()) 100.11/26.20 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.11/26.20 top(ok(X)) -> top(active(X)) 100.11/26.20 Qed 100.11/26.20 100.11/26.20 strict: 100.11/26.20 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.11/26.20 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.11/26.20 weak: 100.11/26.20 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.11/26.20 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.11/26.20 active(b()) -> mark(a()) 100.11/26.20 top(mark(X)) -> top(proper(X)) 100.11/26.20 proper(a()) -> ok(a()) 100.11/26.20 proper(b()) -> ok(b()) 100.11/26.20 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.11/26.20 top(ok(X)) -> top(active(X)) 100.11/26.20 Bounds Processor: 100.11/26.20 bound: 1 100.11/26.20 enrichment: match 100.11/26.20 automaton: 100.11/26.20 final states: {16,14,12,8,7,6,5} 100.11/26.20 transitions: 100.11/26.20 active0(2) -> 6* 100.11/26.20 active0(14) -> 6* 100.11/26.20 active0(4) -> 6* 100.11/26.20 active0(16) -> 6* 100.11/26.20 active0(1) -> 6* 100.11/26.20 active0(3) -> 6* 100.11/26.20 f0(3,4,2) -> 5* 100.11/26.20 f0(16,3,16) -> 5* 100.11/26.20 f0(14,14,3) -> 5* 100.11/26.20 f0(1,3,16) -> 5* 100.11/26.20 f0(16,1,4) -> 5* 100.11/26.20 f0(3,14,14) -> 5* 100.11/26.20 f0(14,16,3) -> 5* 100.11/26.20 f0(4,14,3) -> 5* 100.11/26.20 f0(3,1,16) -> 5* 100.11/26.20 f0(16,3,4) -> 5* 100.11/26.20 f0(3,16,14) -> 5* 100.11/26.20 f0(4,16,3) -> 5* 100.11/26.20 f0(1,1,4) -> 5* 100.11/26.20 f0(14,1,14) -> 5* 100.11/26.20 f0(1,3,4) -> 5* 100.11/26.20 f0(3,14,2) -> 5* 100.11/26.20 f0(14,3,14) -> 5* 100.11/26.20 f0(4,1,14) -> 5* 100.11/26.20 f0(3,16,2) -> 5* 100.11/26.20 f0(4,3,14) -> 5* 100.11/26.20 f0(16,1,1) -> 5* 100.11/26.20 f0(14,1,2) -> 5* 100.11/26.20 f0(16,3,1) -> 5* 100.11/26.20 f0(14,3,2) -> 5* 100.11/26.20 f0(4,1,2) -> 5* 100.11/26.20 f0(1,1,1) -> 5* 100.11/26.20 f0(4,3,2) -> 5* 100.11/26.20 f0(1,3,1) -> 5* 100.11/26.20 f0(2,2,16) -> 5* 100.11/26.20 f0(2,4,16) -> 5* 100.11/26.20 f0(2,2,4) -> 5* 100.11/26.20 f0(2,4,4) -> 5* 100.11/26.20 f0(16,2,3) -> 5* 100.11/26.20 f0(16,4,3) -> 5* 100.11/26.20 f0(1,2,3) -> 5* 100.11/26.20 f0(2,14,16) -> 5* 100.11/26.20 f0(1,4,3) -> 5* 100.11/26.20 f0(2,16,16) -> 5* 100.11/26.20 f0(2,2,1) -> 5* 100.11/26.20 f0(2,14,4) -> 5* 100.11/26.20 f0(2,4,1) -> 5* 100.11/26.20 f0(2,16,4) -> 5* 100.11/26.20 f0(16,14,3) -> 5* 100.11/26.20 f0(3,3,16) -> 5* 100.11/26.20 f0(16,16,3) -> 5* 100.11/26.20 f0(1,14,3) -> 5* 100.11/26.20 f0(3,1,4) -> 5* 100.11/26.20 f0(1,16,3) -> 5* 100.11/26.20 f0(16,1,14) -> 5* 100.11/26.20 f0(3,3,4) -> 5* 100.11/26.20 f0(2,14,1) -> 5* 100.11/26.20 f0(16,3,14) -> 5* 100.11/26.20 f0(1,1,14) -> 5* 100.11/26.20 f0(2,1,3) -> 5* 100.11/26.20 f0(2,16,1) -> 5* 100.11/26.20 f0(1,3,14) -> 5* 100.11/26.20 f0(2,3,3) -> 5* 100.11/26.20 f0(16,1,2) -> 5* 100.11/26.20 f0(16,3,2) -> 5* 100.11/26.20 f0(3,1,1) -> 5* 100.11/26.20 f0(1,1,2) -> 5* 100.11/26.20 f0(3,3,1) -> 5* 100.11/26.20 f0(1,3,2) -> 5* 100.11/26.20 f0(14,2,16) -> 5* 100.11/26.20 f0(4,2,16) -> 5* 100.11/26.20 f0(14,4,16) -> 5* 100.11/26.20 f0(4,4,16) -> 5* 100.11/26.20 f0(14,2,4) -> 5* 100.11/26.20 f0(14,4,4) -> 5* 100.11/26.20 f0(4,2,4) -> 5* 100.11/26.20 f0(4,4,4) -> 5* 100.11/26.20 f0(14,14,16) -> 5* 100.11/26.20 f0(2,2,14) -> 5* 100.11/26.20 f0(3,2,3) -> 5* 100.11/26.20 f0(14,16,16) -> 5* 100.11/26.20 f0(4,14,16) -> 5* 100.11/26.20 f0(2,4,14) -> 5* 100.11/26.20 f0(3,4,3) -> 5* 100.11/26.20 f0(14,2,1) -> 5* 100.11/26.20 f0(4,16,16) -> 5* 100.11/26.20 f0(14,14,4) -> 5* 100.11/26.20 f0(14,4,1) -> 5* 100.11/26.20 f0(4,2,1) -> 5* 100.11/26.20 f0(2,2,2) -> 5* 100.11/26.20 f0(14,16,4) -> 5* 100.11/26.20 f0(4,14,4) -> 5* 100.11/26.20 f0(4,4,1) -> 5* 100.11/26.20 f0(2,4,2) -> 5* 100.11/26.20 f0(4,16,4) -> 5* 100.11/26.20 f0(2,14,14) -> 5* 100.11/26.20 f0(3,14,3) -> 5* 100.11/26.20 f0(2,1,16) -> 5* 100.11/26.20 f0(2,16,14) -> 5* 100.11/26.20 f0(3,16,3) -> 5* 100.11/26.20 f0(14,14,1) -> 5* 100.11/26.20 f0(14,1,3) -> 5* 100.11/26.20 f0(14,16,1) -> 5* 100.11/26.20 f0(4,14,1) -> 5* 100.11/26.20 f0(2,14,2) -> 5* 100.11/26.20 f0(3,1,14) -> 5* 100.11/26.20 f0(14,3,3) -> 5* 100.11/26.20 f0(4,1,3) -> 5* 100.11/26.20 f0(4,16,1) -> 5* 100.11/26.20 f0(2,16,2) -> 5* 100.11/26.20 f0(3,3,14) -> 5* 100.11/26.20 f0(4,3,3) -> 5* 100.11/26.20 f0(3,1,2) -> 5* 100.11/26.20 f0(3,3,2) -> 5* 100.11/26.20 f0(16,2,16) -> 5* 100.11/26.20 f0(16,4,16) -> 5* 100.11/26.20 f0(1,2,16) -> 5* 100.11/26.20 f0(1,4,16) -> 5* 100.11/26.20 f0(16,2,4) -> 5* 100.11/26.20 f0(16,4,4) -> 5* 100.11/26.20 f0(1,2,4) -> 5* 100.11/26.20 f0(14,2,14) -> 5* 100.11/26.20 f0(1,4,4) -> 5* 100.11/26.20 f0(16,14,16) -> 5* 100.11/26.20 f0(4,2,14) -> 5* 100.11/26.20 f0(14,4,14) -> 5* 100.11/26.20 f0(16,16,16) -> 5* 100.11/26.20 f0(4,4,14) -> 5* 100.11/26.20 f0(1,14,16) -> 5* 100.11/26.20 f0(16,2,1) -> 5* 100.11/26.20 f0(14,2,2) -> 5* 100.11/26.20 f0(1,16,16) -> 5* 100.11/26.20 f0(16,14,4) -> 5* 100.11/26.20 f0(16,4,1) -> 5* 100.11/26.20 f0(14,4,2) -> 5* 100.11/26.20 f0(4,2,2) -> 5* 100.11/26.20 f0(1,2,1) -> 5* 100.11/26.20 f0(16,16,4) -> 5* 100.11/26.20 f0(4,4,2) -> 5* 100.11/26.20 f0(1,14,4) -> 5* 100.11/26.20 f0(1,4,1) -> 5* 100.11/26.20 f0(14,14,14) -> 5* 100.11/26.20 f0(1,16,4) -> 5* 100.11/26.20 f0(2,3,16) -> 5* 100.11/26.20 f0(14,16,14) -> 5* 100.11/26.20 f0(4,14,14) -> 5* 100.11/26.20 f0(4,16,14) -> 5* 100.11/26.20 f0(2,1,4) -> 5* 100.11/26.20 f0(16,14,1) -> 5* 100.11/26.20 f0(14,14,2) -> 5* 100.11/26.20 f0(2,3,4) -> 5* 100.11/26.20 f0(16,1,3) -> 5* 100.11/26.20 f0(16,16,1) -> 5* 100.11/26.20 f0(14,16,2) -> 5* 100.11/26.20 f0(4,14,2) -> 5* 100.11/26.20 f0(1,14,1) -> 5* 100.11/26.20 f0(16,3,3) -> 5* 100.11/26.20 f0(4,16,2) -> 5* 100.11/26.20 f0(1,1,3) -> 5* 100.11/26.20 f0(1,16,1) -> 5* 100.11/26.20 f0(1,3,3) -> 5* 100.11/26.20 f0(2,1,1) -> 5* 100.11/26.20 f0(2,3,1) -> 5* 100.11/26.20 f0(3,2,16) -> 5* 100.11/26.20 f0(3,4,16) -> 5* 100.11/26.20 f0(3,2,4) -> 5* 100.11/26.20 f0(16,2,14) -> 5* 100.11/26.20 f0(3,4,4) -> 5* 100.11/26.20 f0(16,4,14) -> 5* 100.11/26.20 f0(1,2,14) -> 5* 100.11/26.20 f0(2,2,3) -> 5* 100.11/26.20 f0(3,14,16) -> 5* 100.11/26.20 f0(1,4,14) -> 5* 100.11/26.20 f0(2,4,3) -> 5* 100.11/26.20 f0(16,2,2) -> 5* 100.11/26.20 f0(3,16,16) -> 5* 100.11/26.20 f0(16,4,2) -> 5* 100.11/26.20 f0(3,2,1) -> 5* 100.11/26.20 f0(1,2,2) -> 5* 100.11/26.20 f0(14,1,16) -> 5* 100.11/26.20 f0(3,14,4) -> 5* 100.11/26.20 f0(3,4,1) -> 5* 100.11/26.20 f0(1,4,2) -> 5* 100.11/26.20 f0(14,3,16) -> 5* 100.11/26.20 f0(4,1,16) -> 5* 100.11/26.20 f0(16,14,14) -> 5* 100.11/26.20 f0(3,16,4) -> 5* 100.11/26.20 f0(4,3,16) -> 5* 100.11/26.20 f0(16,16,14) -> 5* 100.11/26.20 f0(14,1,4) -> 5* 100.11/26.20 f0(1,14,14) -> 5* 100.11/26.21 f0(2,14,3) -> 5* 100.11/26.21 f0(1,1,16) -> 5* 100.11/26.21 f0(1,16,14) -> 5* 100.11/26.21 f0(14,3,4) -> 5* 100.11/26.21 f0(4,1,4) -> 5* 100.11/26.21 f0(2,16,3) -> 5* 100.11/26.21 f0(16,14,2) -> 5* 100.11/26.21 f0(4,3,4) -> 5* 100.11/26.21 f0(16,16,2) -> 5* 100.11/26.21 f0(3,14,1) -> 5* 100.11/26.21 f0(1,14,2) -> 5* 100.11/26.21 f0(2,1,14) -> 5* 100.11/26.21 f0(3,1,3) -> 5* 100.11/26.21 f0(3,16,1) -> 5* 100.11/26.21 f0(1,16,2) -> 5* 100.11/26.21 f0(2,3,14) -> 5* 100.11/26.21 f0(3,3,3) -> 5* 100.11/26.21 f0(14,1,1) -> 5* 100.11/26.21 f0(14,3,1) -> 5* 100.11/26.21 f0(4,1,1) -> 5* 100.11/26.21 f0(2,1,2) -> 5* 100.11/26.21 f0(4,3,1) -> 5* 100.11/26.21 f0(2,3,2) -> 5* 100.11/26.21 f0(14,2,3) -> 5* 100.11/26.21 f0(3,2,14) -> 5* 100.11/26.21 f0(14,4,3) -> 5* 100.11/26.21 f0(4,2,3) -> 5* 100.11/26.21 f0(3,4,14) -> 5* 100.11/26.21 f0(4,4,3) -> 5* 100.11/26.21 f0(3,2,2) -> 5* 100.11/26.21 f0(16,1,16) -> 5* 100.11/26.21 proper0(2) -> 8* 100.11/26.21 proper0(14) -> 8* 100.11/26.21 proper0(4) -> 8* 100.11/26.21 proper0(16) -> 8* 100.11/26.21 proper0(1) -> 8* 100.11/26.21 proper0(3) -> 8* 100.11/26.21 mark0(2) -> 14*,6,1 100.11/26.21 mark0(14) -> 1* 100.11/26.21 mark0(4) -> 1* 100.11/26.21 mark0(16) -> 1* 100.11/26.21 mark0(1) -> 1* 100.11/26.21 mark0(3) -> 1* 100.11/26.21 a0() -> 2* 100.11/26.21 b0() -> 3* 100.11/26.21 top0(2) -> 7* 100.11/26.21 top0(14) -> 7* 100.11/26.21 top0(4) -> 7* 100.11/26.21 top0(16) -> 7* 100.11/26.21 top0(6) -> 7* 100.11/26.21 top0(1) -> 7* 100.11/26.21 top0(8) -> 7* 100.11/26.21 top0(3) -> 7* 100.11/26.21 ok0(5) -> 5* 100.11/26.21 ok0(12) -> 5* 100.11/26.21 ok0(2) -> 16*,8,4 100.11/26.21 ok0(14) -> 4* 100.11/26.21 ok0(4) -> 4* 100.11/26.21 ok0(16) -> 4* 100.11/26.21 ok0(1) -> 4* 100.11/26.21 ok0(3) -> 16*,8,4 100.11/26.21 mark1(10) -> 5* 100.11/26.21 mark1(5) -> 12* 100.11/26.21 mark1(12) -> 12*,5 100.11/26.21 f1(3,2,2) -> 12*,5,10 100.11/26.21 f1(16,1,16) -> 5,12* 100.11/26.21 f1(3,4,2) -> 12*,5,10 100.11/26.21 f1(16,3,16) -> 5,12* 100.11/26.21 f1(14,14,3) -> 5,12* 100.11/26.21 f1(1,3,16) -> 5,12* 100.11/26.21 f1(16,1,4) -> 5,12* 100.11/26.21 f1(3,14,14) -> 5,12* 100.11/26.21 f1(14,16,3) -> 5,12* 100.11/26.21 f1(4,14,3) -> 5,12* 100.11/26.21 f1(3,1,16) -> 5,12* 100.11/26.21 f1(16,3,4) -> 5,12* 100.11/26.21 f1(3,16,14) -> 5,12* 100.11/26.21 f1(4,16,3) -> 5,12* 100.11/26.21 f1(1,1,4) -> 12*,5,10 100.11/26.21 f1(14,1,14) -> 5,12* 100.11/26.21 f1(1,3,4) -> 12*,5,10 100.11/26.21 f1(3,14,2) -> 5,12* 100.11/26.21 f1(14,3,14) -> 5,12* 100.11/26.21 f1(4,1,14) -> 5,12* 100.11/26.21 f1(3,16,2) -> 5,12* 100.11/26.21 f1(4,3,14) -> 5,12* 100.11/26.21 f1(16,1,1) -> 5,12* 100.11/26.21 f1(14,1,2) -> 5,12* 100.11/26.21 f1(16,3,1) -> 5,12* 100.11/26.21 f1(14,3,2) -> 5,12* 100.11/26.21 f1(4,1,2) -> 12*,5,10 100.11/26.21 f1(1,1,1) -> 12*,5,10 100.11/26.21 f1(4,3,2) -> 12*,5,10 100.11/26.21 f1(1,3,1) -> 12*,5,10 100.11/26.21 f1(2,2,16) -> 5,12* 100.11/26.21 f1(2,4,16) -> 5,12* 100.11/26.21 f1(2,2,4) -> 12*,5,10 100.11/26.21 f1(2,4,4) -> 12*,5,10 100.11/26.21 f1(16,2,3) -> 5,12* 100.11/26.21 f1(16,4,3) -> 5,12* 100.11/26.21 f1(1,2,3) -> 12*,5,10 100.11/26.21 f1(2,14,16) -> 5,12* 100.11/26.21 f1(1,4,3) -> 12*,5,10 100.11/26.21 f1(2,16,16) -> 5,12* 100.11/26.21 f1(2,2,1) -> 12*,5,10 100.11/26.21 f1(2,14,4) -> 5,12* 100.11/26.21 f1(2,4,1) -> 12*,5,10 100.11/26.21 f1(2,16,4) -> 5,12* 100.11/26.21 f1(16,14,3) -> 5,12* 100.11/26.21 f1(3,3,16) -> 5,12* 100.11/26.21 f1(16,16,3) -> 5,12* 100.11/26.21 f1(1,14,3) -> 5,12* 100.11/26.21 f1(3,1,4) -> 12*,5,10 100.11/26.21 f1(1,16,3) -> 5,12* 100.11/26.21 f1(16,1,14) -> 5,12* 100.11/26.21 f1(3,3,4) -> 12*,5,10 100.11/26.21 f1(2,14,1) -> 5,12* 100.11/26.21 f1(16,3,14) -> 5,12* 100.11/26.21 f1(1,1,14) -> 5,12* 100.11/26.21 f1(2,1,3) -> 12*,5,10 100.11/26.21 f1(2,16,1) -> 5,12* 100.11/26.21 f1(1,3,14) -> 5,12* 100.11/26.21 f1(2,3,3) -> 12*,5,10 100.11/26.21 f1(16,1,2) -> 5,12* 100.11/26.21 f1(16,3,2) -> 5,12* 100.11/26.21 f1(3,1,1) -> 12*,5,10 100.11/26.21 f1(1,1,2) -> 12*,5,10 100.11/26.21 f1(3,3,1) -> 12*,5,10 100.11/26.21 f1(1,3,2) -> 12*,5,10 100.11/26.21 f1(14,2,16) -> 5,12* 100.11/26.21 f1(4,2,16) -> 5,12* 100.11/26.21 f1(14,4,16) -> 5,12* 100.11/26.21 f1(4,4,16) -> 5,12* 100.11/26.21 f1(14,2,4) -> 5,12* 100.11/26.21 f1(14,4,4) -> 5,12* 100.11/26.21 f1(4,2,4) -> 12*,5,10 100.11/26.21 f1(4,4,4) -> 12*,5,10 100.11/26.21 f1(14,14,16) -> 5,12* 100.11/26.21 f1(2,2,14) -> 5,12* 100.11/26.21 f1(3,2,3) -> 12*,5,10 100.11/26.21 f1(14,16,16) -> 5,12* 100.11/26.21 f1(4,14,16) -> 5,12* 100.11/26.21 f1(2,4,14) -> 5,12* 100.11/26.21 f1(3,4,3) -> 12*,5,10 100.11/26.21 f1(14,2,1) -> 5,12* 100.11/26.21 f1(4,16,16) -> 5,12* 100.11/26.21 f1(14,14,4) -> 5,12* 100.11/26.21 f1(14,4,1) -> 5,12* 100.11/26.21 f1(4,2,1) -> 12*,5,10 100.11/26.21 f1(2,2,2) -> 12*,5,10 100.11/26.21 f1(14,16,4) -> 5,12* 100.11/26.21 f1(4,14,4) -> 5,12* 100.11/26.21 f1(4,4,1) -> 12*,5,10 100.11/26.21 f1(2,4,2) -> 12*,5,10 100.11/26.21 f1(4,16,4) -> 5,12* 100.11/26.21 f1(2,14,14) -> 5,12* 100.11/26.21 f1(3,14,3) -> 5,12* 100.11/26.21 f1(2,1,16) -> 5,12* 100.11/26.21 f1(2,16,14) -> 5,12* 100.11/26.21 f1(3,16,3) -> 5,12* 100.11/26.21 f1(14,14,1) -> 5,12* 100.11/26.21 f1(14,1,3) -> 5,12* 100.11/26.21 f1(14,16,1) -> 5,12* 100.11/26.21 f1(4,14,1) -> 5,12* 100.11/26.21 f1(2,14,2) -> 5,12* 100.11/26.21 f1(3,1,14) -> 5,12* 100.11/26.21 f1(14,3,3) -> 5,12* 100.11/26.21 f1(4,1,3) -> 12*,5,10 100.11/26.21 f1(4,16,1) -> 5,12* 100.11/26.21 f1(2,16,2) -> 5,12* 100.11/26.21 f1(3,3,14) -> 5,12* 100.11/26.21 f1(4,3,3) -> 12*,5,10 100.11/26.21 f1(3,1,2) -> 12*,5,10 100.11/26.21 f1(3,3,2) -> 12*,5,10 100.11/26.21 f1(16,2,16) -> 5,12* 100.11/26.21 f1(16,4,16) -> 5,12* 100.11/26.21 f1(1,2,16) -> 5,12* 100.11/26.21 f1(1,4,16) -> 5,12* 100.11/26.21 f1(16,2,4) -> 5,12* 100.11/26.21 f1(16,4,4) -> 5,12* 100.11/26.21 f1(1,2,4) -> 12*,5,10 100.11/26.21 f1(14,2,14) -> 5,12* 100.11/26.21 f1(1,4,4) -> 12*,5,10 100.11/26.21 f1(16,14,16) -> 5,12* 100.11/26.21 f1(4,2,14) -> 5,12* 100.11/26.21 f1(14,4,14) -> 5,12* 100.11/26.21 f1(16,16,16) -> 5,12* 100.11/26.21 f1(4,4,14) -> 5,12* 100.11/26.21 f1(1,14,16) -> 5,12* 100.11/26.21 f1(16,2,1) -> 5,12* 100.11/26.21 f1(14,2,2) -> 5,12* 100.11/26.21 f1(1,16,16) -> 5,12* 100.11/26.21 f1(16,14,4) -> 5,12* 100.11/26.21 f1(16,4,1) -> 5,12* 100.11/26.21 f1(14,4,2) -> 5,12* 100.11/26.21 f1(4,2,2) -> 12*,5,10 100.11/26.21 f1(1,2,1) -> 12*,5,10 100.11/26.21 f1(16,16,4) -> 5,12* 100.11/26.21 f1(4,4,2) -> 12*,5,10 100.11/26.21 f1(1,14,4) -> 5,12* 100.11/26.21 f1(1,4,1) -> 12*,5,10 100.11/26.21 f1(14,14,14) -> 5,12* 100.11/26.21 f1(1,16,4) -> 5,12* 100.11/26.21 f1(2,3,16) -> 5,12* 100.11/26.21 f1(14,16,14) -> 5,12* 100.11/26.21 f1(4,14,14) -> 5,12* 100.11/26.21 f1(4,16,14) -> 5,12* 100.11/26.21 f1(2,1,4) -> 12*,5,10 100.11/26.21 f1(16,14,1) -> 5,12* 100.11/26.21 f1(14,14,2) -> 5,12* 100.11/26.21 f1(2,3,4) -> 12*,5,10 100.11/26.21 f1(16,1,3) -> 5,12* 100.11/26.21 f1(16,16,1) -> 5,12* 100.11/26.21 f1(14,16,2) -> 5,12* 100.11/26.21 f1(4,14,2) -> 5,12* 100.11/26.21 f1(1,14,1) -> 5,12* 100.11/26.21 f1(16,3,3) -> 5,12* 100.11/26.21 f1(4,16,2) -> 5,12* 100.11/26.21 f1(1,1,3) -> 12*,5,10 100.11/26.21 f1(1,16,1) -> 5,12* 100.11/26.21 f1(1,3,3) -> 12*,5,10 100.11/26.21 f1(2,1,1) -> 12*,5,10 100.11/26.21 f1(2,3,1) -> 12*,5,10 100.11/26.21 f1(3,2,16) -> 5,12* 100.11/26.21 f1(3,4,16) -> 5,12* 100.11/26.21 f1(3,2,4) -> 12*,5,10 100.11/26.21 f1(16,2,14) -> 5,12* 100.11/26.21 f1(3,4,4) -> 12*,5,10 100.11/26.21 f1(16,4,14) -> 5,12* 100.11/26.21 f1(1,2,14) -> 5,12* 100.11/26.21 f1(2,2,3) -> 12*,5,10 100.11/26.21 f1(3,14,16) -> 5,12* 100.11/26.21 f1(1,4,14) -> 5,12* 100.11/26.21 f1(2,4,3) -> 12*,5,10 100.11/26.21 f1(16,2,2) -> 5,12* 100.11/26.21 f1(3,16,16) -> 5,12* 100.11/26.21 f1(16,4,2) -> 5,12* 100.11/26.21 f1(3,2,1) -> 12*,5,10 100.11/26.21 f1(1,2,2) -> 12*,5,10 100.11/26.21 f1(14,1,16) -> 5,12* 100.11/26.21 f1(3,14,4) -> 5,12* 100.11/26.21 f1(3,4,1) -> 12*,5,10 100.11/26.21 f1(1,4,2) -> 12*,5,10 100.11/26.21 f1(14,3,16) -> 5,12* 100.11/26.21 f1(4,1,16) -> 5,12* 100.11/26.21 f1(16,14,14) -> 5,12* 100.11/26.21 f1(3,16,4) -> 5,12* 100.11/26.21 f1(4,3,16) -> 5,12* 100.11/26.21 f1(16,16,14) -> 5,12* 100.11/26.21 f1(14,1,4) -> 5,12* 100.11/26.21 f1(1,14,14) -> 5,12* 100.11/26.21 f1(2,14,3) -> 5,12* 100.11/26.21 f1(1,1,16) -> 5,12* 100.11/26.21 f1(1,16,14) -> 5,12* 100.11/26.21 f1(14,3,4) -> 5,12* 100.11/26.21 f1(4,1,4) -> 12*,5,10 100.11/26.21 f1(2,16,3) -> 5,12* 100.11/26.21 f1(16,14,2) -> 5,12* 100.11/26.21 f1(4,3,4) -> 12*,5,10 100.11/26.21 f1(16,16,2) -> 5,12* 100.11/26.21 f1(3,14,1) -> 5,12* 100.11/26.21 f1(1,14,2) -> 5,12* 100.11/26.21 f1(2,1,14) -> 5,12* 100.11/26.21 f1(3,1,3) -> 12*,5,10 100.11/26.21 f1(3,16,1) -> 5,12* 100.11/26.21 f1(1,16,2) -> 5,12* 100.11/26.21 f1(2,3,14) -> 5,12* 100.11/26.21 f1(3,3,3) -> 12*,5,10 100.11/26.21 f1(14,1,1) -> 5,12* 100.11/26.21 f1(14,3,1) -> 5,12* 100.11/26.21 f1(4,1,1) -> 12*,5,10 100.11/26.21 f1(2,1,2) -> 12*,5,10 100.11/26.21 f1(4,3,1) -> 12*,5,10 100.11/26.21 f1(2,3,2) -> 12*,5,10 100.11/26.21 f1(14,2,3) -> 5,12* 100.11/26.21 f1(3,2,14) -> 5,12* 100.11/26.21 f1(14,4,3) -> 5,12* 100.11/26.21 f1(4,2,3) -> 12*,5,10 100.11/26.21 f1(3,4,14) -> 5,12* 100.11/26.21 f1(4,4,3) -> 12*,5,10 100.11/26.21 ok1(5) -> 5,12* 100.11/26.21 ok1(12) -> 5,12* 100.11/26.21 problem: 100.11/26.21 strict: 100.11/26.21 100.11/26.21 weak: 100.11/26.21 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.11/26.21 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.11/26.21 active(b()) -> mark(a()) 100.11/26.21 top(mark(X)) -> top(proper(X)) 100.11/26.21 proper(a()) -> ok(a()) 100.11/26.21 proper(b()) -> ok(b()) 100.11/26.21 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.11/26.21 top(ok(X)) -> top(active(X)) 100.11/26.21 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.11/26.21 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.11/26.21 Qed 100.11/26.21 100.11/26.21 strict: 100.11/26.21 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.11/26.21 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.11/26.21 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.11/26.21 weak: 100.11/26.21 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.11/26.21 active(b()) -> mark(a()) 100.11/26.21 top(mark(X)) -> top(proper(X)) 100.11/26.21 proper(a()) -> ok(a()) 100.11/26.21 proper(b()) -> ok(b()) 100.11/26.21 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.11/26.21 top(ok(X)) -> top(active(X)) 100.11/26.21 Matrix Interpretation Processor: dim=4 100.11/26.21 100.11/26.21 max_matrix: 100.11/26.21 [1 1 1 0] 100.11/26.21 [0 0 1 0] 100.11/26.21 [0 0 0 0] 100.11/26.21 [0 0 0 0] 100.11/26.21 interpretation: 100.11/26.21 [1 0 0 0] [1] 100.11/26.21 [0 0 1 0] [0] 100.11/26.21 [top](x0) = [0 0 0 0]x0 + [1] 100.11/26.21 [0 0 0 0] [0], 100.11/26.21 100.11/26.21 [1 1 0 0] 100.11/26.21 [0 0 1 0] 100.11/26.21 [ok](x0) = [0 0 0 0]x0 100.11/26.21 [0 0 0 0] , 100.11/26.21 100.11/26.21 [1 0 0 0] 100.11/26.21 [0 0 1 0] 100.11/26.21 [proper](x0) = [0 0 0 0]x0 100.11/26.21 [0 0 0 0] , 100.11/26.21 100.11/26.21 [1 0 0 0] 100.11/26.21 [0 0 0 0] 100.11/26.21 [mark](x0) = [0 0 0 0]x0 100.11/26.21 [0 0 0 0] , 100.11/26.21 100.11/26.21 [0] 100.11/26.21 [0] 100.11/26.21 [b] = [0] 100.11/26.21 [0], 100.11/26.21 100.11/26.21 [1 0 0 0] [0] 100.11/26.21 [0 0 1 0] [0] 100.11/26.21 [active](x0) = [0 0 0 0]x0 + [0] 100.11/26.21 [0 0 0 0] [1], 100.11/26.21 100.11/26.21 [1 1 1 0] [1 0 0 0] [1 1 1 0] 100.11/26.21 [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.21 [f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] , 100.11/26.22 100.11/26.22 [0] 100.11/26.22 [0] 100.11/26.22 [a] = [1] 100.11/26.22 [0] 100.11/26.22 orientation: 100.11/26.22 [2 1 1 0] [1] [1 1 1 0] 100.11/26.22 [0 0 0 0] [0] [0 0 0 0] 100.11/26.22 active(f(a(),X,X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X = mark(f(X,b(),b())) 100.11/26.22 [0 0 0 0] [1] [0 0 0 0] 100.11/26.22 100.11/26.22 [0] [0] 100.11/26.22 [0] [0] 100.11/26.22 active(b()) = [0] >= [0] = mark(a()) 100.11/26.22 [1] [0] 100.11/26.22 100.11/26.22 [1 0 0 0] [1] [1 0 0 0] [1] 100.11/26.22 [0 0 0 0] [0] [0 0 0 0] [0] 100.11/26.22 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 100.11/26.22 [0 0 0 0] [0] [0 0 0 0] [0] 100.11/26.22 100.11/26.22 [0] [0] 100.11/26.22 [1] [1] 100.11/26.22 proper(a()) = [0] >= [0] = ok(a()) 100.11/26.22 [0] [0] 100.11/26.22 100.11/26.22 [0] [0] 100.11/26.22 [0] [0] 100.11/26.22 proper(b()) = [0] >= [0] = ok(b()) 100.11/26.22 [0] [0] 100.11/26.22 100.11/26.22 [1 1 1 0] [1 1 0 0] [1 1 1 0] [1 1 1 0] [1 0 0 0] [1 1 1 0] 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.22 f(ok(X1),ok(X2),ok(X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = ok(f(X1,X2,X3)) 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.22 100.11/26.22 [1 1 0 0] [1] [1 0 0 0] [1] 100.11/26.22 [0 0 0 0] [0] [0 0 0 0] [0] 100.11/26.22 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 100.11/26.22 [0 0 0 0] [0] [0 0 0 0] [0] 100.11/26.22 100.11/26.22 [1 1 1 0] [1 0 0 0] [1 1 1 0] [0] [1 1 1 0] [1 0 0 0] [1 1 1 0] 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.22 active(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = f(X1,active(X2),X3) 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.22 100.11/26.22 [1 1 1 0] [1 0 0 0] [1 1 1 0] [1 1 1 0] [1 0 0 0] [1 1 1 0] 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.22 f(X1,mark(X2),X3) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = mark(f(X1,X2,X3)) 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.22 100.11/26.22 [1 1 1 0] [1 0 0 0] [1 1 1 0] [1 0 1 0] [1 0 0 0] [1 0 1 0] 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.22 proper(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = f(proper(X1),proper(X2),proper(X3)) 100.11/26.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 100.11/26.22 problem: 100.11/26.22 strict: 100.11/26.22 100.11/26.22 weak: 100.11/26.22 active(f(a(),X,X)) -> mark(f(X,b(),b())) 100.11/26.22 active(b()) -> mark(a()) 100.11/26.22 top(mark(X)) -> top(proper(X)) 100.11/26.22 proper(a()) -> ok(a()) 100.11/26.22 proper(b()) -> ok(b()) 100.11/26.22 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) 100.11/26.22 top(ok(X)) -> top(active(X)) 100.11/26.22 active(f(X1,X2,X3)) -> f(X1,active(X2),X3) 100.11/26.22 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) 100.11/26.22 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) 100.11/26.22 Qed 100.11/26.23 EOF