YES(?,O(n^3)) 1162.64/296.14 YES(?,O(n^3)) 1162.64/296.15 1162.64/296.15 Problem: 1162.64/296.15 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.15 active(f(X)) -> f(active(X)) 1162.64/296.15 active(g(X)) -> g(active(X)) 1162.64/296.15 f(mark(X)) -> mark(f(X)) 1162.64/296.15 g(mark(X)) -> mark(g(X)) 1162.64/296.15 proper(f(X)) -> f(proper(X)) 1162.64/296.15 proper(a()) -> ok(a()) 1162.64/296.15 proper(c(X)) -> c(proper(X)) 1162.64/296.15 proper(g(X)) -> g(proper(X)) 1162.64/296.15 f(ok(X)) -> ok(f(X)) 1162.64/296.15 c(ok(X)) -> ok(c(X)) 1162.64/296.15 g(ok(X)) -> ok(g(X)) 1162.64/296.15 top(mark(X)) -> top(proper(X)) 1162.64/296.15 top(ok(X)) -> top(active(X)) 1162.64/296.15 1162.64/296.15 Proof: 1162.64/296.15 Complexity Transformation Processor: 1162.64/296.15 strict: 1162.64/296.15 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.15 active(f(X)) -> f(active(X)) 1162.64/296.15 active(g(X)) -> g(active(X)) 1162.64/296.15 f(mark(X)) -> mark(f(X)) 1162.64/296.15 g(mark(X)) -> mark(g(X)) 1162.64/296.15 proper(f(X)) -> f(proper(X)) 1162.64/296.15 proper(a()) -> ok(a()) 1162.64/296.15 proper(c(X)) -> c(proper(X)) 1162.64/296.15 proper(g(X)) -> g(proper(X)) 1162.64/296.15 f(ok(X)) -> ok(f(X)) 1162.64/296.15 c(ok(X)) -> ok(c(X)) 1162.64/296.15 g(ok(X)) -> ok(g(X)) 1162.64/296.15 top(mark(X)) -> top(proper(X)) 1162.64/296.15 top(ok(X)) -> top(active(X)) 1162.64/296.15 weak: 1162.64/296.15 1162.64/296.15 Matrix Interpretation Processor: dim=1 1162.64/296.15 1162.64/296.15 max_matrix: 1162.64/296.15 1 1162.64/296.15 interpretation: 1162.64/296.15 [top](x0) = x0 + 14, 1162.64/296.15 1162.64/296.15 [ok](x0) = x0 + 9, 1162.64/296.15 1162.64/296.15 [proper](x0) = x0 + 10, 1162.64/296.15 1162.64/296.15 [mark](x0) = x0, 1162.64/296.15 1162.64/296.15 [c](x0) = x0, 1162.64/296.15 1162.64/296.15 [g](x0) = x0 + 8, 1162.64/296.15 1162.64/296.15 [active](x0) = x0 + 2, 1162.64/296.15 1162.64/296.15 [f](x0) = x0 + 6, 1162.64/296.15 1162.64/296.15 [a] = 2 1162.64/296.15 orientation: 1162.64/296.15 active(f(f(a()))) = 16 >= 22 = mark(c(f(g(f(a()))))) 1162.64/296.15 1162.64/296.15 active(f(X)) = X + 8 >= X + 8 = f(active(X)) 1162.64/296.15 1162.64/296.15 active(g(X)) = X + 10 >= X + 10 = g(active(X)) 1162.64/296.15 1162.64/296.15 f(mark(X)) = X + 6 >= X + 6 = mark(f(X)) 1162.64/296.15 1162.64/296.15 g(mark(X)) = X + 8 >= X + 8 = mark(g(X)) 1162.64/296.15 1162.64/296.15 proper(f(X)) = X + 16 >= X + 16 = f(proper(X)) 1162.64/296.15 1162.64/296.15 proper(a()) = 12 >= 11 = ok(a()) 1162.64/296.15 1162.64/296.15 proper(c(X)) = X + 10 >= X + 10 = c(proper(X)) 1162.64/296.15 1162.64/296.15 proper(g(X)) = X + 18 >= X + 18 = g(proper(X)) 1162.64/296.15 1162.64/296.15 f(ok(X)) = X + 15 >= X + 15 = ok(f(X)) 1162.64/296.15 1162.64/296.15 c(ok(X)) = X + 9 >= X + 9 = ok(c(X)) 1162.64/296.15 1162.64/296.15 g(ok(X)) = X + 17 >= X + 17 = ok(g(X)) 1162.64/296.15 1162.64/296.15 top(mark(X)) = X + 14 >= X + 24 = top(proper(X)) 1162.64/296.15 1162.64/296.15 top(ok(X)) = X + 23 >= X + 16 = top(active(X)) 1162.64/296.15 problem: 1162.64/296.15 strict: 1162.64/296.15 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.15 active(f(X)) -> f(active(X)) 1162.64/296.15 active(g(X)) -> g(active(X)) 1162.64/296.15 f(mark(X)) -> mark(f(X)) 1162.64/296.15 g(mark(X)) -> mark(g(X)) 1162.64/296.15 proper(f(X)) -> f(proper(X)) 1162.64/296.15 proper(c(X)) -> c(proper(X)) 1162.64/296.15 proper(g(X)) -> g(proper(X)) 1162.64/296.15 f(ok(X)) -> ok(f(X)) 1162.64/296.15 c(ok(X)) -> ok(c(X)) 1162.64/296.15 g(ok(X)) -> ok(g(X)) 1162.64/296.15 top(mark(X)) -> top(proper(X)) 1162.64/296.15 weak: 1162.64/296.15 proper(a()) -> ok(a()) 1162.64/296.15 top(ok(X)) -> top(active(X)) 1162.64/296.15 Matrix Interpretation Processor: dim=1 1162.64/296.15 1162.64/296.15 max_matrix: 1162.64/296.15 1 1162.64/296.15 interpretation: 1162.64/296.15 [top](x0) = x0 + 24, 1162.64/296.15 1162.64/296.15 [ok](x0) = x0 + 8, 1162.64/296.15 1162.64/296.15 [proper](x0) = x0 + 8, 1162.64/296.15 1162.64/296.15 [mark](x0) = x0 + 33, 1162.64/296.15 1162.64/296.15 [c](x0) = x0 + 77, 1162.64/296.15 1162.64/296.15 [g](x0) = x0 + 96, 1162.64/296.15 1162.64/296.15 [active](x0) = x0 + 8, 1162.64/296.15 1162.64/296.15 [f](x0) = x0 + 49, 1162.64/296.15 1162.64/296.15 [a] = 22 1162.64/296.15 orientation: 1162.64/296.15 active(f(f(a()))) = 128 >= 326 = mark(c(f(g(f(a()))))) 1162.64/296.15 1162.64/296.15 active(f(X)) = X + 57 >= X + 57 = f(active(X)) 1162.64/296.15 1162.64/296.15 active(g(X)) = X + 104 >= X + 104 = g(active(X)) 1162.64/296.15 1162.64/296.15 f(mark(X)) = X + 82 >= X + 82 = mark(f(X)) 1162.64/296.15 1162.64/296.15 g(mark(X)) = X + 129 >= X + 129 = mark(g(X)) 1162.64/296.15 1162.64/296.15 proper(f(X)) = X + 57 >= X + 57 = f(proper(X)) 1162.64/296.15 1162.64/296.15 proper(c(X)) = X + 85 >= X + 85 = c(proper(X)) 1162.64/296.15 1162.64/296.15 proper(g(X)) = X + 104 >= X + 104 = g(proper(X)) 1162.64/296.15 1162.64/296.15 f(ok(X)) = X + 57 >= X + 57 = ok(f(X)) 1162.64/296.15 1162.64/296.15 c(ok(X)) = X + 85 >= X + 85 = ok(c(X)) 1162.64/296.15 1162.64/296.15 g(ok(X)) = X + 104 >= X + 104 = ok(g(X)) 1162.64/296.15 1162.64/296.15 top(mark(X)) = X + 57 >= X + 32 = top(proper(X)) 1162.64/296.15 1162.64/296.15 proper(a()) = 30 >= 30 = ok(a()) 1162.64/296.15 1162.64/296.15 top(ok(X)) = X + 32 >= X + 32 = top(active(X)) 1162.64/296.15 problem: 1162.64/296.15 strict: 1162.64/296.15 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.15 active(f(X)) -> f(active(X)) 1162.64/296.15 active(g(X)) -> g(active(X)) 1162.64/296.15 f(mark(X)) -> mark(f(X)) 1162.64/296.15 g(mark(X)) -> mark(g(X)) 1162.64/296.15 proper(f(X)) -> f(proper(X)) 1162.64/296.15 proper(c(X)) -> c(proper(X)) 1162.64/296.15 proper(g(X)) -> g(proper(X)) 1162.64/296.15 f(ok(X)) -> ok(f(X)) 1162.64/296.15 c(ok(X)) -> ok(c(X)) 1162.64/296.15 g(ok(X)) -> ok(g(X)) 1162.64/296.15 weak: 1162.64/296.15 top(mark(X)) -> top(proper(X)) 1162.64/296.15 proper(a()) -> ok(a()) 1162.64/296.15 top(ok(X)) -> top(active(X)) 1162.64/296.15 Splitting Processor: 1162.64/296.15 strict: 1162.64/296.15 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.15 weak: 1162.64/296.15 top(mark(X)) -> top(proper(X)) 1162.64/296.15 proper(a()) -> ok(a()) 1162.64/296.15 top(ok(X)) -> top(active(X)) 1162.64/296.15 active(f(X)) -> f(active(X)) 1162.64/296.15 active(g(X)) -> g(active(X)) 1162.64/296.15 f(mark(X)) -> mark(f(X)) 1162.64/296.15 g(mark(X)) -> mark(g(X)) 1162.64/296.15 proper(f(X)) -> f(proper(X)) 1162.64/296.15 proper(c(X)) -> c(proper(X)) 1162.64/296.15 proper(g(X)) -> g(proper(X)) 1162.64/296.15 f(ok(X)) -> ok(f(X)) 1162.64/296.15 c(ok(X)) -> ok(c(X)) 1162.64/296.15 g(ok(X)) -> ok(g(X)) 1162.64/296.15 Splitting Processor: 1162.64/296.15 strict: 1162.64/296.15 f(mark(X)) -> mark(f(X)) 1162.64/296.15 weak: 1162.64/296.15 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.15 top(mark(X)) -> top(proper(X)) 1162.64/296.15 proper(a()) -> ok(a()) 1162.64/296.15 top(ok(X)) -> top(active(X)) 1162.64/296.15 active(f(X)) -> f(active(X)) 1162.64/296.15 active(g(X)) -> g(active(X)) 1162.64/296.15 g(mark(X)) -> mark(g(X)) 1162.64/296.15 proper(f(X)) -> f(proper(X)) 1162.64/296.15 proper(c(X)) -> c(proper(X)) 1162.64/296.15 proper(g(X)) -> g(proper(X)) 1162.64/296.15 f(ok(X)) -> ok(f(X)) 1162.64/296.15 c(ok(X)) -> ok(c(X)) 1162.64/296.15 g(ok(X)) -> ok(g(X)) 1162.64/296.15 Matrix Interpretation Processor: dim=3 1162.64/296.15 1162.64/296.15 max_matrix: 1162.64/296.15 [1 1 1] 1162.64/296.15 [0 0 1] 1162.64/296.15 [0 0 1] 1162.64/296.15 interpretation: 1162.64/296.15 [1 0 1] [0] 1162.64/296.15 [top](x0) = [0 0 1]x0 + [1] 1162.64/296.15 [0 0 0] [0], 1162.64/296.15 1162.64/296.15 [1 1 0] 1162.64/296.15 [ok](x0) = [0 0 0]x0 1162.64/296.15 [0 0 1] , 1162.64/296.15 1162.64/296.15 [1 0 0] [1] 1162.64/296.15 [proper](x0) = [0 0 0]x0 + [0] 1162.64/296.15 [0 0 1] [0], 1162.64/296.15 1162.64/296.15 [1 0 0] [0] 1162.64/296.15 [mark](x0) = [0 0 0]x0 + [0] 1162.64/296.15 [0 0 1] [1], 1162.64/296.15 1162.64/296.15 [1 1 0] 1162.64/296.15 [c](x0) = [0 0 0]x0 1162.64/296.15 [0 0 0] , 1162.64/296.15 1162.64/296.15 [1 0 0] 1162.64/296.15 [g](x0) = [0 0 0]x0 1162.64/296.15 [0 0 1] , 1162.64/296.15 1162.64/296.15 [1 0 0] 1162.64/296.15 [active](x0) = [0 0 0]x0 1162.64/296.15 [0 0 1] , 1162.64/296.15 1162.64/296.15 [1 0 1] [0] 1162.64/296.15 [f](x0) = [0 0 0]x0 + [0] 1162.64/296.15 [0 0 1] [1], 1162.64/296.15 1162.64/296.15 [1] 1162.64/296.15 [a] = [1] 1162.64/296.15 [0] 1162.64/296.15 orientation: 1162.64/296.15 [1 0 1] [1] [1 0 1] [0] 1162.64/296.15 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(f(X)) 1162.64/296.15 [0 0 1] [2] [0 0 1] [2] 1162.64/296.15 1162.64/296.15 [2] [2] 1162.64/296.15 active(f(f(a()))) = [0] >= [0] = mark(c(f(g(f(a()))))) 1162.64/296.15 [2] [1] 1162.64/296.15 1162.64/296.15 [1 0 1] [1] [1 0 1] [1] 1162.64/296.15 top(mark(X)) = [0 0 1]X + [2] >= [0 0 1]X + [1] = top(proper(X)) 1162.64/296.15 [0 0 0] [0] [0 0 0] [0] 1162.64/296.15 1162.64/296.15 [2] [2] 1162.64/296.15 proper(a()) = [0] >= [0] = ok(a()) 1162.64/296.15 [0] [0] 1162.64/296.15 1162.64/296.15 [1 1 1] [0] [1 0 1] [0] 1162.64/296.15 top(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = top(active(X)) 1162.64/296.15 [0 0 0] [0] [0 0 0] [0] 1162.64/296.15 1162.64/296.15 [1 0 1] [0] [1 0 1] [0] 1162.64/296.15 active(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(active(X)) 1162.64/296.15 [0 0 1] [1] [0 0 1] [1] 1162.64/296.15 1162.64/296.15 [1 0 0] [1 0 0] 1162.64/296.15 active(g(X)) = [0 0 0]X >= [0 0 0]X = g(active(X)) 1162.64/296.15 [0 0 1] [0 0 1] 1162.64/296.15 1162.64/296.15 [1 0 0] [0] [1 0 0] [0] 1162.64/296.15 g(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(g(X)) 1162.64/296.15 [0 0 1] [1] [0 0 1] [1] 1162.64/296.15 1162.64/296.15 [1 0 1] [1] [1 0 1] [1] 1162.64/296.15 proper(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(proper(X)) 1162.64/296.15 [0 0 1] [1] [0 0 1] [1] 1162.64/296.15 1162.64/296.15 [1 1 0] [1] [1 0 0] [1] 1162.64/296.15 proper(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(proper(X)) 1162.64/296.16 [0 0 0] [0] [0 0 0] [0] 1162.64/296.16 1162.64/296.16 [1 0 0] [1] [1 0 0] [1] 1162.64/296.16 proper(g(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = g(proper(X)) 1162.64/296.16 [0 0 1] [0] [0 0 1] [0] 1162.64/296.16 1162.64/296.16 [1 1 1] [0] [1 0 1] [0] 1162.64/296.16 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 1162.64/296.16 [0 0 1] [1] [0 0 1] [1] 1162.64/296.16 1162.64/296.16 [1 1 0] [1 1 0] 1162.64/296.16 c(ok(X)) = [0 0 0]X >= [0 0 0]X = ok(c(X)) 1162.64/296.16 [0 0 0] [0 0 0] 1162.64/296.16 1162.64/296.16 [1 1 0] [1 0 0] 1162.64/296.16 g(ok(X)) = [0 0 0]X >= [0 0 0]X = ok(g(X)) 1162.64/296.16 [0 0 1] [0 0 1] 1162.64/296.16 problem: 1162.64/296.16 strict: 1162.64/296.16 1162.64/296.16 weak: 1162.64/296.16 f(mark(X)) -> mark(f(X)) 1162.64/296.16 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.16 top(mark(X)) -> top(proper(X)) 1162.64/296.16 proper(a()) -> ok(a()) 1162.64/296.16 top(ok(X)) -> top(active(X)) 1162.64/296.16 active(f(X)) -> f(active(X)) 1162.64/296.16 active(g(X)) -> g(active(X)) 1162.64/296.16 g(mark(X)) -> mark(g(X)) 1162.64/296.16 proper(f(X)) -> f(proper(X)) 1162.64/296.16 proper(c(X)) -> c(proper(X)) 1162.64/296.16 proper(g(X)) -> g(proper(X)) 1162.64/296.16 f(ok(X)) -> ok(f(X)) 1162.64/296.16 c(ok(X)) -> ok(c(X)) 1162.64/296.16 g(ok(X)) -> ok(g(X)) 1162.64/296.16 Qed 1162.64/296.16 1162.64/296.16 strict: 1162.64/296.16 active(f(X)) -> f(active(X)) 1162.64/296.16 active(g(X)) -> g(active(X)) 1162.64/296.16 g(mark(X)) -> mark(g(X)) 1162.64/296.16 proper(f(X)) -> f(proper(X)) 1162.64/296.16 proper(c(X)) -> c(proper(X)) 1162.64/296.16 proper(g(X)) -> g(proper(X)) 1162.64/296.16 f(ok(X)) -> ok(f(X)) 1162.64/296.16 c(ok(X)) -> ok(c(X)) 1162.64/296.16 g(ok(X)) -> ok(g(X)) 1162.64/296.16 weak: 1162.64/296.16 f(mark(X)) -> mark(f(X)) 1162.64/296.16 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.16 top(mark(X)) -> top(proper(X)) 1162.64/296.16 proper(a()) -> ok(a()) 1162.64/296.16 top(ok(X)) -> top(active(X)) 1162.64/296.16 Matrix Interpretation Processor: dim=3 1162.64/296.16 1162.64/296.16 max_matrix: 1162.64/296.16 [1 1 1] 1162.64/296.16 [0 1 0] 1162.64/296.16 [0 0 1] 1162.64/296.16 interpretation: 1162.64/296.16 [1 0 0] [0] 1162.64/296.16 [top](x0) = [0 0 0]x0 + [0] 1162.64/296.16 [0 0 0] [1], 1162.64/296.16 1162.64/296.16 1162.64/296.16 [ok](x0) = x0 1162.64/296.16 , 1162.64/296.16 1162.64/296.16 [1 0 1] 1162.64/296.16 [proper](x0) = [0 1 0]x0 1162.64/296.16 [0 0 1] , 1162.64/296.16 1162.64/296.16 [1 0 1] 1162.64/296.16 [mark](x0) = [0 1 0]x0 1162.64/296.16 [0 0 0] , 1162.64/296.16 1162.64/296.16 [1 0 0] [0] 1162.64/296.16 [c](x0) = [0 0 0]x0 + [0] 1162.64/296.16 [0 0 1] [1], 1162.64/296.16 1162.64/296.16 [1 0 0] 1162.64/296.16 [g](x0) = [0 0 0]x0 1162.64/296.16 [0 0 1] , 1162.64/296.16 1162.64/296.16 [1 0 0] 1162.64/296.16 [active](x0) = [0 1 0]x0 1162.64/296.16 [0 0 0] , 1162.64/296.16 1162.64/296.16 [1 1 0] [0] 1162.64/296.16 [f](x0) = [0 1 0]x0 + [1] 1162.64/296.16 [0 0 1] [0], 1162.64/296.16 1162.64/296.16 [0] 1162.64/296.16 [a] = [1] 1162.64/296.16 [0] 1162.64/296.16 orientation: 1162.64/296.16 [1 1 0] [0] [1 1 0] [0] 1162.64/296.16 active(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(active(X)) 1162.64/296.16 [0 0 0] [0] [0 0 0] [0] 1162.64/296.16 1162.64/296.16 [1 0 0] [1 0 0] 1162.64/296.16 active(g(X)) = [0 0 0]X >= [0 0 0]X = g(active(X)) 1162.64/296.16 [0 0 0] [0 0 0] 1162.64/296.16 1162.64/296.16 [1 0 1] [1 0 1] 1162.64/296.16 g(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(g(X)) 1162.64/296.16 [0 0 0] [0 0 0] 1162.64/296.16 1162.64/296.16 [1 1 1] [0] [1 1 1] [0] 1162.64/296.16 proper(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(proper(X)) 1162.64/296.16 [0 0 1] [0] [0 0 1] [0] 1162.64/296.16 1162.64/296.16 [1 0 1] [1] [1 0 1] [0] 1162.64/296.16 proper(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(proper(X)) 1162.64/296.16 [0 0 1] [1] [0 0 1] [1] 1162.64/296.16 1162.64/296.16 [1 0 1] [1 0 1] 1162.64/296.16 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 1162.64/296.17 [0 0 1] [0 0 1] 1162.64/296.17 1162.64/296.17 [1 1 0] [0] [1 1 0] [0] 1162.64/296.17 f(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(f(X)) 1162.64/296.17 [0 0 1] [0] [0 0 1] [0] 1162.64/296.17 1162.64/296.17 [1 0 0] [0] [1 0 0] [0] 1162.64/296.17 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 1162.64/296.17 [0 0 1] [1] [0 0 1] [1] 1162.64/296.17 1162.64/296.17 [1 0 0] [1 0 0] 1162.64/296.17 g(ok(X)) = [0 0 0]X >= [0 0 0]X = ok(g(X)) 1162.64/296.17 [0 0 1] [0 0 1] 1162.64/296.17 1162.64/296.17 [1 1 1] [0] [1 1 1] [0] 1162.64/296.17 f(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(f(X)) 1162.64/296.17 [0 0 0] [0] [0 0 0] [0] 1162.64/296.17 1162.64/296.17 [3] [2] 1162.64/296.17 active(f(f(a()))) = [3] >= [0] = mark(c(f(g(f(a()))))) 1162.64/296.17 [0] [0] 1162.64/296.17 1162.64/296.17 [1 0 1] [0] [1 0 1] [0] 1162.64/296.17 top(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(proper(X)) 1162.64/296.17 [0 0 0] [1] [0 0 0] [1] 1162.64/296.17 1162.64/296.17 [0] [0] 1162.64/296.17 proper(a()) = [1] >= [1] = ok(a()) 1162.64/296.17 [0] [0] 1162.64/296.17 1162.64/296.17 [1 0 0] [0] [1 0 0] [0] 1162.64/296.17 top(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(active(X)) 1162.64/296.17 [0 0 0] [1] [0 0 0] [1] 1162.64/296.17 problem: 1162.64/296.17 strict: 1162.64/296.17 active(f(X)) -> f(active(X)) 1162.64/296.17 active(g(X)) -> g(active(X)) 1162.64/296.17 g(mark(X)) -> mark(g(X)) 1162.64/296.17 proper(f(X)) -> f(proper(X)) 1162.64/296.17 proper(g(X)) -> g(proper(X)) 1162.64/296.17 f(ok(X)) -> ok(f(X)) 1162.64/296.17 c(ok(X)) -> ok(c(X)) 1162.64/296.17 g(ok(X)) -> ok(g(X)) 1162.64/296.17 weak: 1162.64/296.17 proper(c(X)) -> c(proper(X)) 1162.64/296.17 f(mark(X)) -> mark(f(X)) 1162.64/296.17 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.17 top(mark(X)) -> top(proper(X)) 1162.64/296.17 proper(a()) -> ok(a()) 1162.64/296.17 top(ok(X)) -> top(active(X)) 1162.64/296.17 Matrix Interpretation Processor: dim=4 1162.64/296.17 1162.64/296.17 max_matrix: 1162.64/296.17 [1 1 0 1] 1162.64/296.17 [0 1 0 1] 1162.64/296.17 [0 0 0 1] 1162.64/296.17 [0 0 0 1] 1162.64/296.17 interpretation: 1162.64/296.17 [1 0 0 0] [0] 1162.64/296.17 [0 0 0 1] [0] 1162.64/296.17 [top](x0) = [0 0 0 1]x0 + [1] 1162.64/296.17 [0 0 0 0] [0], 1162.64/296.17 1162.64/296.17 [1 0 0 0] 1162.64/296.17 [0 1 0 0] 1162.64/296.17 [ok](x0) = [0 0 0 0]x0 1162.64/296.17 [0 0 0 1] , 1162.64/296.17 1162.64/296.17 [1 0 0 0] 1162.64/296.17 [0 1 0 0] 1162.64/296.17 [proper](x0) = [0 0 0 0]x0 1162.64/296.17 [0 0 0 1] , 1162.64/296.17 1162.64/296.17 [1 0 0 0] [0] 1162.64/296.17 [0 1 0 0] [1] 1162.64/296.17 [mark](x0) = [0 0 0 0]x0 + [0] 1162.64/296.17 [0 0 0 1] [0], 1162.64/296.17 1162.64/296.17 [1 0 0 0] [0] 1162.64/296.17 [0 0 0 0] [0] 1162.64/296.17 [c](x0) = [0 0 0 0]x0 + [0] 1162.64/296.17 [0 0 0 0] [1], 1162.64/296.17 1162.64/296.17 [1 1 0 0] [1] 1162.64/296.17 [0 1 0 0] [0] 1162.64/296.17 [g](x0) = [0 0 0 0]x0 + [0] 1162.64/296.17 [0 0 0 0] [0], 1162.64/296.17 1162.64/296.17 [1 0 0 0] 1162.64/296.17 [0 1 0 0] 1162.64/296.17 [active](x0) = [0 0 0 0]x0 1162.64/296.17 [0 0 0 1] , 1162.64/296.17 1162.64/296.17 [1 0 0 1] [0] 1162.64/296.17 [0 1 0 1] [0] 1162.64/296.17 [f](x0) = [0 0 0 0]x0 + [0] 1162.64/296.17 [0 0 0 0] [1], 1162.64/296.17 1162.64/296.17 [1] 1162.64/296.17 [0] 1162.64/296.17 [a] = [0] 1162.64/296.17 [0] 1162.64/296.17 orientation: 1162.64/296.17 [1 0 0 1] [0] [1 0 0 1] [0] 1162.64/296.17 [0 1 0 1] [0] [0 1 0 1] [0] 1162.64/296.17 active(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(active(X)) 1162.64/296.17 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.17 1162.64/296.17 [1 1 0 0] [1] [1 1 0 0] [1] 1162.64/296.17 [0 1 0 0] [0] [0 1 0 0] [0] 1162.64/296.17 active(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(active(X)) 1162.64/296.17 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.17 1162.64/296.17 [1 1 0 0] [2] [1 1 0 0] [1] 1162.64/296.17 [0 1 0 0] [1] [0 1 0 0] [1] 1162.64/296.17 g(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(g(X)) 1162.64/296.17 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.17 1162.64/296.17 [1 0 0 1] [0] [1 0 0 1] [0] 1162.64/296.17 [0 1 0 1] [0] [0 1 0 1] [0] 1162.64/296.17 proper(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(proper(X)) 1162.64/296.17 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.17 1162.64/296.17 [1 1 0 0] [1] [1 1 0 0] [1] 1162.64/296.17 [0 1 0 0] [0] [0 1 0 0] [0] 1162.64/296.17 proper(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(proper(X)) 1162.64/296.17 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.17 1162.64/296.17 [1 0 0 1] [0] [1 0 0 1] [0] 1162.64/296.17 [0 1 0 1] [0] [0 1 0 1] [0] 1162.64/296.17 f(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(f(X)) 1162.64/296.17 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.17 1162.64/296.17 [1 0 0 0] [0] [1 0 0 0] [0] 1162.64/296.17 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.17 c(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(c(X)) 1162.64/296.17 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.17 1162.64/296.17 [1 1 0 0] [1] [1 1 0 0] [1] 1162.64/296.17 [0 1 0 0] [0] [0 1 0 0] [0] 1162.64/296.17 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(g(X)) 1162.64/296.17 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.17 1162.64/296.17 [1 0 0 0] [0] [1 0 0 0] [0] 1162.64/296.17 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.17 proper(c(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = c(proper(X)) 1162.64/296.17 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.17 1162.64/296.17 [1 0 0 1] [0] [1 0 0 1] [0] 1162.64/296.17 [0 1 0 1] [1] [0 1 0 1] [1] 1162.64/296.17 f(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(f(X)) 1162.64/296.17 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.17 1162.64/296.17 [2] [2] 1162.64/296.17 [1] [1] 1162.64/296.17 active(f(f(a()))) = [0] >= [0] = mark(c(f(g(f(a()))))) 1162.64/296.17 [1] [1] 1162.64/296.17 1162.64/296.17 [1 0 0 0] [0] [1 0 0 0] [0] 1162.64/296.17 [0 0 0 1] [0] [0 0 0 1] [0] 1162.64/296.17 top(mark(X)) = [0 0 0 1]X + [1] >= [0 0 0 1]X + [1] = top(proper(X)) 1162.64/296.17 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.17 1162.64/296.17 [1] [1] 1162.64/296.17 [0] [0] 1162.64/296.17 proper(a()) = [0] >= [0] = ok(a()) 1162.64/296.17 [0] [0] 1162.64/296.17 1162.64/296.17 [1 0 0 0] [0] [1 0 0 0] [0] 1162.64/296.17 [0 0 0 1] [0] [0 0 0 1] [0] 1162.64/296.17 top(ok(X)) = [0 0 0 1]X + [1] >= [0 0 0 1]X + [1] = top(active(X)) 1162.64/296.17 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.17 problem: 1162.64/296.17 strict: 1162.64/296.17 active(f(X)) -> f(active(X)) 1162.64/296.17 active(g(X)) -> g(active(X)) 1162.64/296.17 proper(f(X)) -> f(proper(X)) 1162.64/296.17 proper(g(X)) -> g(proper(X)) 1162.64/296.17 f(ok(X)) -> ok(f(X)) 1162.64/296.17 c(ok(X)) -> ok(c(X)) 1162.64/296.17 g(ok(X)) -> ok(g(X)) 1162.64/296.17 weak: 1162.64/296.17 g(mark(X)) -> mark(g(X)) 1162.64/296.17 proper(c(X)) -> c(proper(X)) 1162.64/296.18 f(mark(X)) -> mark(f(X)) 1162.64/296.18 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.18 top(mark(X)) -> top(proper(X)) 1162.64/296.18 proper(a()) -> ok(a()) 1162.64/296.18 top(ok(X)) -> top(active(X)) 1162.64/296.18 Matrix Interpretation Processor: dim=4 1162.64/296.18 1162.64/296.18 max_matrix: 1162.64/296.18 [1 0 1 1] 1162.64/296.18 [0 0 0 1] 1162.64/296.18 [0 0 1 1] 1162.64/296.18 [0 0 0 1] 1162.64/296.18 interpretation: 1162.64/296.18 [1 0 0 0] 1162.64/296.18 [0 0 0 1] 1162.64/296.18 [top](x0) = [0 0 0 1]x0 1162.64/296.18 [0 0 0 0] , 1162.64/296.18 1162.64/296.18 [1 0 0 0] [0] 1162.64/296.18 [0 0 0 0] [0] 1162.64/296.18 [ok](x0) = [0 0 1 0]x0 + [1] 1162.64/296.18 [0 0 0 1] [0], 1162.64/296.18 1162.64/296.18 [1 0 1 0] [0] 1162.64/296.18 [0 0 0 1] [0] 1162.64/296.18 [proper](x0) = [0 0 1 0]x0 + [1] 1162.64/296.18 [0 0 0 1] [0], 1162.64/296.18 1162.64/296.18 [1 0 1 0] 1162.64/296.18 [0 0 0 0] 1162.64/296.18 [mark](x0) = [0 0 0 0]x0 1162.64/296.18 [0 0 0 1] , 1162.64/296.18 1162.64/296.18 [1 0 1 0] [0] 1162.64/296.18 [0 0 0 0] [0] 1162.64/296.18 [c](x0) = [0 0 1 0]x0 + [1] 1162.64/296.18 [0 0 0 0] [0], 1162.64/296.18 1162.64/296.18 [1 0 0 0] 1162.64/296.18 [0 0 0 0] 1162.64/296.18 [g](x0) = [0 0 1 0]x0 1162.64/296.18 [0 0 0 0] , 1162.64/296.18 1162.64/296.18 [1 0 0 0] 1162.64/296.18 [0 0 0 0] 1162.64/296.18 [active](x0) = [0 0 0 0]x0 1162.64/296.18 [0 0 0 1] , 1162.64/296.18 1162.64/296.18 [1 0 0 1] [0] 1162.64/296.18 [0 0 0 0] [0] 1162.64/296.18 [f](x0) = [0 0 1 0]x0 + [0] 1162.64/296.18 [0 0 0 0] [1], 1162.64/296.18 1162.64/296.18 [0] 1162.64/296.18 [0] 1162.64/296.18 [a] = [0] 1162.64/296.18 [0] 1162.64/296.18 orientation: 1162.64/296.18 [1 0 0 1] [0] [1 0 0 1] [0] 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 active(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(active(X)) 1162.64/296.18 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.18 1162.64/296.18 [1 0 0 0] [1 0 0 0] 1162.64/296.18 [0 0 0 0] [0 0 0 0] 1162.64/296.18 active(g(X)) = [0 0 0 0]X >= [0 0 0 0]X = g(active(X)) 1162.64/296.18 [0 0 0 0] [0 0 0 0] 1162.64/296.18 1162.64/296.18 [1 0 1 1] [0] [1 0 1 1] [0] 1162.64/296.18 [0 0 0 0] [1] [0 0 0 0] [0] 1162.64/296.18 proper(f(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = f(proper(X)) 1162.64/296.18 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.18 1162.64/296.18 [1 0 1 0] [0] [1 0 1 0] [0] 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 proper(g(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = g(proper(X)) 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 1162.64/296.18 [1 0 0 1] [0] [1 0 0 1] [0] 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 f(ok(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = ok(f(X)) 1162.64/296.18 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.18 1162.64/296.18 [1 0 1 0] [1] [1 0 1 0] [0] 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 c(ok(X)) = [0 0 1 0]X + [2] >= [0 0 1 0]X + [2] = ok(c(X)) 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 1162.64/296.18 [1 0 0 0] [0] [1 0 0 0] [0] 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 g(ok(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = ok(g(X)) 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 1162.64/296.18 [1 0 1 0] [1 0 1 0] 1162.64/296.18 [0 0 0 0] [0 0 0 0] 1162.64/296.18 g(mark(X)) = [0 0 0 0]X >= [0 0 0 0]X = mark(g(X)) 1162.64/296.18 [0 0 0 0] [0 0 0 0] 1162.64/296.18 1162.64/296.18 [1 0 2 0] [1] [1 0 2 0] [1] 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 proper(c(X)) = [0 0 1 0]X + [2] >= [0 0 1 0]X + [2] = c(proper(X)) 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 1162.64/296.18 [1 0 1 1] [0] [1 0 1 1] [0] 1162.64/296.18 [0 0 0 0] [0] [0 0 0 0] [0] 1162.64/296.18 f(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(f(X)) 1162.64/296.18 [0 0 0 0] [1] [0 0 0 0] [1] 1162.64/296.18 1162.64/296.18 [1] [1] 1162.64/296.18 [0] [0] 1162.64/296.18 active(f(f(a()))) = [0] >= [0] = mark(c(f(g(f(a()))))) 1162.64/296.18 [1] [0] 1162.64/296.18 1162.64/296.18 [1 0 1 0] [1 0 1 0] 1162.64/296.18 [0 0 0 1] [0 0 0 1] 1162.64/296.18 top(mark(X)) = [0 0 0 1]X >= [0 0 0 1]X = top(proper(X)) 1162.64/296.18 [0 0 0 0] [0 0 0 0] 1162.64/296.18 1162.64/296.18 [0] [0] 1162.64/296.18 [0] [0] 1162.64/296.18 proper(a()) = [1] >= [1] = ok(a()) 1162.64/296.18 [0] [0] 1162.64/296.18 1162.64/296.18 [1 0 0 0] [1 0 0 0] 1162.64/296.18 [0 0 0 1] [0 0 0 1] 1162.64/296.18 top(ok(X)) = [0 0 0 1]X >= [0 0 0 1]X = top(active(X)) 1162.64/296.18 [0 0 0 0] [0 0 0 0] 1162.64/296.18 problem: 1162.64/296.18 strict: 1162.64/296.18 active(f(X)) -> f(active(X)) 1162.64/296.18 active(g(X)) -> g(active(X)) 1162.64/296.18 proper(f(X)) -> f(proper(X)) 1162.64/296.18 proper(g(X)) -> g(proper(X)) 1162.64/296.18 f(ok(X)) -> ok(f(X)) 1162.64/296.18 g(ok(X)) -> ok(g(X)) 1162.64/296.18 weak: 1162.64/296.18 c(ok(X)) -> ok(c(X)) 1162.64/296.18 g(mark(X)) -> mark(g(X)) 1162.64/296.18 proper(c(X)) -> c(proper(X)) 1162.64/296.18 f(mark(X)) -> mark(f(X)) 1162.64/296.18 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.18 top(mark(X)) -> top(proper(X)) 1162.64/296.18 proper(a()) -> ok(a()) 1162.64/296.18 top(ok(X)) -> top(active(X)) 1162.64/296.18 Splitting Processor: 1162.64/296.18 strict: 1162.64/296.18 proper(g(X)) -> g(proper(X)) 1162.64/296.18 weak: 1162.64/296.18 c(ok(X)) -> ok(c(X)) 1162.64/296.18 g(mark(X)) -> mark(g(X)) 1162.64/296.18 proper(c(X)) -> c(proper(X)) 1162.64/296.18 f(mark(X)) -> mark(f(X)) 1162.64/296.18 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.18 top(mark(X)) -> top(proper(X)) 1162.64/296.18 proper(a()) -> ok(a()) 1162.64/296.18 top(ok(X)) -> top(active(X)) 1162.64/296.18 active(f(X)) -> f(active(X)) 1162.64/296.18 active(g(X)) -> g(active(X)) 1162.64/296.18 proper(f(X)) -> f(proper(X)) 1162.64/296.18 f(ok(X)) -> ok(f(X)) 1162.64/296.18 g(ok(X)) -> ok(g(X)) 1162.64/296.18 Splitting Processor: 1162.64/296.18 strict: 1162.64/296.18 proper(f(X)) -> f(proper(X)) 1162.64/296.18 weak: 1162.64/296.18 proper(g(X)) -> g(proper(X)) 1162.64/296.18 c(ok(X)) -> ok(c(X)) 1162.64/296.18 g(mark(X)) -> mark(g(X)) 1162.64/296.18 proper(c(X)) -> c(proper(X)) 1162.64/296.18 f(mark(X)) -> mark(f(X)) 1162.64/296.18 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.18 top(mark(X)) -> top(proper(X)) 1162.64/296.18 proper(a()) -> ok(a()) 1162.64/296.18 top(ok(X)) -> top(active(X)) 1162.64/296.18 active(f(X)) -> f(active(X)) 1162.64/296.18 active(g(X)) -> g(active(X)) 1162.64/296.18 f(ok(X)) -> ok(f(X)) 1162.64/296.18 g(ok(X)) -> ok(g(X)) 1162.64/296.18 Matrix Interpretation Processor: dim=3 1162.64/296.18 1162.64/296.18 max_matrix: 1162.64/296.18 [1 3 1] 1162.64/296.18 [0 1 0] 1162.64/296.18 [0 0 1] 1162.64/296.18 interpretation: 1162.64/296.18 [1 3 0] [0] 1162.64/296.18 [top](x0) = [0 0 0]x0 + [1] 1162.64/296.18 [0 0 0] [3], 1162.64/296.18 1162.64/296.18 [1 0 0] [3] 1162.64/296.18 [ok](x0) = [0 1 0]x0 + [0] 1162.64/296.18 [0 0 0] [0], 1162.64/296.18 1162.64/296.18 [1 0 1] [3] 1162.64/296.18 [proper](x0) = [0 1 0]x0 + [0] 1162.64/296.18 [0 0 1] [0], 1162.64/296.18 1162.64/296.18 [1 0 1] [0] 1162.64/296.19 [mark](x0) = [0 1 0]x0 + [1] 1162.64/296.19 [0 0 0] [0], 1162.64/296.19 1162.64/296.19 [1 0 0] 1162.64/296.19 [c](x0) = [0 0 0]x0 1162.64/296.19 [0 0 1] , 1162.64/296.19 1162.64/296.19 [1] 1162.64/296.19 [g](x0) = x0 + [0] 1162.64/296.19 [0], 1162.64/296.19 1162.64/296.19 [3] 1162.64/296.19 [active](x0) = x0 + [0] 1162.64/296.19 [2], 1162.64/296.19 1162.64/296.19 [1 1 0] [0] 1162.64/296.19 [f](x0) = [0 1 0]x0 + [0] 1162.64/296.19 [0 0 1] [1], 1162.64/296.19 1162.64/296.19 [1] 1162.64/296.19 [a] = [1] 1162.64/296.19 [0] 1162.64/296.19 orientation: 1162.64/296.19 [1 1 1] [4] [1 1 1] [3] 1162.64/296.19 proper(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(proper(X)) 1162.64/296.19 [0 0 1] [1] [0 0 1] [1] 1162.64/296.19 1162.64/296.19 [1 0 1] [4] [1 0 1] [4] 1162.64/296.19 proper(g(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = g(proper(X)) 1162.64/296.19 [0 0 1] [0] [0 0 1] [0] 1162.64/296.19 1162.64/296.19 [1 0 0] [3] [1 0 0] [3] 1162.64/296.19 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 1162.64/296.19 [0 0 0] [0] [0 0 0] [0] 1162.64/296.19 1162.64/296.19 [1 0 1] [1] [1 0 1] [1] 1162.64/296.19 g(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(g(X)) 1162.64/296.19 [0 0 0] [0] [0 0 0] [0] 1162.64/296.19 1162.64/296.19 [1 0 1] [3] [1 0 1] [3] 1162.64/296.19 proper(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(proper(X)) 1162.64/296.19 [0 0 1] [0] [0 0 1] [0] 1162.64/296.19 1162.64/296.19 [1 1 1] [1] [1 1 1] [1] 1162.64/296.19 f(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(f(X)) 1162.64/296.19 [0 0 0] [1] [0 0 0] [0] 1162.64/296.19 1162.64/296.19 [6] [6] 1162.64/296.19 active(f(f(a()))) = [1] >= [1] = mark(c(f(g(f(a()))))) 1162.64/296.19 [4] [0] 1162.64/296.19 1162.64/296.19 [1 3 1] [3] [1 3 1] [3] 1162.64/296.19 top(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(proper(X)) 1162.64/296.19 [0 0 0] [3] [0 0 0] [3] 1162.64/296.19 1162.64/296.19 [4] [4] 1162.64/296.19 proper(a()) = [1] >= [1] = ok(a()) 1162.64/296.19 [0] [0] 1162.64/296.19 1162.64/296.19 [1 3 0] [3] [1 3 0] [3] 1162.64/296.19 top(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(active(X)) 1162.64/296.19 [0 0 0] [3] [0 0 0] [3] 1162.64/296.19 1162.64/296.19 [1 1 0] [3] [1 1 0] [3] 1162.64/296.19 active(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(active(X)) 1162.64/296.19 [0 0 1] [3] [0 0 1] [3] 1162.64/296.19 1162.64/296.19 [4] [4] 1162.64/296.19 active(g(X)) = X + [0] >= X + [0] = g(active(X)) 1162.64/296.19 [2] [2] 1162.64/296.19 1162.64/296.19 [1 1 0] [3] [1 1 0] [3] 1162.64/296.19 f(ok(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = ok(f(X)) 1162.64/296.19 [0 0 0] [1] [0 0 0] [0] 1162.64/296.19 1162.64/296.19 [1 0 0] [4] [1 0 0] [4] 1162.64/296.19 g(ok(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = ok(g(X)) 1162.64/296.19 [0 0 0] [0] [0 0 0] [0] 1162.64/296.19 problem: 1162.64/296.19 strict: 1162.64/296.19 1162.64/296.19 weak: 1162.64/296.19 proper(f(X)) -> f(proper(X)) 1162.64/296.19 proper(g(X)) -> g(proper(X)) 1162.64/296.19 c(ok(X)) -> ok(c(X)) 1162.64/296.19 g(mark(X)) -> mark(g(X)) 1162.64/296.19 proper(c(X)) -> c(proper(X)) 1162.64/296.19 f(mark(X)) -> mark(f(X)) 1162.64/296.19 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.19 top(mark(X)) -> top(proper(X)) 1162.64/296.19 proper(a()) -> ok(a()) 1162.64/296.19 top(ok(X)) -> top(active(X)) 1162.64/296.19 active(f(X)) -> f(active(X)) 1162.64/296.19 active(g(X)) -> g(active(X)) 1162.64/296.19 f(ok(X)) -> ok(f(X)) 1162.64/296.19 g(ok(X)) -> ok(g(X)) 1162.64/296.19 Qed 1162.64/296.19 1162.64/296.19 strict: 1162.64/296.19 active(f(X)) -> f(active(X)) 1162.64/296.19 active(g(X)) -> g(active(X)) 1162.64/296.19 f(ok(X)) -> ok(f(X)) 1162.64/296.19 g(ok(X)) -> ok(g(X)) 1162.64/296.19 weak: 1162.64/296.19 proper(f(X)) -> f(proper(X)) 1162.64/296.19 proper(g(X)) -> g(proper(X)) 1162.64/296.19 c(ok(X)) -> ok(c(X)) 1162.64/296.19 g(mark(X)) -> mark(g(X)) 1162.64/296.19 proper(c(X)) -> c(proper(X)) 1162.64/296.19 f(mark(X)) -> mark(f(X)) 1162.64/296.19 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.19 top(mark(X)) -> top(proper(X)) 1162.64/296.19 proper(a()) -> ok(a()) 1162.64/296.19 top(ok(X)) -> top(active(X)) 1162.64/296.19 Splitting Processor: 1162.64/296.19 strict: 1162.64/296.19 f(ok(X)) -> ok(f(X)) 1162.64/296.19 weak: 1162.64/296.19 proper(f(X)) -> f(proper(X)) 1162.64/296.19 proper(g(X)) -> g(proper(X)) 1162.64/296.19 c(ok(X)) -> ok(c(X)) 1162.64/296.19 g(mark(X)) -> mark(g(X)) 1162.64/296.19 proper(c(X)) -> c(proper(X)) 1162.64/296.19 f(mark(X)) -> mark(f(X)) 1162.64/296.19 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.19 top(mark(X)) -> top(proper(X)) 1162.64/296.19 proper(a()) -> ok(a()) 1162.64/296.19 top(ok(X)) -> top(active(X)) 1162.64/296.19 active(f(X)) -> f(active(X)) 1162.64/296.19 active(g(X)) -> g(active(X)) 1162.64/296.19 g(ok(X)) -> ok(g(X)) 1162.64/296.19 Splitting Processor: 1162.64/296.19 strict: 1162.64/296.19 active(g(X)) -> g(active(X)) 1162.64/296.19 weak: 1162.64/296.19 f(ok(X)) -> ok(f(X)) 1162.64/296.19 proper(f(X)) -> f(proper(X)) 1162.64/296.19 proper(g(X)) -> g(proper(X)) 1162.64/296.19 c(ok(X)) -> ok(c(X)) 1162.64/296.19 g(mark(X)) -> mark(g(X)) 1162.64/296.19 proper(c(X)) -> c(proper(X)) 1162.64/296.19 f(mark(X)) -> mark(f(X)) 1162.64/296.19 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.64/296.19 top(mark(X)) -> top(proper(X)) 1162.64/296.19 proper(a()) -> ok(a()) 1162.64/296.19 top(ok(X)) -> top(active(X)) 1162.64/296.19 active(f(X)) -> f(active(X)) 1162.64/296.19 g(ok(X)) -> ok(g(X)) 1162.64/296.19 Matrix Interpretation Processor: dim=3 1162.64/296.19 1162.64/296.19 max_matrix: 1162.64/296.19 [1 3 1] 1162.64/296.19 [0 1 1] 1162.64/296.19 [0 0 1] 1162.64/296.19 interpretation: 1162.64/296.19 [1 3 0] [0] 1162.64/296.19 [top](x0) = [0 0 0]x0 + [1] 1162.64/296.19 [0 0 0] [1], 1162.64/296.19 1162.64/296.19 [1 0 1] [0] 1162.64/296.19 [ok](x0) = [0 1 0]x0 + [1] 1162.64/296.19 [0 0 1] [1], 1162.64/296.19 1162.64/296.19 [1 0 1] [0] 1162.64/296.19 [proper](x0) = [0 1 0]x0 + [1] 1162.64/296.19 [0 0 1] [1], 1162.64/296.19 1162.64/296.19 [1 0 1] [0] 1162.64/296.19 [mark](x0) = [0 1 0]x0 + [1] 1162.64/296.19 [0 0 0] [0], 1162.64/296.19 1162.64/296.19 [1 0 0] 1162.64/296.19 [c](x0) = [0 0 1]x0 1162.64/296.19 [0 0 1] , 1162.64/296.19 1162.64/296.19 [1 1 0] [0] 1162.64/296.19 [g](x0) = [0 1 0]x0 + [0] 1162.64/296.19 [0 0 1] [1], 1162.64/296.19 1162.64/296.19 [1 0 1] [3] 1162.64/296.19 [active](x0) = [0 1 0]x0 + [0] 1162.64/296.19 [0 0 1] [0], 1162.64/296.19 1162.64/296.19 [1] 1162.64/296.19 [f](x0) = x0 + [0] 1162.64/296.19 [0], 1162.64/296.19 1162.64/296.19 [0] 1162.64/296.19 [a] = [2] 1162.64/296.19 [0] 1162.64/296.19 orientation: 1162.64/296.19 [1 1 1] [4] [1 1 1] [3] 1162.64/296.19 active(g(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = g(active(X)) 1162.64/296.19 [0 0 1] [1] [0 0 1] [1] 1162.64/296.19 1162.64/296.19 [1 0 1] [1] [1 0 1] [1] 1162.64/296.19 f(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(f(X)) 1162.74/296.20 [0 0 1] [1] [0 0 1] [1] 1162.74/296.20 1162.74/296.20 [1 0 1] [1] [1 0 1] [1] 1162.74/296.20 proper(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(proper(X)) 1162.74/296.20 [0 0 1] [1] [0 0 1] [1] 1162.74/296.20 1162.74/296.20 [1 1 1] [1] [1 1 1] [1] 1162.74/296.20 proper(g(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = g(proper(X)) 1162.74/296.20 [0 0 1] [2] [0 0 1] [2] 1162.74/296.20 1162.74/296.20 [1 0 1] [0] [1 0 1] [0] 1162.74/296.20 c(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = ok(c(X)) 1162.74/296.20 [0 0 1] [1] [0 0 1] [1] 1162.74/296.20 1162.74/296.20 [1 1 1] [1] [1 1 1] [1] 1162.74/296.20 g(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(g(X)) 1162.74/296.20 [0 0 0] [1] [0 0 0] [0] 1162.74/296.20 1162.74/296.20 [1 0 1] [0] [1 0 1] [0] 1162.74/296.20 proper(c(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = c(proper(X)) 1162.74/296.20 [0 0 1] [1] [0 0 1] [1] 1162.74/296.20 1162.74/296.20 [1 0 1] [1] [1 0 1] [1] 1162.74/296.20 f(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(f(X)) 1162.74/296.20 [0 0 0] [0] [0 0 0] [0] 1162.74/296.20 1162.74/296.20 [5] [5] 1162.74/296.20 active(f(f(a()))) = [2] >= [2] = mark(c(f(g(f(a()))))) 1162.74/296.20 [0] [0] 1162.74/296.20 1162.74/296.20 [1 3 1] [3] [1 3 1] [3] 1162.74/296.20 top(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(proper(X)) 1162.74/296.20 [0 0 0] [1] [0 0 0] [1] 1162.74/296.20 1162.74/296.20 [0] [0] 1162.74/296.20 proper(a()) = [3] >= [3] = ok(a()) 1162.74/296.20 [1] [1] 1162.74/296.20 1162.74/296.20 [1 3 1] [3] [1 3 1] [3] 1162.74/296.20 top(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(active(X)) 1162.74/296.20 [0 0 0] [1] [0 0 0] [1] 1162.74/296.20 1162.74/296.20 [1 0 1] [4] [1 0 1] [4] 1162.74/296.20 active(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(active(X)) 1162.74/296.20 [0 0 1] [0] [0 0 1] [0] 1162.74/296.20 1162.74/296.20 [1 1 1] [1] [1 1 1] [1] 1162.74/296.20 g(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 1162.74/296.20 [0 0 1] [2] [0 0 1] [2] 1162.74/296.20 problem: 1162.74/296.20 strict: 1162.74/296.20 1162.74/296.20 weak: 1162.74/296.20 active(g(X)) -> g(active(X)) 1162.74/296.20 f(ok(X)) -> ok(f(X)) 1162.74/296.20 proper(f(X)) -> f(proper(X)) 1162.74/296.20 proper(g(X)) -> g(proper(X)) 1162.74/296.20 c(ok(X)) -> ok(c(X)) 1162.74/296.20 g(mark(X)) -> mark(g(X)) 1162.74/296.20 proper(c(X)) -> c(proper(X)) 1162.74/296.20 f(mark(X)) -> mark(f(X)) 1162.74/296.20 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.20 top(mark(X)) -> top(proper(X)) 1162.74/296.20 proper(a()) -> ok(a()) 1162.74/296.20 top(ok(X)) -> top(active(X)) 1162.74/296.20 active(f(X)) -> f(active(X)) 1162.74/296.20 g(ok(X)) -> ok(g(X)) 1162.74/296.20 Qed 1162.74/296.20 1162.74/296.20 strict: 1162.74/296.20 active(f(X)) -> f(active(X)) 1162.74/296.20 g(ok(X)) -> ok(g(X)) 1162.74/296.20 weak: 1162.74/296.20 active(g(X)) -> g(active(X)) 1162.74/296.20 f(ok(X)) -> ok(f(X)) 1162.74/296.20 proper(f(X)) -> f(proper(X)) 1162.74/296.20 proper(g(X)) -> g(proper(X)) 1162.74/296.20 c(ok(X)) -> ok(c(X)) 1162.74/296.20 g(mark(X)) -> mark(g(X)) 1162.74/296.20 proper(c(X)) -> c(proper(X)) 1162.74/296.20 f(mark(X)) -> mark(f(X)) 1162.74/296.20 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.20 top(mark(X)) -> top(proper(X)) 1162.74/296.20 proper(a()) -> ok(a()) 1162.74/296.20 top(ok(X)) -> top(active(X)) 1162.74/296.20 Splitting Processor: 1162.74/296.20 strict: 1162.74/296.20 active(f(X)) -> f(active(X)) 1162.74/296.20 weak: 1162.74/296.20 active(g(X)) -> g(active(X)) 1162.74/296.20 f(ok(X)) -> ok(f(X)) 1162.74/296.20 proper(f(X)) -> f(proper(X)) 1162.74/296.20 proper(g(X)) -> g(proper(X)) 1162.74/296.20 c(ok(X)) -> ok(c(X)) 1162.74/296.20 g(mark(X)) -> mark(g(X)) 1162.74/296.20 proper(c(X)) -> c(proper(X)) 1162.74/296.20 f(mark(X)) -> mark(f(X)) 1162.74/296.20 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.20 top(mark(X)) -> top(proper(X)) 1162.74/296.20 proper(a()) -> ok(a()) 1162.74/296.20 top(ok(X)) -> top(active(X)) 1162.74/296.20 g(ok(X)) -> ok(g(X)) 1162.74/296.20 Matrix Interpretation Processor: dim=3 1162.74/296.20 1162.74/296.20 max_matrix: 1162.74/296.20 [1 3 2] 1162.74/296.20 [0 1 0] 1162.74/296.20 [0 0 1] 1162.74/296.20 interpretation: 1162.74/296.20 [1 3 2] [0] 1162.74/296.20 [top](x0) = [0 1 0]x0 + [2] 1162.74/296.20 [0 0 0] [0], 1162.74/296.20 1162.74/296.20 [1 0 1] [1] 1162.74/296.20 [ok](x0) = [0 1 0]x0 + [0] 1162.74/296.20 [0 0 1] [2], 1162.74/296.20 1162.74/296.20 [1 0 2] [1] 1162.74/296.20 [proper](x0) = [0 1 0]x0 + [0] 1162.74/296.20 [0 0 1] [2], 1162.74/296.20 1162.74/296.20 [1 0 2] [0] 1162.74/296.20 [mark](x0) = [0 1 0]x0 + [2] 1162.74/296.20 [0 0 1] [0], 1162.74/296.20 1162.74/296.20 [1 0 0] 1162.74/296.20 [c](x0) = [0 0 0]x0 1162.74/296.20 [0 0 1] , 1162.74/296.20 1162.74/296.20 [1 1 1] [0] 1162.74/296.20 [g](x0) = [0 1 0]x0 + [0] 1162.74/296.20 [0 0 1] [1], 1162.74/296.20 1162.74/296.20 [1 0 1] [3] 1162.74/296.20 [active](x0) = [0 1 0]x0 + [0] 1162.74/296.20 [0 0 1] [1], 1162.74/296.20 1162.74/296.20 [1 3 0] [0] 1162.74/296.20 [f](x0) = [0 1 0]x0 + [1] 1162.74/296.20 [0 0 1] [0], 1162.74/296.20 1162.74/296.20 [1] 1162.74/296.20 [a] = [0] 1162.74/296.20 [0] 1162.74/296.20 orientation: 1162.74/296.20 [1 1 2] [3] [1 1 2] [2] 1162.74/296.20 g(ok(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = ok(g(X)) 1162.74/296.20 [0 0 1] [3] [0 0 1] [3] 1162.74/296.20 1162.74/296.20 [1 3 1] [3] [1 3 1] [3] 1162.74/296.20 active(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(active(X)) 1162.74/296.20 [0 0 1] [1] [0 0 1] [1] 1162.74/296.20 1162.74/296.20 [1 1 2] [4] [1 1 2] [4] 1162.74/296.20 active(g(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = g(active(X)) 1162.74/296.20 [0 0 1] [2] [0 0 1] [2] 1162.74/296.20 1162.74/296.20 [1 3 1] [1] [1 3 1] [1] 1162.74/296.20 f(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(f(X)) 1162.74/296.20 [0 0 1] [2] [0 0 1] [2] 1162.74/296.20 1162.74/296.20 [1 3 2] [1] [1 3 2] [1] 1162.74/296.20 proper(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(proper(X)) 1162.74/296.20 [0 0 1] [2] [0 0 1] [2] 1162.74/296.20 1162.74/296.20 [1 1 3] [3] [1 1 3] [3] 1162.74/296.20 proper(g(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = g(proper(X)) 1162.74/296.20 [0 0 1] [3] [0 0 1] [3] 1162.74/296.20 1162.74/296.20 [1 0 1] [1] [1 0 1] [1] 1162.74/296.20 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 1162.74/296.20 [0 0 1] [2] [0 0 1] [2] 1162.74/296.20 1162.74/296.20 [1 1 3] [2] [1 1 3] [2] 1162.74/296.20 g(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = mark(g(X)) 1162.74/296.21 [0 0 1] [1] [0 0 1] [1] 1162.74/296.21 1162.74/296.21 [1 0 2] [1] [1 0 2] [1] 1162.74/296.21 proper(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(proper(X)) 1162.74/296.21 [0 0 1] [2] [0 0 1] [2] 1162.74/296.21 1162.74/296.21 [1 3 2] [6] [1 3 2] [0] 1162.74/296.21 f(mark(X)) = [0 1 0]X + [3] >= [0 1 0]X + [3] = mark(f(X)) 1162.74/296.21 [0 0 1] [0] [0 0 1] [0] 1162.74/296.21 1162.74/296.21 [7] [7] 1162.74/296.21 active(f(f(a()))) = [2] >= [2] = mark(c(f(g(f(a()))))) 1162.74/296.21 [1] [1] 1162.74/296.21 1162.74/296.21 [1 3 4] [6] [1 3 4] [5] 1162.74/296.21 top(mark(X)) = [0 1 0]X + [4] >= [0 1 0]X + [2] = top(proper(X)) 1162.74/296.21 [0 0 0] [0] [0 0 0] [0] 1162.74/296.21 1162.74/296.21 [2] [2] 1162.74/296.21 proper(a()) = [0] >= [0] = ok(a()) 1162.74/296.21 [2] [2] 1162.74/296.21 1162.74/296.21 [1 3 3] [5] [1 3 3] [5] 1162.74/296.21 top(ok(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = top(active(X)) 1162.74/296.21 [0 0 0] [0] [0 0 0] [0] 1162.74/296.21 problem: 1162.74/296.21 strict: 1162.74/296.21 1162.74/296.21 weak: 1162.74/296.21 g(ok(X)) -> ok(g(X)) 1162.74/296.21 active(f(X)) -> f(active(X)) 1162.74/296.21 active(g(X)) -> g(active(X)) 1162.74/296.21 f(ok(X)) -> ok(f(X)) 1162.74/296.21 proper(f(X)) -> f(proper(X)) 1162.74/296.21 proper(g(X)) -> g(proper(X)) 1162.74/296.21 c(ok(X)) -> ok(c(X)) 1162.74/296.21 g(mark(X)) -> mark(g(X)) 1162.74/296.21 proper(c(X)) -> c(proper(X)) 1162.74/296.21 f(mark(X)) -> mark(f(X)) 1162.74/296.21 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.21 top(mark(X)) -> top(proper(X)) 1162.74/296.21 proper(a()) -> ok(a()) 1162.74/296.21 top(ok(X)) -> top(active(X)) 1162.74/296.21 Qed 1162.74/296.21 1162.74/296.21 strict: 1162.74/296.21 g(ok(X)) -> ok(g(X)) 1162.74/296.21 weak: 1162.74/296.21 active(f(X)) -> f(active(X)) 1162.74/296.21 active(g(X)) -> g(active(X)) 1162.74/296.21 f(ok(X)) -> ok(f(X)) 1162.74/296.21 proper(f(X)) -> f(proper(X)) 1162.74/296.21 proper(g(X)) -> g(proper(X)) 1162.74/296.21 c(ok(X)) -> ok(c(X)) 1162.74/296.21 g(mark(X)) -> mark(g(X)) 1162.74/296.21 proper(c(X)) -> c(proper(X)) 1162.74/296.21 f(mark(X)) -> mark(f(X)) 1162.74/296.21 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.21 top(mark(X)) -> top(proper(X)) 1162.74/296.21 proper(a()) -> ok(a()) 1162.74/296.21 top(ok(X)) -> top(active(X)) 1162.74/296.21 Matrix Interpretation Processor: dim=3 1162.74/296.21 1162.74/296.21 max_matrix: 1162.74/296.21 [1 2 2] 1162.74/296.21 [0 1 1] 1162.74/296.21 [0 0 1] 1162.74/296.21 interpretation: 1162.74/296.21 [1 2 2] [0] 1162.74/296.21 [top](x0) = [0 1 1]x0 + [1] 1162.74/296.21 [0 0 0] [3], 1162.74/296.21 1162.74/296.21 [1 1 0] [0] 1162.74/296.21 [ok](x0) = [0 1 0]x0 + [1] 1162.74/296.21 [0 0 1] [0], 1162.74/296.21 1162.74/296.21 [1 1 0] [0] 1162.74/296.21 [proper](x0) = [0 1 0]x0 + [1] 1162.74/296.21 [0 0 1] [0], 1162.74/296.21 1162.74/296.21 [1 1 0] [0] 1162.74/296.21 [mark](x0) = [0 1 1]x0 + [1] 1162.74/296.21 [0 0 0] [0], 1162.74/296.21 1162.74/296.21 [1 0 0] [0] 1162.74/296.21 [c](x0) = [0 1 0]x0 + [0] 1162.74/296.21 [0 0 0] [1], 1162.74/296.21 1162.74/296.21 1162.74/296.21 [g](x0) = x0 1162.74/296.21 , 1162.74/296.21 1162.74/296.21 [1 1 0] 1162.74/296.21 [active](x0) = [0 1 1]x0 1162.74/296.21 [0 0 0] , 1162.74/296.21 1162.74/296.21 [1 1 1] [0] 1162.74/296.21 [f](x0) = [0 1 0]x0 + [1] 1162.74/296.21 [0 0 1] [0], 1162.74/296.21 1162.74/296.21 [0] 1162.74/296.21 [a] = [0] 1162.74/296.21 [2] 1162.74/296.21 orientation: 1162.74/296.21 [1 2 1] [1] [1 2 1] [0] 1162.74/296.21 active(f(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = f(active(X)) 1162.74/296.21 [0 0 0] [0] [0 0 0] [0] 1162.74/296.21 1162.74/296.21 [1 1 0] [1 1 0] 1162.74/296.21 active(g(X)) = [0 1 1]X >= [0 1 1]X = g(active(X)) 1162.74/296.21 [0 0 0] [0 0 0] 1162.74/296.21 1162.74/296.21 [1 2 1] [1] [1 2 1] [1] 1162.74/296.21 f(ok(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = ok(f(X)) 1162.74/296.21 [0 0 1] [0] [0 0 1] [0] 1162.74/296.21 1162.74/296.21 [1 2 1] [1] [1 2 1] [1] 1162.74/296.21 proper(f(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = f(proper(X)) 1162.74/296.21 [0 0 1] [0] [0 0 1] [0] 1162.74/296.21 1162.74/296.21 [1 1 0] [0] [1 1 0] [0] 1162.74/296.21 proper(g(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = g(proper(X)) 1162.74/296.21 [0 0 1] [0] [0 0 1] [0] 1162.74/296.21 1162.74/296.21 [1 1 0] [0] [1 1 0] [0] 1162.74/296.21 c(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(c(X)) 1162.74/296.21 [0 0 0] [1] [0 0 0] [1] 1162.74/296.21 1162.74/296.21 [1 1 0] [0] [1 1 0] [0] 1162.74/296.21 g(mark(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = mark(g(X)) 1162.74/296.21 [0 0 0] [0] [0 0 0] [0] 1162.74/296.21 1162.74/296.21 [1 1 0] [0] [1 1 0] [0] 1162.74/296.21 proper(c(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = c(proper(X)) 1162.74/296.21 [0 0 0] [1] [0 0 0] [1] 1162.74/296.21 1162.74/296.21 [1 2 1] [1] [1 2 1] [1] 1162.74/296.21 f(mark(X)) = [0 1 1]X + [2] >= [0 1 1]X + [2] = mark(f(X)) 1162.74/296.21 [0 0 0] [0] [0 0 0] [0] 1162.74/296.21 1162.74/296.21 [7] [7] 1162.74/296.21 active(f(f(a()))) = [4] >= [4] = mark(c(f(g(f(a()))))) 1162.74/296.21 [0] [0] 1162.74/296.21 1162.74/296.21 [1 3 2] [2] [1 3 2] [2] 1162.74/296.21 top(mark(X)) = [0 1 1]X + [2] >= [0 1 1]X + [2] = top(proper(X)) 1162.74/296.21 [0 0 0] [3] [0 0 0] [3] 1162.74/296.21 1162.74/296.21 [0] [0] 1162.74/296.21 proper(a()) = [1] >= [1] = ok(a()) 1162.74/296.21 [2] [2] 1162.74/296.21 1162.74/296.21 [1 3 2] [2] [1 3 2] [0] 1162.74/296.21 top(ok(X)) = [0 1 1]X + [2] >= [0 1 1]X + [1] = top(active(X)) 1162.74/296.21 [0 0 0] [3] [0 0 0] [3] 1162.74/296.21 1162.74/296.21 [1 1 0] [0] [1 1 0] [0] 1162.74/296.21 g(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 1162.74/296.21 [0 0 1] [0] [0 0 1] [0] 1162.74/296.21 problem: 1162.74/296.21 strict: 1162.74/296.21 1162.74/296.21 weak: 1162.74/296.21 active(f(X)) -> f(active(X)) 1162.74/296.21 active(g(X)) -> g(active(X)) 1162.74/296.21 f(ok(X)) -> ok(f(X)) 1162.74/296.21 proper(f(X)) -> f(proper(X)) 1162.74/296.21 proper(g(X)) -> g(proper(X)) 1162.74/296.21 c(ok(X)) -> ok(c(X)) 1162.74/296.21 g(mark(X)) -> mark(g(X)) 1162.74/296.21 proper(c(X)) -> c(proper(X)) 1162.74/296.21 f(mark(X)) -> mark(f(X)) 1162.74/296.21 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.22 top(mark(X)) -> top(proper(X)) 1162.74/296.22 proper(a()) -> ok(a()) 1162.74/296.22 top(ok(X)) -> top(active(X)) 1162.74/296.22 g(ok(X)) -> ok(g(X)) 1162.74/296.22 Qed 1162.74/296.22 1162.74/296.22 strict: 1162.74/296.22 active(f(X)) -> f(active(X)) 1162.74/296.22 active(g(X)) -> g(active(X)) 1162.74/296.22 g(ok(X)) -> ok(g(X)) 1162.74/296.22 weak: 1162.74/296.22 f(ok(X)) -> ok(f(X)) 1162.74/296.22 proper(f(X)) -> f(proper(X)) 1162.74/296.22 proper(g(X)) -> g(proper(X)) 1162.74/296.22 c(ok(X)) -> ok(c(X)) 1162.74/296.22 g(mark(X)) -> mark(g(X)) 1162.74/296.22 proper(c(X)) -> c(proper(X)) 1162.74/296.22 f(mark(X)) -> mark(f(X)) 1162.74/296.22 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.22 top(mark(X)) -> top(proper(X)) 1162.74/296.22 proper(a()) -> ok(a()) 1162.74/296.22 top(ok(X)) -> top(active(X)) 1162.74/296.22 Matrix Interpretation Processor: dim=3 1162.74/296.22 1162.74/296.22 max_matrix: 1162.74/296.22 [1 2 2] 1162.74/296.22 [0 1 1] 1162.74/296.22 [0 0 1] 1162.74/296.22 interpretation: 1162.74/296.22 [1 2 2] [2] 1162.74/296.22 [top](x0) = [0 0 0]x0 + [2] 1162.74/296.22 [0 0 0] [0], 1162.74/296.22 1162.74/296.22 [2] 1162.74/296.22 [ok](x0) = x0 + [1] 1162.74/296.22 [0], 1162.74/296.22 1162.74/296.22 [1 1 0] [2] 1162.74/296.22 [proper](x0) = [0 1 0]x0 + [1] 1162.74/296.22 [0 0 1] [0], 1162.74/296.22 1162.74/296.22 [1 1 0] [0] 1162.74/296.22 [mark](x0) = [0 1 1]x0 + [2] 1162.74/296.22 [0 0 0] [0], 1162.74/296.22 1162.74/296.22 [1 0 0] 1162.74/296.22 [c](x0) = [0 1 0]x0 1162.74/296.22 [0 0 0] , 1162.74/296.22 1162.74/296.22 1162.74/296.22 [g](x0) = x0 1162.74/296.22 , 1162.74/296.22 1162.74/296.22 [1 0 0] [2] 1162.74/296.22 [active](x0) = [0 1 1]x0 + [0] 1162.74/296.22 [0 0 0] [0], 1162.74/296.22 1162.74/296.22 [1 1 1] [0] 1162.74/296.22 [f](x0) = [0 1 0]x0 + [1] 1162.74/296.22 [0 0 1] [0], 1162.74/296.22 1162.74/296.22 [0] 1162.74/296.22 [a] = [0] 1162.74/296.22 [2] 1162.74/296.22 orientation: 1162.74/296.22 [1 1 1] [3] [1 1 1] [2] 1162.74/296.22 f(ok(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = ok(f(X)) 1162.74/296.22 [0 0 1] [0] [0 0 1] [0] 1162.74/296.22 1162.74/296.22 [1 2 1] [3] [1 2 1] [3] 1162.74/296.22 proper(f(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = f(proper(X)) 1162.74/296.22 [0 0 1] [0] [0 0 1] [0] 1162.74/296.22 1162.74/296.22 [1 1 0] [2] [1 1 0] [2] 1162.74/296.22 proper(g(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = g(proper(X)) 1162.74/296.22 [0 0 1] [0] [0 0 1] [0] 1162.74/296.22 1162.74/296.22 [1 0 0] [2] [1 0 0] [2] 1162.74/296.22 c(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(c(X)) 1162.74/296.22 [0 0 0] [0] [0 0 0] [0] 1162.74/296.22 1162.74/296.22 [1 1 0] [0] [1 1 0] [0] 1162.74/296.22 g(mark(X)) = [0 1 1]X + [2] >= [0 1 1]X + [2] = mark(g(X)) 1162.74/296.22 [0 0 0] [0] [0 0 0] [0] 1162.74/296.22 1162.74/296.22 [1 1 0] [2] [1 1 0] [2] 1162.74/296.22 proper(c(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = c(proper(X)) 1162.74/296.22 [0 0 0] [0] [0 0 0] [0] 1162.74/296.22 1162.74/296.22 [1 2 1] [2] [1 2 1] [1] 1162.74/296.22 f(mark(X)) = [0 1 1]X + [3] >= [0 1 1]X + [3] = mark(f(X)) 1162.74/296.22 [0 0 0] [0] [0 0 0] [0] 1162.74/296.22 1162.74/296.22 [7] [7] 1162.74/296.22 active(f(f(a()))) = [4] >= [4] = mark(c(f(g(f(a()))))) 1162.74/296.22 [0] [0] 1162.74/296.22 1162.74/296.22 [1 3 2] [6] [1 3 2] [6] 1162.74/296.22 top(mark(X)) = [0 0 0]X + [2] >= [0 0 0]X + [2] = top(proper(X)) 1162.74/296.22 [0 0 0] [0] [0 0 0] [0] 1162.74/296.22 1162.74/296.22 [2] [2] 1162.74/296.22 proper(a()) = [1] >= [1] = ok(a()) 1162.74/296.22 [2] [2] 1162.74/296.22 1162.74/296.22 [1 2 2] [6] [1 2 2] [4] 1162.74/296.22 top(ok(X)) = [0 0 0]X + [2] >= [0 0 0]X + [2] = top(active(X)) 1162.74/296.22 [0 0 0] [0] [0 0 0] [0] 1162.74/296.22 1162.74/296.22 [1 1 1] [2] [1 1 1] [2] 1162.74/296.22 active(f(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = f(active(X)) 1162.74/296.22 [0 0 0] [0] [0 0 0] [0] 1162.74/296.22 1162.74/296.22 [1 0 0] [2] [1 0 0] [2] 1162.74/296.22 active(g(X)) = [0 1 1]X + [0] >= [0 1 1]X + [0] = g(active(X)) 1162.74/296.22 [0 0 0] [0] [0 0 0] [0] 1162.74/296.22 1162.74/296.22 [2] [2] 1162.74/296.22 g(ok(X)) = X + [1] >= X + [1] = ok(g(X)) 1162.74/296.22 [0] [0] 1162.74/296.22 problem: 1162.74/296.22 strict: 1162.74/296.22 1162.74/296.22 weak: 1162.74/296.22 f(ok(X)) -> ok(f(X)) 1162.74/296.22 proper(f(X)) -> f(proper(X)) 1162.74/296.22 proper(g(X)) -> g(proper(X)) 1162.74/296.22 c(ok(X)) -> ok(c(X)) 1162.74/296.22 g(mark(X)) -> mark(g(X)) 1162.74/296.22 proper(c(X)) -> c(proper(X)) 1162.74/296.22 f(mark(X)) -> mark(f(X)) 1162.74/296.22 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.22 top(mark(X)) -> top(proper(X)) 1162.74/296.22 proper(a()) -> ok(a()) 1162.74/296.22 top(ok(X)) -> top(active(X)) 1162.74/296.22 active(f(X)) -> f(active(X)) 1162.74/296.22 active(g(X)) -> g(active(X)) 1162.74/296.22 g(ok(X)) -> ok(g(X)) 1162.74/296.22 Qed 1162.74/296.22 1162.74/296.22 strict: 1162.74/296.22 active(f(X)) -> f(active(X)) 1162.74/296.22 active(g(X)) -> g(active(X)) 1162.74/296.22 proper(f(X)) -> f(proper(X)) 1162.74/296.22 f(ok(X)) -> ok(f(X)) 1162.74/296.22 g(ok(X)) -> ok(g(X)) 1162.74/296.22 weak: 1162.74/296.22 proper(g(X)) -> g(proper(X)) 1162.74/296.22 c(ok(X)) -> ok(c(X)) 1162.74/296.22 g(mark(X)) -> mark(g(X)) 1162.74/296.22 proper(c(X)) -> c(proper(X)) 1162.74/296.22 f(mark(X)) -> mark(f(X)) 1162.74/296.22 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.22 top(mark(X)) -> top(proper(X)) 1162.74/296.22 proper(a()) -> ok(a()) 1162.74/296.22 top(ok(X)) -> top(active(X)) 1162.74/296.22 Matrix Interpretation Processor: dim=3 1162.74/296.22 1162.74/296.22 max_matrix: 1162.74/296.22 [1 2 2] 1162.74/296.22 [0 1 0] 1162.74/296.22 [0 0 1] 1162.74/296.22 interpretation: 1162.74/296.22 [1 2 1] [0] 1162.74/296.22 [top](x0) = [0 0 0]x0 + [3] 1162.74/296.22 [0 0 0] [0], 1162.74/296.22 1162.74/296.22 [1 1 0] [0] 1162.74/296.22 [ok](x0) = [0 1 0]x0 + [0] 1162.74/296.22 [0 0 1] [2], 1162.74/296.22 1162.74/296.22 [1 0 1] [2] 1162.74/296.22 [proper](x0) = [0 1 0]x0 + [0] 1162.74/296.22 [0 0 1] [2], 1162.74/296.22 1162.74/296.22 [1 0 2] [0] 1162.74/296.22 [mark](x0) = [0 1 0]x0 + [2] 1162.74/296.22 [0 0 0] [0], 1162.74/296.22 1162.74/296.22 [1 0 0] 1162.74/296.22 [c](x0) = [0 0 0]x0 1162.74/296.22 [0 0 1] , 1162.74/296.22 1162.74/296.22 [1 1 0] [0] 1162.74/296.22 [g](x0) = [0 1 0]x0 + [0] 1162.74/296.22 [0 0 1] [1], 1162.74/296.22 1162.74/296.22 [1 1 0] [2] 1162.74/296.22 [active](x0) = [0 1 0]x0 + [0] 1162.74/296.22 [0 0 1] [0], 1162.74/296.22 1162.74/296.22 [1] 1162.74/296.22 [f](x0) = x0 + [0] 1162.74/296.22 [0], 1162.74/296.22 1162.74/296.22 [0] 1162.74/296.22 [a] = [2] 1162.74/296.22 [0] 1162.74/296.22 orientation: 1162.74/296.22 [1 1 1] [3] [1 1 1] [2] 1162.74/296.22 proper(g(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = g(proper(X)) 1162.74/296.22 [0 0 1] [3] [0 0 1] [3] 1162.74/296.22 1162.74/296.22 [1 1 0] [0] [1 0 0] [0] 1162.74/296.23 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 1162.74/296.23 [0 0 1] [2] [0 0 1] [2] 1162.74/296.23 1162.74/296.23 [1 1 2] [2] [1 1 2] [2] 1162.74/296.23 g(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = mark(g(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [0] 1162.74/296.23 1162.74/296.23 [1 0 1] [2] [1 0 1] [2] 1162.74/296.23 proper(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(proper(X)) 1162.74/296.23 [0 0 1] [2] [0 0 1] [2] 1162.74/296.23 1162.74/296.23 [1 0 2] [1] [1 0 2] [1] 1162.74/296.23 f(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = mark(f(X)) 1162.74/296.23 [0 0 0] [0] [0 0 0] [0] 1162.74/296.23 1162.74/296.23 [6] [6] 1162.74/296.23 active(f(f(a()))) = [2] >= [2] = mark(c(f(g(f(a()))))) 1162.74/296.23 [0] [0] 1162.74/296.23 1162.74/296.23 [1 2 2] [4] [1 2 2] [4] 1162.74/296.23 top(mark(X)) = [0 0 0]X + [3] >= [0 0 0]X + [3] = top(proper(X)) 1162.74/296.23 [0 0 0] [0] [0 0 0] [0] 1162.74/296.23 1162.74/296.23 [2] [2] 1162.74/296.23 proper(a()) = [2] >= [2] = ok(a()) 1162.74/296.23 [2] [2] 1162.74/296.23 1162.74/296.23 [1 3 1] [2] [1 3 1] [2] 1162.74/296.23 top(ok(X)) = [0 0 0]X + [3] >= [0 0 0]X + [3] = top(active(X)) 1162.74/296.23 [0 0 0] [0] [0 0 0] [0] 1162.74/296.23 1162.74/296.23 [1 1 0] [3] [1 1 0] [3] 1162.74/296.23 active(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(active(X)) 1162.74/296.23 [0 0 1] [0] [0 0 1] [0] 1162.74/296.23 1162.74/296.23 [1 2 0] [2] [1 2 0] [2] 1162.74/296.23 active(g(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = g(active(X)) 1162.74/296.23 [0 0 1] [1] [0 0 1] [1] 1162.74/296.23 1162.74/296.23 [1 0 1] [3] [1 0 1] [3] 1162.74/296.23 proper(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(proper(X)) 1162.74/296.23 [0 0 1] [2] [0 0 1] [2] 1162.74/296.23 1162.74/296.23 [1 1 0] [1] [1 1 0] [1] 1162.74/296.23 f(ok(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = ok(f(X)) 1162.74/296.23 [0 0 1] [2] [0 0 1] [2] 1162.74/296.23 1162.74/296.23 [1 2 0] [0] [1 2 0] [0] 1162.74/296.23 g(ok(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = ok(g(X)) 1162.74/296.23 [0 0 1] [3] [0 0 1] [3] 1162.74/296.23 problem: 1162.74/296.23 strict: 1162.74/296.23 1162.74/296.23 weak: 1162.74/296.23 proper(g(X)) -> g(proper(X)) 1162.74/296.23 c(ok(X)) -> ok(c(X)) 1162.74/296.23 g(mark(X)) -> mark(g(X)) 1162.74/296.23 proper(c(X)) -> c(proper(X)) 1162.74/296.23 f(mark(X)) -> mark(f(X)) 1162.74/296.23 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.23 top(mark(X)) -> top(proper(X)) 1162.74/296.23 proper(a()) -> ok(a()) 1162.74/296.23 top(ok(X)) -> top(active(X)) 1162.74/296.23 active(f(X)) -> f(active(X)) 1162.74/296.23 active(g(X)) -> g(active(X)) 1162.74/296.23 proper(f(X)) -> f(proper(X)) 1162.74/296.23 f(ok(X)) -> ok(f(X)) 1162.74/296.23 g(ok(X)) -> ok(g(X)) 1162.74/296.23 Qed 1162.74/296.23 1162.74/296.23 strict: 1162.74/296.23 active(f(X)) -> f(active(X)) 1162.74/296.23 active(g(X)) -> g(active(X)) 1162.74/296.23 f(mark(X)) -> mark(f(X)) 1162.74/296.23 g(mark(X)) -> mark(g(X)) 1162.74/296.23 proper(f(X)) -> f(proper(X)) 1162.74/296.23 proper(c(X)) -> c(proper(X)) 1162.74/296.23 proper(g(X)) -> g(proper(X)) 1162.74/296.23 f(ok(X)) -> ok(f(X)) 1162.74/296.23 c(ok(X)) -> ok(c(X)) 1162.74/296.23 g(ok(X)) -> ok(g(X)) 1162.74/296.23 weak: 1162.74/296.23 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.23 top(mark(X)) -> top(proper(X)) 1162.74/296.23 proper(a()) -> ok(a()) 1162.74/296.23 top(ok(X)) -> top(active(X)) 1162.74/296.23 Matrix Interpretation Processor: dim=3 1162.74/296.23 1162.74/296.23 max_matrix: 1162.74/296.23 [1 0 1] 1162.74/296.23 [0 0 1] 1162.74/296.23 [0 0 1] 1162.74/296.23 interpretation: 1162.74/296.23 [1 0 0] [0] 1162.74/296.23 [top](x0) = [0 0 1]x0 + [0] 1162.74/296.23 [0 0 0] [1], 1162.74/296.23 1162.74/296.23 [1 0 0] 1162.74/296.23 [ok](x0) = [0 0 0]x0 1162.74/296.23 [0 0 1] , 1162.74/296.23 1162.74/296.23 [1 0 0] 1162.74/296.23 [proper](x0) = [0 0 0]x0 1162.74/296.23 [0 0 1] , 1162.74/296.23 1162.74/296.23 [1 0 0] 1162.74/296.23 [mark](x0) = [0 0 0]x0 1162.74/296.23 [0 0 1] , 1162.74/296.23 1162.74/296.23 [1 0 0] [0] 1162.74/296.23 [c](x0) = [0 0 0]x0 + [0] 1162.74/296.23 [0 0 0] [1], 1162.74/296.23 1162.74/296.23 [1 0 0] 1162.74/296.23 [g](x0) = [0 0 0]x0 1162.74/296.23 [0 0 0] , 1162.74/296.23 1162.74/296.23 [1 0 0] 1162.74/296.23 [active](x0) = [0 0 0]x0 1162.74/296.23 [0 0 1] , 1162.74/296.23 1162.74/296.23 [1 0 1] [0] 1162.74/296.23 [f](x0) = [0 0 0]x0 + [0] 1162.74/296.23 [0 0 0] [1], 1162.74/296.23 1162.74/296.23 [0] 1162.74/296.23 [a] = [0] 1162.74/296.23 [0] 1162.74/296.23 orientation: 1162.74/296.23 [1] [0] 1162.74/296.23 active(f(f(a()))) = [0] >= [0] = mark(c(f(g(f(a()))))) 1162.74/296.23 [1] [1] 1162.74/296.23 1162.74/296.23 [1 0 0] [0] [1 0 0] [0] 1162.74/296.23 top(mark(X)) = [0 0 1]X + [0] >= [0 0 1]X + [0] = top(proper(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [1] 1162.74/296.23 1162.74/296.23 [0] [0] 1162.74/296.23 proper(a()) = [0] >= [0] = ok(a()) 1162.74/296.23 [0] [0] 1162.74/296.23 1162.74/296.23 [1 0 0] [0] [1 0 0] [0] 1162.74/296.23 top(ok(X)) = [0 0 1]X + [0] >= [0 0 1]X + [0] = top(active(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [1] 1162.74/296.23 1162.74/296.23 [1 0 1] [0] [1 0 1] [0] 1162.74/296.23 active(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(active(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [1] 1162.74/296.23 1162.74/296.23 [1 0 0] [1 0 0] 1162.74/296.23 active(g(X)) = [0 0 0]X >= [0 0 0]X = g(active(X)) 1162.74/296.23 [0 0 0] [0 0 0] 1162.74/296.23 1162.74/296.23 [1 0 1] [0] [1 0 1] [0] 1162.74/296.23 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(f(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [1] 1162.74/296.23 1162.74/296.23 [1 0 0] [1 0 0] 1162.74/296.23 g(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(g(X)) 1162.74/296.23 [0 0 0] [0 0 0] 1162.74/296.23 1162.74/296.23 [1 0 1] [0] [1 0 1] [0] 1162.74/296.23 proper(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(proper(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [1] 1162.74/296.23 1162.74/296.23 [1 0 0] [0] [1 0 0] [0] 1162.74/296.23 proper(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(proper(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [1] 1162.74/296.23 1162.74/296.23 [1 0 0] [1 0 0] 1162.74/296.23 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 1162.74/296.23 [0 0 0] [0 0 0] 1162.74/296.23 1162.74/296.23 [1 0 1] [0] [1 0 1] [0] 1162.74/296.23 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [1] 1162.74/296.23 1162.74/296.23 [1 0 0] [0] [1 0 0] [0] 1162.74/296.23 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 1162.74/296.23 [0 0 0] [1] [0 0 0] [1] 1162.74/296.23 1162.74/296.23 [1 0 0] [1 0 0] 1162.74/296.23 g(ok(X)) = [0 0 0]X >= [0 0 0]X = ok(g(X)) 1162.74/296.23 [0 0 0] [0 0 0] 1162.74/296.23 problem: 1162.74/296.23 strict: 1162.74/296.23 1162.74/296.23 weak: 1162.74/296.23 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 1162.74/296.23 top(mark(X)) -> top(proper(X)) 1162.74/296.23 proper(a()) -> ok(a()) 1162.74/296.23 top(ok(X)) -> top(active(X)) 1162.74/296.23 active(f(X)) -> f(active(X)) 1162.74/296.23 active(g(X)) -> g(active(X)) 1162.74/296.23 f(mark(X)) -> mark(f(X)) 1162.74/296.23 g(mark(X)) -> mark(g(X)) 1162.74/296.23 proper(f(X)) -> f(proper(X)) 1162.74/296.23 proper(c(X)) -> c(proper(X)) 1162.74/296.23 proper(g(X)) -> g(proper(X)) 1162.74/296.23 f(ok(X)) -> ok(f(X)) 1162.74/296.23 c(ok(X)) -> ok(c(X)) 1162.74/296.23 g(ok(X)) -> ok(g(X)) 1162.74/296.23 Qed 1162.74/296.24 EOF