YES(?,O(n^2)) 180.57/61.71 YES(?,O(n^2)) 180.57/61.72 180.57/61.72 Problem: 180.57/61.72 active(f(x)) -> mark(x) 180.57/61.72 top(active(c())) -> top(mark(c())) 180.57/61.72 top(mark(x)) -> top(check(x)) 180.57/61.72 check(f(x)) -> f(check(x)) 180.57/61.72 check(x) -> start(match(f(X()),x)) 180.57/61.72 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.72 match(X(),x) -> proper(x) 180.57/61.72 proper(c()) -> ok(c()) 180.57/61.72 proper(f(x)) -> f(proper(x)) 180.57/61.72 f(ok(x)) -> ok(f(x)) 180.57/61.72 start(ok(x)) -> found(x) 180.57/61.72 f(found(x)) -> found(f(x)) 180.57/61.72 top(found(x)) -> top(active(x)) 180.57/61.72 active(f(x)) -> f(active(x)) 180.57/61.72 f(mark(x)) -> mark(f(x)) 180.57/61.72 180.57/61.72 Proof: 180.57/61.72 Complexity Transformation Processor: 180.57/61.72 strict: 180.57/61.72 active(f(x)) -> mark(x) 180.57/61.72 top(active(c())) -> top(mark(c())) 180.57/61.72 top(mark(x)) -> top(check(x)) 180.57/61.72 check(f(x)) -> f(check(x)) 180.57/61.72 check(x) -> start(match(f(X()),x)) 180.57/61.72 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.72 match(X(),x) -> proper(x) 180.57/61.72 proper(c()) -> ok(c()) 180.57/61.72 proper(f(x)) -> f(proper(x)) 180.57/61.72 f(ok(x)) -> ok(f(x)) 180.57/61.72 start(ok(x)) -> found(x) 180.57/61.72 f(found(x)) -> found(f(x)) 180.57/61.72 top(found(x)) -> top(active(x)) 180.57/61.72 active(f(x)) -> f(active(x)) 180.57/61.72 f(mark(x)) -> mark(f(x)) 180.57/61.72 weak: 180.57/61.72 180.57/61.72 Matrix Interpretation Processor: dim=1 180.57/61.72 180.57/61.72 max_matrix: 180.57/61.72 1 180.57/61.72 interpretation: 180.57/61.72 [found](x0) = x0 + 6, 180.57/61.72 180.57/61.72 [ok](x0) = x0 + 6, 180.57/61.72 180.57/61.72 [proper](x0) = x0, 180.57/61.72 180.57/61.72 [start](x0) = x0 + 5, 180.57/61.72 180.57/61.72 [match](x0, x1) = x0 + x1, 180.57/61.72 180.57/61.72 [X] = 9, 180.57/61.72 180.57/61.72 [check](x0) = x0 + 6, 180.57/61.72 180.57/61.72 [top](x0) = x0 + 8, 180.57/61.72 180.57/61.72 [c] = 8, 180.57/61.72 180.57/61.72 [mark](x0) = x0 + 4, 180.57/61.72 180.57/61.72 [active](x0) = x0 + 4, 180.57/61.72 180.57/61.72 [f](x0) = x0 + 10 180.57/61.72 orientation: 180.57/61.72 active(f(x)) = x + 14 >= x + 4 = mark(x) 180.57/61.72 180.57/61.72 top(active(c())) = 20 >= 20 = top(mark(c())) 180.57/61.72 180.57/61.72 top(mark(x)) = x + 12 >= x + 14 = top(check(x)) 180.57/61.72 180.57/61.72 check(f(x)) = x + 16 >= x + 16 = f(check(x)) 180.57/61.72 180.57/61.72 check(x) = x + 6 >= x + 24 = start(match(f(X()),x)) 180.57/61.72 180.57/61.72 match(f(x),f(y)) = x + y + 20 >= x + y + 10 = f(match(x,y)) 180.57/61.72 180.57/61.72 match(X(),x) = x + 9 >= x = proper(x) 180.57/61.72 180.57/61.72 proper(c()) = 8 >= 14 = ok(c()) 180.57/61.72 180.57/61.72 proper(f(x)) = x + 10 >= x + 10 = f(proper(x)) 180.57/61.72 180.57/61.72 f(ok(x)) = x + 16 >= x + 16 = ok(f(x)) 180.57/61.72 180.57/61.72 start(ok(x)) = x + 11 >= x + 6 = found(x) 180.57/61.72 180.57/61.72 f(found(x)) = x + 16 >= x + 16 = found(f(x)) 180.57/61.72 180.57/61.72 top(found(x)) = x + 14 >= x + 12 = top(active(x)) 180.57/61.72 180.57/61.72 active(f(x)) = x + 14 >= x + 14 = f(active(x)) 180.57/61.72 180.57/61.72 f(mark(x)) = x + 14 >= x + 14 = mark(f(x)) 180.57/61.72 problem: 180.57/61.72 strict: 180.57/61.72 top(active(c())) -> top(mark(c())) 180.57/61.72 top(mark(x)) -> top(check(x)) 180.57/61.72 check(f(x)) -> f(check(x)) 180.57/61.72 check(x) -> start(match(f(X()),x)) 180.57/61.72 proper(c()) -> ok(c()) 180.57/61.72 proper(f(x)) -> f(proper(x)) 180.57/61.72 f(ok(x)) -> ok(f(x)) 180.57/61.72 f(found(x)) -> found(f(x)) 180.57/61.72 active(f(x)) -> f(active(x)) 180.57/61.72 f(mark(x)) -> mark(f(x)) 180.57/61.72 weak: 180.57/61.72 active(f(x)) -> mark(x) 180.57/61.72 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.72 match(X(),x) -> proper(x) 180.57/61.72 start(ok(x)) -> found(x) 180.57/61.72 top(found(x)) -> top(active(x)) 180.57/61.72 Matrix Interpretation Processor: dim=1 180.57/61.72 180.57/61.72 max_matrix: 180.57/61.72 1 180.57/61.72 interpretation: 180.57/61.72 [found](x0) = x0 + 4, 180.57/61.72 180.57/61.72 [ok](x0) = x0 + 9, 180.57/61.72 180.57/61.72 [proper](x0) = x0, 180.57/61.72 180.57/61.72 [start](x0) = x0 + 1, 180.57/61.72 180.57/61.72 [match](x0, x1) = x0 + x1 + 4, 180.57/61.72 180.57/61.72 [X] = 0, 180.57/61.72 180.57/61.72 [check](x0) = x0 + 8, 180.57/61.72 180.57/61.72 [top](x0) = x0 + 10, 180.57/61.72 180.57/61.72 [c] = 8, 180.57/61.72 180.57/61.72 [mark](x0) = x0 + 4, 180.57/61.72 180.57/61.72 [active](x0) = x0 + 4, 180.57/61.72 180.57/61.72 [f](x0) = x0 180.57/61.72 orientation: 180.57/61.72 top(active(c())) = 22 >= 22 = top(mark(c())) 180.57/61.72 180.57/61.72 top(mark(x)) = x + 14 >= x + 18 = top(check(x)) 180.57/61.72 180.57/61.72 check(f(x)) = x + 8 >= x + 8 = f(check(x)) 180.57/61.72 180.57/61.72 check(x) = x + 8 >= x + 5 = start(match(f(X()),x)) 180.57/61.72 180.57/61.72 proper(c()) = 8 >= 17 = ok(c()) 180.57/61.72 180.57/61.72 proper(f(x)) = x >= x = f(proper(x)) 180.57/61.72 180.57/61.72 f(ok(x)) = x + 9 >= x + 9 = ok(f(x)) 180.57/61.72 180.57/61.72 f(found(x)) = x + 4 >= x + 4 = found(f(x)) 180.57/61.72 180.57/61.72 active(f(x)) = x + 4 >= x + 4 = f(active(x)) 180.57/61.72 180.57/61.72 f(mark(x)) = x + 4 >= x + 4 = mark(f(x)) 180.57/61.72 180.57/61.72 active(f(x)) = x + 4 >= x + 4 = mark(x) 180.57/61.72 180.57/61.72 match(f(x),f(y)) = x + y + 4 >= x + y + 4 = f(match(x,y)) 180.57/61.72 180.57/61.72 match(X(),x) = x + 4 >= x = proper(x) 180.57/61.72 180.57/61.72 start(ok(x)) = x + 10 >= x + 4 = found(x) 180.57/61.72 180.57/61.72 top(found(x)) = x + 14 >= x + 14 = top(active(x)) 180.57/61.72 problem: 180.57/61.72 strict: 180.57/61.72 top(active(c())) -> top(mark(c())) 180.57/61.72 top(mark(x)) -> top(check(x)) 180.57/61.72 check(f(x)) -> f(check(x)) 180.57/61.72 proper(c()) -> ok(c()) 180.57/61.72 proper(f(x)) -> f(proper(x)) 180.57/61.72 f(ok(x)) -> ok(f(x)) 180.57/61.72 f(found(x)) -> found(f(x)) 180.57/61.72 active(f(x)) -> f(active(x)) 180.57/61.72 f(mark(x)) -> mark(f(x)) 180.57/61.72 weak: 180.57/61.72 check(x) -> start(match(f(X()),x)) 180.57/61.72 active(f(x)) -> mark(x) 180.57/61.72 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.72 match(X(),x) -> proper(x) 180.57/61.72 start(ok(x)) -> found(x) 180.57/61.72 top(found(x)) -> top(active(x)) 180.57/61.72 Matrix Interpretation Processor: dim=1 180.57/61.72 180.57/61.72 max_matrix: 180.57/61.72 1 180.57/61.72 interpretation: 180.57/61.72 [found](x0) = x0, 180.57/61.72 180.57/61.72 [ok](x0) = x0, 180.57/61.72 180.57/61.72 [proper](x0) = x0 + 2, 180.57/61.72 180.57/61.72 [start](x0) = x0 + 6, 180.57/61.72 180.57/61.72 [match](x0, x1) = x0 + x1 + 4, 180.57/61.72 180.57/61.72 [X] = 1, 180.57/61.72 180.57/61.72 [check](x0) = x0 + 11, 180.57/61.72 180.57/61.72 [top](x0) = x0 + 1, 180.57/61.72 180.57/61.72 [c] = 8, 180.57/61.72 180.57/61.72 [mark](x0) = x0, 180.57/61.72 180.57/61.72 [active](x0) = x0, 180.57/61.72 180.57/61.72 [f](x0) = x0 180.57/61.72 orientation: 180.57/61.72 top(active(c())) = 9 >= 9 = top(mark(c())) 180.57/61.72 180.57/61.72 top(mark(x)) = x + 1 >= x + 12 = top(check(x)) 180.57/61.72 180.57/61.72 check(f(x)) = x + 11 >= x + 11 = f(check(x)) 180.57/61.72 180.57/61.72 proper(c()) = 10 >= 8 = ok(c()) 180.57/61.72 180.57/61.72 proper(f(x)) = x + 2 >= x + 2 = f(proper(x)) 180.57/61.72 180.57/61.72 f(ok(x)) = x >= x = ok(f(x)) 180.57/61.72 180.57/61.72 f(found(x)) = x >= x = found(f(x)) 180.57/61.72 180.57/61.72 active(f(x)) = x >= x = f(active(x)) 180.57/61.72 180.57/61.72 f(mark(x)) = x >= x = mark(f(x)) 180.57/61.72 180.57/61.72 check(x) = x + 11 >= x + 11 = start(match(f(X()),x)) 180.57/61.72 180.57/61.72 active(f(x)) = x >= x = mark(x) 180.57/61.72 180.57/61.72 match(f(x),f(y)) = x + y + 4 >= x + y + 4 = f(match(x,y)) 180.57/61.72 180.57/61.72 match(X(),x) = x + 5 >= x + 2 = proper(x) 180.57/61.72 180.57/61.72 start(ok(x)) = x + 6 >= x = found(x) 180.57/61.72 180.57/61.72 top(found(x)) = x + 1 >= x + 1 = top(active(x)) 180.57/61.72 problem: 180.57/61.72 strict: 180.57/61.72 top(active(c())) -> top(mark(c())) 180.57/61.72 top(mark(x)) -> top(check(x)) 180.57/61.72 check(f(x)) -> f(check(x)) 180.57/61.72 proper(f(x)) -> f(proper(x)) 180.57/61.72 f(ok(x)) -> ok(f(x)) 180.57/61.72 f(found(x)) -> found(f(x)) 180.57/61.72 active(f(x)) -> f(active(x)) 180.57/61.72 f(mark(x)) -> mark(f(x)) 180.57/61.72 weak: 180.57/61.72 proper(c()) -> ok(c()) 180.57/61.72 check(x) -> start(match(f(X()),x)) 180.57/61.72 active(f(x)) -> mark(x) 180.57/61.72 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.72 match(X(),x) -> proper(x) 180.57/61.72 start(ok(x)) -> found(x) 180.57/61.72 top(found(x)) -> top(active(x)) 180.57/61.72 Matrix Interpretation Processor: dim=1 180.57/61.72 180.57/61.72 max_matrix: 180.57/61.72 1 180.57/61.72 interpretation: 180.57/61.72 [found](x0) = x0 + 33, 180.57/61.72 180.57/61.72 [ok](x0) = x0 + 29, 180.57/61.72 180.57/61.72 [proper](x0) = x0 + 80, 180.57/61.72 180.57/61.72 [start](x0) = x0 + 4, 180.57/61.72 180.57/61.72 [match](x0, x1) = x0 + x1 + 48, 180.57/61.72 180.57/61.72 [X] = 48, 180.57/61.72 180.57/61.72 [check](x0) = x0 + 117, 180.57/61.72 180.57/61.72 [top](x0) = x0 + 90, 180.57/61.72 180.57/61.72 [c] = 33, 180.57/61.72 180.57/61.72 [mark](x0) = x0, 180.57/61.72 180.57/61.72 [active](x0) = x0 + 19, 180.57/61.72 180.57/61.72 [f](x0) = x0 + 16 180.57/61.72 orientation: 180.57/61.72 top(active(c())) = 142 >= 123 = top(mark(c())) 180.57/61.72 180.57/61.72 top(mark(x)) = x + 90 >= x + 207 = top(check(x)) 180.57/61.72 180.57/61.72 check(f(x)) = x + 133 >= x + 133 = f(check(x)) 180.57/61.72 180.57/61.72 proper(f(x)) = x + 96 >= x + 96 = f(proper(x)) 180.57/61.72 180.57/61.72 f(ok(x)) = x + 45 >= x + 45 = ok(f(x)) 180.57/61.72 180.57/61.72 f(found(x)) = x + 49 >= x + 49 = found(f(x)) 180.57/61.72 180.57/61.72 active(f(x)) = x + 35 >= x + 35 = f(active(x)) 180.57/61.72 180.57/61.72 f(mark(x)) = x + 16 >= x + 16 = mark(f(x)) 180.57/61.72 180.57/61.72 proper(c()) = 113 >= 62 = ok(c()) 180.57/61.72 180.57/61.72 check(x) = x + 117 >= x + 116 = start(match(f(X()),x)) 180.57/61.72 180.57/61.72 active(f(x)) = x + 35 >= x = mark(x) 180.57/61.72 180.57/61.72 match(f(x),f(y)) = x + y + 80 >= x + y + 64 = f(match(x,y)) 180.57/61.72 180.57/61.72 match(X(),x) = x + 96 >= x + 80 = proper(x) 180.57/61.72 180.57/61.72 start(ok(x)) = x + 33 >= x + 33 = found(x) 180.57/61.72 180.57/61.72 top(found(x)) = x + 123 >= x + 109 = top(active(x)) 180.57/61.72 problem: 180.57/61.72 strict: 180.57/61.72 top(mark(x)) -> top(check(x)) 180.57/61.72 check(f(x)) -> f(check(x)) 180.57/61.72 proper(f(x)) -> f(proper(x)) 180.57/61.72 f(ok(x)) -> ok(f(x)) 180.57/61.72 f(found(x)) -> found(f(x)) 180.57/61.72 active(f(x)) -> f(active(x)) 180.57/61.72 f(mark(x)) -> mark(f(x)) 180.57/61.72 weak: 180.57/61.72 top(active(c())) -> top(mark(c())) 180.57/61.72 proper(c()) -> ok(c()) 180.57/61.72 check(x) -> start(match(f(X()),x)) 180.57/61.72 active(f(x)) -> mark(x) 180.57/61.72 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.72 match(X(),x) -> proper(x) 180.57/61.72 start(ok(x)) -> found(x) 180.57/61.72 top(found(x)) -> top(active(x)) 180.57/61.72 Splitting Processor: 180.57/61.72 strict: 180.57/61.72 f(mark(x)) -> mark(f(x)) 180.57/61.72 weak: 180.57/61.72 top(active(c())) -> top(mark(c())) 180.57/61.72 proper(c()) -> ok(c()) 180.57/61.72 check(x) -> start(match(f(X()),x)) 180.57/61.72 active(f(x)) -> mark(x) 180.57/61.72 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.72 match(X(),x) -> proper(x) 180.57/61.72 start(ok(x)) -> found(x) 180.57/61.72 top(found(x)) -> top(active(x)) 180.57/61.72 top(mark(x)) -> top(check(x)) 180.57/61.72 check(f(x)) -> f(check(x)) 180.57/61.72 proper(f(x)) -> f(proper(x)) 180.57/61.72 f(ok(x)) -> ok(f(x)) 180.57/61.72 f(found(x)) -> found(f(x)) 180.57/61.72 active(f(x)) -> f(active(x)) 180.57/61.72 Matrix Interpretation Processor: dim=3 180.57/61.72 180.57/61.72 max_matrix: 180.57/61.72 [1 0 1] 180.57/61.72 [0 0 1] 180.57/61.72 [0 0 1] 180.57/61.72 interpretation: 180.57/61.72 [1 0 0] 180.57/61.72 [found](x0) = [0 0 0]x0 180.57/61.72 [0 0 1] , 180.57/61.72 180.57/61.72 [1 0 0] 180.57/61.72 [ok](x0) = [0 0 0]x0 180.57/61.72 [0 0 1] , 180.57/61.72 180.57/61.72 [1 0 0] 180.57/61.72 [proper](x0) = [0 0 1]x0 180.57/61.72 [0 0 1] , 180.57/61.72 180.57/61.72 [1 0 0] 180.57/61.72 [start](x0) = [0 0 0]x0 180.57/61.72 [0 0 1] , 180.57/61.72 180.57/61.72 [1 0 0] [1 0 0] [0] 180.57/61.72 [match](x0, x1) = [0 0 0]x0 + [0 0 1]x1 + [1] 180.57/61.72 [0 0 0] [0 0 1] [0], 180.57/61.72 180.57/61.72 [0] 180.57/61.72 [X] = [0] 180.57/61.72 [0], 180.57/61.72 180.57/61.72 [1 0 0] 180.57/61.72 [check](x0) = [0 0 0]x0 180.57/61.72 [0 0 1] , 180.57/61.72 180.57/61.72 [1 0 0] [0] 180.57/61.72 [top](x0) = [0 0 0]x0 + [1] 180.57/61.72 [0 0 0] [0], 180.57/61.72 180.57/61.72 [0] 180.57/61.72 [c] = [0] 180.57/61.72 [0], 180.57/61.72 180.57/61.72 [1 0 0] [0] 180.57/61.72 [mark](x0) = [0 0 0]x0 + [0] 180.57/61.72 [0 0 1] [1], 180.57/61.72 180.57/61.72 [1 0 0] 180.57/61.72 [active](x0) = [0 0 0]x0 180.57/61.72 [0 0 1] , 180.57/61.72 180.57/61.72 [1 0 1] [0] 180.57/61.72 [f](x0) = [0 0 0]x0 + [0] 180.57/61.72 [0 0 1] [1] 180.57/61.72 orientation: 180.57/61.72 [1 0 1] [1] [1 0 1] [0] 180.57/61.72 f(mark(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(f(x)) 180.57/61.72 [0 0 1] [2] [0 0 1] [2] 180.57/61.72 180.57/61.72 [0] [0] 180.57/61.72 top(active(c())) = [1] >= [1] = top(mark(c())) 180.57/61.72 [0] [0] 180.57/61.72 180.57/61.72 [0] [0] 180.57/61.72 proper(c()) = [0] >= [0] = ok(c()) 180.57/61.72 [0] [0] 180.57/61.72 180.57/61.72 [1 0 0] [1 0 0] 180.57/61.72 check(x) = [0 0 0]x >= [0 0 0]x = start(match(f(X()),x)) 180.57/61.72 [0 0 1] [0 0 1] 180.57/61.72 180.57/61.72 [1 0 1] [0] [1 0 0] [0] 180.57/61.72 active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(x) 180.57/61.72 [0 0 1] [1] [0 0 1] [1] 180.57/61.72 180.57/61.72 [1 0 1] [1 0 1] [0] [1 0 0] [1 0 1] [0] 180.57/61.72 match(f(x),f(y)) = [0 0 0]x + [0 0 1]y + [2] >= [0 0 0]x + [0 0 0]y + [0] = f(match(x,y)) 180.57/61.72 [0 0 0] [0 0 1] [1] [0 0 0] [0 0 1] [1] 180.57/61.72 180.57/61.72 [1 0 0] [0] [1 0 0] 180.57/61.72 match(X(),x) = [0 0 1]x + [1] >= [0 0 1]x = proper(x) 180.57/61.72 [0 0 1] [0] [0 0 1] 180.57/61.72 180.57/61.72 [1 0 0] [1 0 0] 180.57/61.72 start(ok(x)) = [0 0 0]x >= [0 0 0]x = found(x) 180.57/61.72 [0 0 1] [0 0 1] 180.57/61.72 180.57/61.72 [1 0 0] [0] [1 0 0] [0] 180.57/61.72 top(found(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = top(active(x)) 180.57/61.73 [0 0 0] [0] [0 0 0] [0] 180.57/61.73 180.57/61.73 [1 0 0] [0] [1 0 0] [0] 180.57/61.73 top(mark(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = top(check(x)) 180.57/61.73 [0 0 0] [0] [0 0 0] [0] 180.57/61.73 180.57/61.73 [1 0 1] [0] [1 0 1] [0] 180.57/61.73 check(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(check(x)) 180.57/61.73 [0 0 1] [1] [0 0 1] [1] 180.57/61.73 180.57/61.73 [1 0 1] [0] [1 0 1] [0] 180.57/61.73 proper(f(x)) = [0 0 1]x + [1] >= [0 0 0]x + [0] = f(proper(x)) 180.57/61.73 [0 0 1] [1] [0 0 1] [1] 180.57/61.73 180.57/61.73 [1 0 1] [0] [1 0 1] [0] 180.57/61.73 f(ok(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = ok(f(x)) 180.57/61.73 [0 0 1] [1] [0 0 1] [1] 180.57/61.73 180.57/61.73 [1 0 1] [0] [1 0 1] [0] 180.57/61.73 f(found(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = found(f(x)) 180.57/61.73 [0 0 1] [1] [0 0 1] [1] 180.57/61.73 180.57/61.73 [1 0 1] [0] [1 0 1] [0] 180.57/61.73 active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(active(x)) 180.57/61.73 [0 0 1] [1] [0 0 1] [1] 180.57/61.73 problem: 180.57/61.73 strict: 180.57/61.73 180.57/61.73 weak: 180.57/61.73 f(mark(x)) -> mark(f(x)) 180.57/61.73 top(active(c())) -> top(mark(c())) 180.57/61.73 proper(c()) -> ok(c()) 180.57/61.73 check(x) -> start(match(f(X()),x)) 180.57/61.73 active(f(x)) -> mark(x) 180.57/61.73 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.73 match(X(),x) -> proper(x) 180.57/61.73 start(ok(x)) -> found(x) 180.57/61.73 top(found(x)) -> top(active(x)) 180.57/61.73 top(mark(x)) -> top(check(x)) 180.57/61.73 check(f(x)) -> f(check(x)) 180.57/61.73 proper(f(x)) -> f(proper(x)) 180.57/61.73 f(ok(x)) -> ok(f(x)) 180.57/61.73 f(found(x)) -> found(f(x)) 180.57/61.73 active(f(x)) -> f(active(x)) 180.57/61.73 Qed 180.57/61.73 180.57/61.73 strict: 180.57/61.73 top(mark(x)) -> top(check(x)) 180.57/61.73 check(f(x)) -> f(check(x)) 180.57/61.73 proper(f(x)) -> f(proper(x)) 180.57/61.73 f(ok(x)) -> ok(f(x)) 180.57/61.73 f(found(x)) -> found(f(x)) 180.57/61.73 active(f(x)) -> f(active(x)) 180.57/61.73 weak: 180.57/61.73 f(mark(x)) -> mark(f(x)) 180.57/61.73 top(active(c())) -> top(mark(c())) 180.57/61.73 proper(c()) -> ok(c()) 180.57/61.73 check(x) -> start(match(f(X()),x)) 180.57/61.73 active(f(x)) -> mark(x) 180.57/61.73 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.73 match(X(),x) -> proper(x) 180.57/61.73 start(ok(x)) -> found(x) 180.57/61.73 top(found(x)) -> top(active(x)) 180.57/61.73 Splitting Processor: 180.57/61.73 strict: 180.57/61.73 check(f(x)) -> f(check(x)) 180.57/61.73 weak: 180.57/61.73 f(mark(x)) -> mark(f(x)) 180.57/61.73 top(active(c())) -> top(mark(c())) 180.57/61.73 proper(c()) -> ok(c()) 180.57/61.73 check(x) -> start(match(f(X()),x)) 180.57/61.73 active(f(x)) -> mark(x) 180.57/61.73 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.73 match(X(),x) -> proper(x) 180.57/61.73 start(ok(x)) -> found(x) 180.57/61.73 top(found(x)) -> top(active(x)) 180.57/61.73 top(mark(x)) -> top(check(x)) 180.57/61.73 proper(f(x)) -> f(proper(x)) 180.57/61.73 f(ok(x)) -> ok(f(x)) 180.57/61.73 f(found(x)) -> found(f(x)) 180.57/61.73 active(f(x)) -> f(active(x)) 180.57/61.73 Matrix Interpretation Processor: dim=4 180.57/61.73 180.57/61.73 max_matrix: 180.57/61.73 [1 0 1 0] 180.57/61.73 [0 0 0 1] 180.57/61.73 [0 0 1 1] 180.57/61.73 [0 0 0 0] 180.57/61.73 interpretation: 180.57/61.73 [1 0 0 0] 180.57/61.73 [0 0 0 0] 180.57/61.73 [found](x0) = [0 0 1 0]x0 180.57/61.73 [0 0 0 0] , 180.57/61.73 180.57/61.73 [1 0 0 0] 180.57/61.73 [0 0 0 0] 180.57/61.73 [ok](x0) = [0 0 1 1]x0 180.57/61.73 [0 0 0 0] , 180.57/61.73 180.57/61.73 [1 0 0 0] 180.57/61.73 [0 0 0 0] 180.57/61.73 [proper](x0) = [0 0 1 0]x0 180.57/61.73 [0 0 0 0] , 180.57/61.73 180.57/61.73 [1 0 0 0] 180.57/61.73 [0 0 0 1] 180.57/61.73 [start](x0) = [0 0 1 0]x0 180.57/61.73 [0 0 0 0] , 180.57/61.73 180.57/61.73 [1 0 0 0] [1 0 0 0] [0] 180.57/61.73 [0 0 0 1] [0 0 0 1] [1] 180.57/61.73 [match](x0, x1) = [0 0 0 0]x0 + [0 0 1 0]x1 + [0] 180.57/61.73 [0 0 0 0] [0 0 0 0] [0], 180.57/61.73 180.57/61.73 [0] 180.57/61.73 [0] 180.57/61.73 [X] = [0] 180.57/61.73 [0], 180.57/61.73 180.57/61.73 [1 0 1 0] 180.57/61.73 [0 0 0 0] 180.57/61.73 [check](x0) = [0 0 1 0]x0 180.57/61.73 [0 0 0 0] , 180.57/61.73 180.57/61.73 [1 0 0 0] 180.57/61.73 [0 0 0 0] 180.57/61.73 [top](x0) = [0 0 0 0]x0 180.57/61.73 [0 0 0 0] , 180.57/61.73 180.57/61.73 [0] 180.57/61.73 [0] 180.57/61.73 [c] = [0] 180.57/61.73 [0], 180.57/61.73 180.57/61.73 [1 0 1 0] [0] 180.57/61.73 [0 0 0 0] [0] 180.57/61.73 [mark](x0) = [0 0 1 0]x0 + [1] 180.57/61.73 [0 0 0 0] [0], 180.57/61.73 180.57/61.73 [1 0 0 0] 180.57/61.73 [0 0 0 0] 180.57/61.73 [active](x0) = [0 0 1 0]x0 180.57/61.73 [0 0 0 0] , 180.57/61.74 180.57/61.74 [1 0 1 0] [0] 180.57/61.74 [0 0 0 0] [0] 180.57/61.74 [f](x0) = [0 0 1 0]x0 + [1] 180.57/61.74 [0 0 0 0] [0] 180.57/61.74 orientation: 180.57/61.74 [1 0 2 0] [1] [1 0 2 0] [0] 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 check(f(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = f(check(x)) 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 180.57/61.74 [1 0 2 0] [1] [1 0 2 0] [1] 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 f(mark(x)) = [0 0 1 0]x + [2] >= [0 0 1 0]x + [2] = mark(f(x)) 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 180.57/61.74 [0] [0] 180.57/61.74 [0] [0] 180.57/61.74 top(active(c())) = [0] >= [0] = top(mark(c())) 180.57/61.74 [0] [0] 180.57/61.74 180.57/61.74 [0] [0] 180.57/61.74 [0] [0] 180.57/61.74 proper(c()) = [0] >= [0] = ok(c()) 180.57/61.74 [0] [0] 180.57/61.74 180.57/61.74 [1 0 1 0] [1 0 0 0] 180.57/61.74 [0 0 0 0] [0 0 0 0] 180.57/61.74 check(x) = [0 0 1 0]x >= [0 0 1 0]x = start(match(f(X()),x)) 180.57/61.74 [0 0 0 0] [0 0 0 0] 180.57/61.74 180.57/61.74 [1 0 1 0] [0] [1 0 1 0] [0] 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 active(f(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = mark(x) 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 180.57/61.74 [1 0 1 0] [1 0 1 0] [0] [1 0 0 0] [1 0 1 0] [0] 180.57/61.74 [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0] 180.57/61.74 match(f(x),f(y)) = [0 0 0 0]x + [0 0 1 0]y + [1] >= [0 0 0 0]x + [0 0 1 0]y + [1] = f(match(x,y)) 180.57/61.74 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 180.57/61.74 180.57/61.74 [1 0 0 0] [0] [1 0 0 0] 180.57/61.74 [0 0 0 1] [1] [0 0 0 0] 180.57/61.74 match(X(),x) = [0 0 1 0]x + [0] >= [0 0 1 0]x = proper(x) 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] 180.57/61.74 180.57/61.74 [1 0 0 0] [1 0 0 0] 180.57/61.74 [0 0 0 0] [0 0 0 0] 180.57/61.74 start(ok(x)) = [0 0 1 1]x >= [0 0 1 0]x = found(x) 180.57/61.74 [0 0 0 0] [0 0 0 0] 180.57/61.74 180.57/61.74 [1 0 0 0] [1 0 0 0] 180.57/61.74 [0 0 0 0] [0 0 0 0] 180.57/61.74 top(found(x)) = [0 0 0 0]x >= [0 0 0 0]x = top(active(x)) 180.57/61.74 [0 0 0 0] [0 0 0 0] 180.57/61.74 180.57/61.74 [1 0 1 0] [1 0 1 0] 180.57/61.74 [0 0 0 0] [0 0 0 0] 180.57/61.74 top(mark(x)) = [0 0 0 0]x >= [0 0 0 0]x = top(check(x)) 180.57/61.74 [0 0 0 0] [0 0 0 0] 180.57/61.74 180.57/61.74 [1 0 1 0] [0] [1 0 1 0] [0] 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 proper(f(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = f(proper(x)) 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 180.57/61.74 [1 0 1 1] [0] [1 0 1 0] [0] 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 f(ok(x)) = [0 0 1 1]x + [1] >= [0 0 1 0]x + [1] = ok(f(x)) 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 180.57/61.74 [1 0 1 0] [0] [1 0 1 0] [0] 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 f(found(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = found(f(x)) 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 180.57/61.74 [1 0 1 0] [0] [1 0 1 0] [0] 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 active(f(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = f(active(x)) 180.57/61.74 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.74 problem: 180.57/61.74 strict: 180.57/61.74 180.57/61.74 weak: 180.57/61.74 check(f(x)) -> f(check(x)) 180.57/61.74 f(mark(x)) -> mark(f(x)) 180.57/61.74 top(active(c())) -> top(mark(c())) 180.57/61.74 proper(c()) -> ok(c()) 180.57/61.74 check(x) -> start(match(f(X()),x)) 180.57/61.74 active(f(x)) -> mark(x) 180.57/61.74 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.74 match(X(),x) -> proper(x) 180.57/61.74 start(ok(x)) -> found(x) 180.57/61.74 top(found(x)) -> top(active(x)) 180.57/61.74 top(mark(x)) -> top(check(x)) 180.57/61.74 proper(f(x)) -> f(proper(x)) 180.57/61.74 f(ok(x)) -> ok(f(x)) 180.57/61.74 f(found(x)) -> found(f(x)) 180.57/61.74 active(f(x)) -> f(active(x)) 180.57/61.74 Qed 180.57/61.74 180.57/61.74 strict: 180.57/61.74 top(mark(x)) -> top(check(x)) 180.57/61.74 proper(f(x)) -> f(proper(x)) 180.57/61.74 f(ok(x)) -> ok(f(x)) 180.57/61.74 f(found(x)) -> found(f(x)) 180.57/61.74 active(f(x)) -> f(active(x)) 180.57/61.74 weak: 180.57/61.74 check(f(x)) -> f(check(x)) 180.57/61.74 f(mark(x)) -> mark(f(x)) 180.57/61.74 top(active(c())) -> top(mark(c())) 180.57/61.74 proper(c()) -> ok(c()) 180.57/61.74 check(x) -> start(match(f(X()),x)) 180.57/61.74 active(f(x)) -> mark(x) 180.57/61.74 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.74 match(X(),x) -> proper(x) 180.57/61.74 start(ok(x)) -> found(x) 180.57/61.74 top(found(x)) -> top(active(x)) 180.57/61.74 Splitting Processor: 180.57/61.74 strict: 180.57/61.74 proper(f(x)) -> f(proper(x)) 180.57/61.74 weak: 180.57/61.74 check(f(x)) -> f(check(x)) 180.57/61.74 f(mark(x)) -> mark(f(x)) 180.57/61.74 top(active(c())) -> top(mark(c())) 180.57/61.74 proper(c()) -> ok(c()) 180.57/61.74 check(x) -> start(match(f(X()),x)) 180.57/61.74 active(f(x)) -> mark(x) 180.57/61.74 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.74 match(X(),x) -> proper(x) 180.57/61.74 start(ok(x)) -> found(x) 180.57/61.74 top(found(x)) -> top(active(x)) 180.57/61.74 top(mark(x)) -> top(check(x)) 180.57/61.74 f(ok(x)) -> ok(f(x)) 180.57/61.74 f(found(x)) -> found(f(x)) 180.57/61.74 active(f(x)) -> f(active(x)) 180.57/61.74 Splitting Processor: 180.57/61.74 strict: 180.57/61.74 f(found(x)) -> found(f(x)) 180.57/61.74 weak: 180.57/61.74 proper(f(x)) -> f(proper(x)) 180.57/61.74 check(f(x)) -> f(check(x)) 180.57/61.74 f(mark(x)) -> mark(f(x)) 180.57/61.74 top(active(c())) -> top(mark(c())) 180.57/61.74 proper(c()) -> ok(c()) 180.57/61.74 check(x) -> start(match(f(X()),x)) 180.57/61.74 active(f(x)) -> mark(x) 180.57/61.74 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.74 match(X(),x) -> proper(x) 180.57/61.74 start(ok(x)) -> found(x) 180.57/61.74 top(found(x)) -> top(active(x)) 180.57/61.74 top(mark(x)) -> top(check(x)) 180.57/61.74 f(ok(x)) -> ok(f(x)) 180.57/61.74 active(f(x)) -> f(active(x)) 180.57/61.74 Splitting Processor: 180.57/61.74 strict: 180.57/61.74 active(f(x)) -> f(active(x)) 180.57/61.74 weak: 180.57/61.74 f(found(x)) -> found(f(x)) 180.57/61.74 proper(f(x)) -> f(proper(x)) 180.57/61.74 check(f(x)) -> f(check(x)) 180.57/61.74 f(mark(x)) -> mark(f(x)) 180.57/61.74 top(active(c())) -> top(mark(c())) 180.57/61.74 proper(c()) -> ok(c()) 180.57/61.74 check(x) -> start(match(f(X()),x)) 180.57/61.74 active(f(x)) -> mark(x) 180.57/61.74 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.74 match(X(),x) -> proper(x) 180.57/61.74 start(ok(x)) -> found(x) 180.57/61.74 top(found(x)) -> top(active(x)) 180.57/61.74 top(mark(x)) -> top(check(x)) 180.57/61.74 f(ok(x)) -> ok(f(x)) 180.57/61.74 Splitting Processor: 180.57/61.74 strict: 180.57/61.74 f(ok(x)) -> ok(f(x)) 180.57/61.74 weak: 180.57/61.74 active(f(x)) -> f(active(x)) 180.57/61.74 f(found(x)) -> found(f(x)) 180.57/61.74 proper(f(x)) -> f(proper(x)) 180.57/61.74 check(f(x)) -> f(check(x)) 180.57/61.74 f(mark(x)) -> mark(f(x)) 180.57/61.74 top(active(c())) -> top(mark(c())) 180.57/61.74 proper(c()) -> ok(c()) 180.57/61.74 check(x) -> start(match(f(X()),x)) 180.57/61.74 active(f(x)) -> mark(x) 180.57/61.74 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.74 match(X(),x) -> proper(x) 180.57/61.74 start(ok(x)) -> found(x) 180.57/61.74 top(found(x)) -> top(active(x)) 180.57/61.74 top(mark(x)) -> top(check(x)) 180.57/61.74 Matrix Interpretation Processor: dim=3 180.57/61.74 180.57/61.74 max_matrix: 180.57/61.74 [1 1 1] 180.57/61.74 [0 0 1] 180.57/61.74 [0 0 1] 180.57/61.74 interpretation: 180.57/61.74 [1 0 0] [0] 180.57/61.74 [found](x0) = [0 0 1]x0 + [1] 180.57/61.74 [0 0 1] [1], 180.57/61.74 180.57/61.74 [1 0 0] [0] 180.57/61.74 [ok](x0) = [0 0 0]x0 + [0] 180.57/61.74 [0 0 1] [1], 180.57/61.74 180.57/61.74 [1 0 1] [0] 180.57/61.74 [proper](x0) = [0 0 1]x0 + [1] 180.57/61.74 [0 0 1] [1], 180.57/61.74 180.57/61.74 [1 0 0] 180.57/61.74 [start](x0) = [0 0 1]x0 180.57/61.74 [0 0 1] , 180.57/61.74 180.57/61.74 [1 0 0] [1 0 1] [0] 180.57/61.74 [match](x0, x1) = [0 0 0]x0 + [0 0 1]x1 + [1] 180.57/61.74 [0 0 0] [0 0 1] [1], 180.57/61.74 180.57/61.74 [0] 180.57/61.74 [X] = [0] 180.57/61.74 [0], 180.57/61.74 180.57/61.74 [1 0 1] [0] 180.57/61.74 [check](x0) = [0 0 1]x0 + [1] 180.57/61.74 [0 0 1] [1], 180.57/61.74 180.57/61.74 [1 1 0] 180.57/61.74 [top](x0) = [0 0 0]x0 180.57/61.74 [0 0 0] , 180.57/61.74 180.57/61.74 [1] 180.57/61.74 [c] = [0] 180.57/61.74 [0], 180.57/61.74 180.57/61.74 [1 0 1] [0] 180.57/61.74 [mark](x0) = [0 0 1]x0 + [1] 180.57/61.74 [0 0 1] [1], 180.57/61.74 180.57/61.74 [1 0 0] [0] 180.57/61.74 [active](x0) = [0 0 1]x0 + [1] 180.57/61.74 [0 0 1] [0], 180.57/61.74 180.57/61.74 [1 0 1] [0] 180.57/61.74 [f](x0) = [0 0 1]x0 + [1] 180.57/61.74 [0 0 1] [1] 180.57/61.74 orientation: 180.57/61.74 [1 0 1] [1] [1 0 1] [0] 180.57/61.74 f(ok(x)) = [0 0 1]x + [2] >= [0 0 0]x + [0] = ok(f(x)) 180.57/61.74 [0 0 1] [2] [0 0 1] [2] 180.57/61.74 180.57/61.74 [1 0 1] [0] [1 0 1] [0] 180.57/61.74 active(f(x)) = [0 0 1]x + [2] >= [0 0 1]x + [1] = f(active(x)) 180.57/61.74 [0 0 1] [1] [0 0 1] [1] 180.57/61.74 180.57/61.74 [1 0 1] [1] [1 0 1] [0] 180.57/61.74 f(found(x)) = [0 0 1]x + [2] >= [0 0 1]x + [2] = found(f(x)) 180.57/61.74 [0 0 1] [2] [0 0 1] [2] 180.57/61.74 180.57/61.74 [1 0 2] [1] [1 0 2] [1] 180.57/61.74 proper(f(x)) = [0 0 1]x + [2] >= [0 0 1]x + [2] = f(proper(x)) 180.57/61.74 [0 0 1] [2] [0 0 1] [2] 180.57/61.75 180.57/61.75 [1 0 2] [1] [1 0 2] [1] 180.57/61.75 check(f(x)) = [0 0 1]x + [2] >= [0 0 1]x + [2] = f(check(x)) 180.57/61.75 [0 0 1] [2] [0 0 1] [2] 180.57/61.75 180.57/61.75 [1 0 2] [1] [1 0 2] [1] 180.57/61.75 f(mark(x)) = [0 0 1]x + [2] >= [0 0 1]x + [2] = mark(f(x)) 180.57/61.75 [0 0 1] [2] [0 0 1] [2] 180.57/61.75 180.57/61.75 [2] [2] 180.57/61.75 top(active(c())) = [0] >= [0] = top(mark(c())) 180.57/61.75 [0] [0] 180.57/61.75 180.57/61.75 [1] [1] 180.57/61.75 proper(c()) = [1] >= [0] = ok(c()) 180.57/61.75 [1] [1] 180.57/61.75 180.57/61.75 [1 0 1] [0] [1 0 1] [0] 180.57/61.75 check(x) = [0 0 1]x + [1] >= [0 0 1]x + [1] = start(match(f(X()),x)) 180.57/61.75 [0 0 1] [1] [0 0 1] [1] 180.57/61.75 180.57/61.75 [1 0 1] [0] [1 0 1] [0] 180.57/61.75 active(f(x)) = [0 0 1]x + [2] >= [0 0 1]x + [1] = mark(x) 180.57/61.75 [0 0 1] [1] [0 0 1] [1] 180.57/61.75 180.57/61.75 [1 0 1] [1 0 2] [1] [1 0 0] [1 0 2] [1] 180.57/61.75 match(f(x),f(y)) = [0 0 0]x + [0 0 1]y + [2] >= [0 0 0]x + [0 0 1]y + [2] = f(match(x,y)) 180.57/61.75 [0 0 0] [0 0 1] [2] [0 0 0] [0 0 1] [2] 180.57/61.75 180.57/61.75 [1 0 1] [0] [1 0 1] [0] 180.57/61.75 match(X(),x) = [0 0 1]x + [1] >= [0 0 1]x + [1] = proper(x) 180.57/61.75 [0 0 1] [1] [0 0 1] [1] 180.57/61.75 180.57/61.75 [1 0 0] [0] [1 0 0] [0] 180.57/61.75 start(ok(x)) = [0 0 1]x + [1] >= [0 0 1]x + [1] = found(x) 180.57/61.75 [0 0 1] [1] [0 0 1] [1] 180.57/61.75 180.57/61.75 [1 0 1] [1] [1 0 1] [1] 180.57/61.75 top(found(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = top(active(x)) 180.57/61.75 [0 0 0] [0] [0 0 0] [0] 180.57/61.75 180.57/61.75 [1 0 2] [1] [1 0 2] [1] 180.57/61.75 top(mark(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = top(check(x)) 180.57/61.75 [0 0 0] [0] [0 0 0] [0] 180.57/61.75 problem: 180.57/61.75 strict: 180.57/61.75 180.57/61.75 weak: 180.57/61.75 f(ok(x)) -> ok(f(x)) 180.57/61.75 active(f(x)) -> f(active(x)) 180.57/61.75 f(found(x)) -> found(f(x)) 180.57/61.75 proper(f(x)) -> f(proper(x)) 180.57/61.75 check(f(x)) -> f(check(x)) 180.57/61.75 f(mark(x)) -> mark(f(x)) 180.57/61.75 top(active(c())) -> top(mark(c())) 180.57/61.75 proper(c()) -> ok(c()) 180.57/61.75 check(x) -> start(match(f(X()),x)) 180.57/61.75 active(f(x)) -> mark(x) 180.57/61.75 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.75 match(X(),x) -> proper(x) 180.57/61.75 start(ok(x)) -> found(x) 180.57/61.75 top(found(x)) -> top(active(x)) 180.57/61.75 top(mark(x)) -> top(check(x)) 180.57/61.75 Qed 180.57/61.75 180.57/61.75 strict: 180.57/61.75 top(mark(x)) -> top(check(x)) 180.57/61.75 weak: 180.57/61.75 f(ok(x)) -> ok(f(x)) 180.57/61.75 active(f(x)) -> f(active(x)) 180.57/61.75 f(found(x)) -> found(f(x)) 180.57/61.75 proper(f(x)) -> f(proper(x)) 180.57/61.75 check(f(x)) -> f(check(x)) 180.57/61.75 f(mark(x)) -> mark(f(x)) 180.57/61.75 top(active(c())) -> top(mark(c())) 180.57/61.75 proper(c()) -> ok(c()) 180.57/61.75 check(x) -> start(match(f(X()),x)) 180.57/61.75 active(f(x)) -> mark(x) 180.57/61.75 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.75 match(X(),x) -> proper(x) 180.57/61.75 start(ok(x)) -> found(x) 180.57/61.75 top(found(x)) -> top(active(x)) 180.57/61.75 Matrix Interpretation Processor: dim=4 180.57/61.75 180.57/61.75 max_matrix: 180.57/61.75 [1 1 1 1] 180.57/61.75 [0 0 1 0] 180.57/61.75 [0 0 0 0] 180.57/61.75 [0 0 0 0] 180.57/61.75 interpretation: 180.57/61.75 [1 0 1 1] [0] 180.57/61.75 [0 0 0 0] [0] 180.57/61.75 [found](x0) = [0 0 0 0]x0 + [0] 180.57/61.75 [0 0 0 0] [1], 180.57/61.75 180.57/61.75 [1 0 0 1] [0] 180.57/61.75 [0 0 1 0] [0] 180.57/61.75 [ok](x0) = [0 0 0 0]x0 + [0] 180.57/61.75 [0 0 0 0] [1], 180.57/61.75 180.57/61.75 [1 0 0 1] [0] 180.57/61.75 [0 0 0 0] [1] 180.57/61.75 [proper](x0) = [0 0 0 0]x0 + [0] 180.57/61.75 [0 0 0 0] [1], 180.57/61.75 180.57/61.75 [1 1 0 0] [0] 180.57/61.75 [0 0 0 0] [0] 180.57/61.75 [start](x0) = [0 0 0 0]x0 + [0] 180.57/61.75 [0 0 0 0] [1], 180.57/61.75 180.57/61.75 [1 0 0 0] [1 0 0 1] [0] 180.57/61.75 [0 0 1 0] [0 0 0 0] [0] 180.57/61.75 [match](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0] 180.57/61.75 [0 0 0 0] [0 0 0 0] [1], 180.57/61.75 180.57/61.75 [0] 180.57/61.75 [0] 180.57/61.75 [X] = [1] 180.57/61.75 [0], 180.57/61.75 180.57/61.75 [1 0 0 1] [0] 180.57/61.75 [0 0 0 0] [0] 180.57/61.75 [check](x0) = [0 0 0 0]x0 + [0] 180.57/61.75 [0 0 0 0] [1], 180.57/61.75 180.57/61.75 [1 1 0 0] 180.57/61.75 [0 0 0 0] 180.57/61.75 [top](x0) = [0 0 0 0]x0 180.57/61.75 [0 0 0 0] , 180.57/61.75 180.57/61.75 [0] 180.57/61.75 [0] 180.57/61.75 [c] = [1] 180.57/61.75 [0], 180.57/61.75 180.57/61.75 [1 0 0 1] [1] 180.57/61.75 [0 0 0 0] [0] 180.57/61.75 [mark](x0) = [0 0 0 0]x0 + [0] 180.57/61.75 [0 0 0 0] [1], 180.57/61.75 180.57/61.75 [1 0 0 1] [0] 180.57/61.75 [0 0 1 0] [0] 180.57/61.75 [active](x0) = [0 0 0 0]x0 + [0] 180.57/61.75 [0 0 0 0] [1], 180.57/61.75 180.57/61.75 [1 0 0 1] [0] 180.57/61.75 [0 0 0 0] [0] 180.57/61.75 [f](x0) = [0 0 0 0]x0 + [0] 180.57/61.75 [0 0 0 0] [1] 180.57/61.75 orientation: 180.57/61.75 [1 0 0 1] [1] [1 0 0 1] 180.57/61.75 [0 0 0 0] [0] [0 0 0 0] 180.57/61.75 top(mark(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x = top(check(x)) 180.57/61.75 [0 0 0 0] [0] [0 0 0 0] 180.57/61.75 180.57/61.75 [1 0 0 1] [1] [1 0 0 1] [1] 180.57/61.75 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.75 f(ok(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = ok(f(x)) 180.57/61.75 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.75 180.57/61.75 [1 0 0 1] [1] [1 0 0 1] [1] 180.57/61.75 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.75 active(f(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = f(active(x)) 180.57/61.75 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.75 180.57/61.75 [1 0 1 1] [1] [1 0 0 1] [1] 180.57/61.75 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.75 f(found(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = found(f(x)) 180.57/61.75 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.75 180.57/61.75 [1 0 0 1] [1] [1 0 0 1] [1] 180.57/61.75 [0 0 0 0] [1] [0 0 0 0] [0] 180.57/61.75 proper(f(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = f(proper(x)) 180.57/61.75 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.75 180.57/61.75 [1 0 0 1] [1] [1 0 0 1] [1] 180.57/61.76 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.76 check(f(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = f(check(x)) 180.57/61.76 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.76 180.57/61.76 [1 0 0 1] [2] [1 0 0 1] [2] 180.57/61.76 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.76 f(mark(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = mark(f(x)) 180.57/61.76 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.76 180.57/61.76 [1] [1] 180.57/61.76 [0] [0] 180.57/61.76 top(active(c())) = [0] >= [0] = top(mark(c())) 180.57/61.76 [0] [0] 180.57/61.76 180.57/61.76 [0] [0] 180.57/61.76 [1] [1] 180.57/61.76 proper(c()) = [0] >= [0] = ok(c()) 180.57/61.76 [1] [1] 180.57/61.76 180.57/61.76 [1 0 0 1] [0] [1 0 0 1] [0] 180.57/61.76 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.76 check(x) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = start(match(f(X()),x)) 180.57/61.76 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.76 180.57/61.76 [1 0 0 1] [1] [1 0 0 1] [1] 180.57/61.76 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.76 active(f(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = mark(x) 180.57/61.76 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.76 180.57/61.76 [1 0 0 1] [1 0 0 1] [1] [1 0 0 0] [1 0 0 1] [1] 180.57/61.76 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 180.57/61.76 match(f(x),f(y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = f(match(x,y)) 180.57/61.76 [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [1] 180.57/61.76 180.57/61.76 [1 0 0 1] [0] [1 0 0 1] [0] 180.57/61.76 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.76 match(X(),x) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = proper(x) 180.57/61.76 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.76 180.57/61.76 [1 0 1 1] [0] [1 0 1 1] [0] 180.57/61.76 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.76 start(ok(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = found(x) 180.57/61.76 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.76 180.57/61.76 [1 0 1 1] [1 0 1 1] 180.57/61.76 [0 0 0 0] [0 0 0 0] 180.57/61.76 top(found(x)) = [0 0 0 0]x >= [0 0 0 0]x = top(active(x)) 180.57/61.76 [0 0 0 0] [0 0 0 0] 180.57/61.76 problem: 180.57/61.76 strict: 180.57/61.76 180.57/61.76 weak: 180.57/61.76 top(mark(x)) -> top(check(x)) 180.57/61.76 f(ok(x)) -> ok(f(x)) 180.57/61.76 active(f(x)) -> f(active(x)) 180.57/61.76 f(found(x)) -> found(f(x)) 180.57/61.76 proper(f(x)) -> f(proper(x)) 180.57/61.76 check(f(x)) -> f(check(x)) 180.57/61.76 f(mark(x)) -> mark(f(x)) 180.57/61.76 top(active(c())) -> top(mark(c())) 180.57/61.76 proper(c()) -> ok(c()) 180.57/61.76 check(x) -> start(match(f(X()),x)) 180.57/61.76 active(f(x)) -> mark(x) 180.57/61.76 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.76 match(X(),x) -> proper(x) 180.57/61.76 start(ok(x)) -> found(x) 180.57/61.76 top(found(x)) -> top(active(x)) 180.57/61.76 Qed 180.57/61.76 180.57/61.76 strict: 180.57/61.76 top(mark(x)) -> top(check(x)) 180.57/61.76 f(ok(x)) -> ok(f(x)) 180.57/61.76 weak: 180.57/61.76 active(f(x)) -> f(active(x)) 180.57/61.76 f(found(x)) -> found(f(x)) 180.57/61.76 proper(f(x)) -> f(proper(x)) 180.57/61.76 check(f(x)) -> f(check(x)) 180.57/61.76 f(mark(x)) -> mark(f(x)) 180.57/61.76 top(active(c())) -> top(mark(c())) 180.57/61.76 proper(c()) -> ok(c()) 180.57/61.76 check(x) -> start(match(f(X()),x)) 180.57/61.76 active(f(x)) -> mark(x) 180.57/61.76 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.76 match(X(),x) -> proper(x) 180.57/61.76 start(ok(x)) -> found(x) 180.57/61.76 top(found(x)) -> top(active(x)) 180.57/61.76 Matrix Interpretation Processor: dim=3 180.57/61.76 180.57/61.76 max_matrix: 180.57/61.76 [1 0 1] 180.57/61.76 [0 0 1] 180.57/61.76 [0 0 1] 180.57/61.76 interpretation: 180.57/61.76 [1 0 1] [0] 180.57/61.76 [found](x0) = [0 0 0]x0 + [0] 180.57/61.76 [0 0 1] [1], 180.57/61.76 180.57/61.76 [1 0 0] 180.57/61.76 [ok](x0) = [0 0 0]x0 180.57/61.76 [0 0 1] , 180.57/61.76 180.57/61.76 [1 0 0] 180.57/61.76 [proper](x0) = [0 0 0]x0 180.57/61.76 [0 0 1] , 180.57/61.76 180.57/61.76 [1 0 1] [0] 180.57/61.76 [start](x0) = [0 0 0]x0 + [0] 180.57/61.76 [0 0 1] [1], 180.57/61.76 180.57/61.76 [1 0 0] [1 0 0] [0] 180.57/61.76 [match](x0, x1) = [0 0 1]x0 + [0 0 0]x1 + [1] 180.57/61.76 [0 0 0] [0 0 1] [0], 180.57/61.76 180.57/61.76 [0] 180.57/61.76 [X] = [0] 180.57/61.76 [0], 180.57/61.76 180.57/61.76 [1 0 1] [0] 180.57/61.76 [check](x0) = [0 0 1]x0 + [1] 180.57/61.76 [0 0 1] [1], 180.57/61.76 180.57/61.76 [1 0 0] [0] 180.57/61.76 [top](x0) = [0 0 0]x0 + [1] 180.57/61.76 [0 0 0] [1], 180.57/61.76 180.57/61.76 [0] 180.57/61.76 [c] = [0] 180.57/61.76 [0], 180.57/61.76 180.57/61.76 [1 0 1] [0] 180.57/61.76 [mark](x0) = [0 0 0]x0 + [0] 180.57/61.76 [0 0 1] [1], 180.57/61.76 180.57/61.76 [1 0 1] 180.57/61.76 [active](x0) = [0 0 0]x0 180.57/61.76 [0 0 1] , 180.57/61.76 180.57/61.76 [1 0 1] [0] 180.57/61.76 [f](x0) = [0 0 0]x0 + [0] 180.57/61.76 [0 0 1] [1] 180.57/61.76 orientation: 180.57/61.76 [1 0 2] [1] [1 0 2] [0] 180.57/61.76 active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(active(x)) 180.57/61.76 [0 0 1] [1] [0 0 1] [1] 180.57/61.76 180.57/61.76 [1 0 2] [1] [1 0 2] [1] 180.57/61.76 f(found(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = found(f(x)) 180.57/61.76 [0 0 1] [2] [0 0 1] [2] 180.57/61.76 180.57/61.76 [1 0 1] [0] [1 0 1] [0] 180.57/61.76 proper(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(proper(x)) 180.57/61.76 [0 0 1] [1] [0 0 1] [1] 180.57/61.76 180.57/61.76 [1 0 2] [1] [1 0 2] [1] 180.57/61.76 check(f(x)) = [0 0 1]x + [2] >= [0 0 0]x + [0] = f(check(x)) 180.57/61.76 [0 0 1] [2] [0 0 1] [2] 180.57/61.76 180.57/61.76 [1 0 2] [1] [1 0 2] [1] 180.57/61.76 f(mark(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(f(x)) 180.57/61.76 [0 0 1] [2] [0 0 1] [2] 180.57/61.76 180.57/61.76 [0] [0] 180.57/61.76 top(active(c())) = [1] >= [1] = top(mark(c())) 180.57/61.76 [1] [1] 180.57/61.76 180.57/61.76 [0] [0] 180.57/61.76 proper(c()) = [0] >= [0] = ok(c()) 180.57/61.76 [0] [0] 180.57/61.76 180.57/61.76 [1 0 1] [0] [1 0 1] [0] 180.57/61.76 check(x) = [0 0 1]x + [1] >= [0 0 0]x + [0] = start(match(f(X()),x)) 180.57/61.76 [0 0 1] [1] [0 0 1] [1] 180.57/61.76 180.57/61.76 [1 0 2] [1] [1 0 1] [0] 180.57/61.77 active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(x) 180.57/61.77 [0 0 1] [1] [0 0 1] [1] 180.57/61.77 180.57/61.77 [1 0 1] [1 0 1] [0] [1 0 0] [1 0 1] [0] 180.57/61.77 match(f(x),f(y)) = [0 0 1]x + [0 0 0]y + [2] >= [0 0 0]x + [0 0 0]y + [0] = f(match(x,y)) 180.57/61.77 [0 0 0] [0 0 1] [1] [0 0 0] [0 0 1] [1] 180.57/61.77 180.57/61.77 [1 0 0] [0] [1 0 0] 180.57/61.77 match(X(),x) = [0 0 0]x + [1] >= [0 0 0]x = proper(x) 180.57/61.77 [0 0 1] [0] [0 0 1] 180.57/61.77 180.57/61.77 [1 0 1] [0] [1 0 1] [0] 180.57/61.77 start(ok(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = found(x) 180.57/61.77 [0 0 1] [1] [0 0 1] [1] 180.57/61.77 180.57/61.77 [1 0 1] [0] [1 0 1] [0] 180.57/61.77 top(found(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = top(active(x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [1] 180.57/61.77 180.57/61.77 [1 0 1] [0] [1 0 1] [0] 180.57/61.77 top(mark(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = top(check(x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [1] 180.57/61.77 180.57/61.77 [1 0 1] [0] [1 0 1] [0] 180.57/61.77 f(ok(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = ok(f(x)) 180.57/61.77 [0 0 1] [1] [0 0 1] [1] 180.57/61.77 problem: 180.57/61.77 strict: 180.57/61.77 180.57/61.77 weak: 180.57/61.77 active(f(x)) -> f(active(x)) 180.57/61.77 f(found(x)) -> found(f(x)) 180.57/61.77 proper(f(x)) -> f(proper(x)) 180.57/61.77 check(f(x)) -> f(check(x)) 180.57/61.77 f(mark(x)) -> mark(f(x)) 180.57/61.77 top(active(c())) -> top(mark(c())) 180.57/61.77 proper(c()) -> ok(c()) 180.57/61.77 check(x) -> start(match(f(X()),x)) 180.57/61.77 active(f(x)) -> mark(x) 180.57/61.77 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.77 match(X(),x) -> proper(x) 180.57/61.77 start(ok(x)) -> found(x) 180.57/61.77 top(found(x)) -> top(active(x)) 180.57/61.77 top(mark(x)) -> top(check(x)) 180.57/61.77 f(ok(x)) -> ok(f(x)) 180.57/61.77 Qed 180.57/61.77 180.57/61.77 strict: 180.57/61.77 top(mark(x)) -> top(check(x)) 180.57/61.77 f(ok(x)) -> ok(f(x)) 180.57/61.77 active(f(x)) -> f(active(x)) 180.57/61.77 weak: 180.57/61.77 f(found(x)) -> found(f(x)) 180.57/61.77 proper(f(x)) -> f(proper(x)) 180.57/61.77 check(f(x)) -> f(check(x)) 180.57/61.77 f(mark(x)) -> mark(f(x)) 180.57/61.77 top(active(c())) -> top(mark(c())) 180.57/61.77 proper(c()) -> ok(c()) 180.57/61.77 check(x) -> start(match(f(X()),x)) 180.57/61.77 active(f(x)) -> mark(x) 180.57/61.77 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.77 match(X(),x) -> proper(x) 180.57/61.77 start(ok(x)) -> found(x) 180.57/61.77 top(found(x)) -> top(active(x)) 180.57/61.77 Matrix Interpretation Processor: dim=3 180.57/61.77 180.57/61.77 max_matrix: 180.57/61.77 [1 1 0] 180.57/61.77 [0 1 1] 180.57/61.77 [0 0 0] 180.57/61.77 interpretation: 180.57/61.77 [1 0 0] [0] 180.57/61.77 [found](x0) = [0 1 0]x0 + [1] 180.57/61.77 [0 0 0] [0], 180.57/61.77 180.57/61.77 [1 0 0] [0] 180.57/61.77 [ok](x0) = [0 1 0]x0 + [0] 180.57/61.77 [0 0 0] [1], 180.57/61.77 180.57/61.77 [1 0 0] [0] 180.57/61.77 [proper](x0) = [0 1 0]x0 + [0] 180.57/61.77 [0 0 0] [1], 180.57/61.77 180.57/61.77 [1 1 0] 180.57/61.77 [start](x0) = [0 1 1]x0 180.57/61.77 [0 0 0] , 180.57/61.77 180.57/61.77 [1 0 0] [1 0 0] [0] 180.57/61.77 [match](x0, x1) = [0 0 0]x0 + [0 1 0]x1 + [0] 180.57/61.77 [0 0 0] [0 0 0] [1], 180.57/61.77 180.57/61.77 [0] 180.57/61.77 [X] = [0] 180.57/61.77 [0], 180.57/61.77 180.57/61.77 [1 1 0] [0] 180.57/61.77 [check](x0) = [0 1 0]x0 + [1] 180.57/61.77 [0 0 0] [1], 180.57/61.77 180.57/61.77 [1 0 0] [0] 180.57/61.77 [top](x0) = [0 0 0]x0 + [1] 180.57/61.77 [0 0 0] [0], 180.57/61.77 180.57/61.77 [0] 180.57/61.77 [c] = [0] 180.57/61.77 [0], 180.57/61.77 180.57/61.77 [1 1 0] [0] 180.57/61.77 [mark](x0) = [0 1 0]x0 + [1] 180.57/61.77 [0 0 0] [0], 180.57/61.77 180.57/61.77 [1 0 0] [0] 180.57/61.77 [active](x0) = [0 1 0]x0 + [0] 180.57/61.77 [0 0 0] [1], 180.57/61.77 180.57/61.77 [1 1 0] [0] 180.57/61.77 [f](x0) = [0 1 0]x0 + [1] 180.57/61.77 [0 0 0] [1] 180.57/61.77 orientation: 180.57/61.77 [1 1 0] [1] [1 1 0] [0] 180.57/61.77 f(found(x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = found(f(x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [0] 180.57/61.77 180.57/61.77 [1 1 0] [0] [1 1 0] [0] 180.57/61.77 proper(f(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = f(proper(x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [1] 180.57/61.77 180.57/61.77 [1 2 0] [1] [1 2 0] [1] 180.57/61.77 check(f(x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = f(check(x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [1] 180.57/61.77 180.57/61.77 [1 2 0] [1] [1 2 0] [1] 180.57/61.77 f(mark(x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = mark(f(x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [0] 180.57/61.77 180.57/61.77 [0] [0] 180.57/61.77 top(active(c())) = [1] >= [1] = top(mark(c())) 180.57/61.77 [0] [0] 180.57/61.77 180.57/61.77 [0] [0] 180.57/61.77 proper(c()) = [0] >= [0] = ok(c()) 180.57/61.77 [1] [1] 180.57/61.77 180.57/61.77 [1 1 0] [0] [1 1 0] [0] 180.57/61.77 check(x) = [0 1 0]x + [1] >= [0 1 0]x + [1] = start(match(f(X()),x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [0] 180.57/61.77 180.57/61.77 [1 1 0] [0] [1 1 0] [0] 180.57/61.77 active(f(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = mark(x) 180.57/61.77 [0 0 0] [1] [0 0 0] [0] 180.57/61.77 180.57/61.77 [1 1 0] [1 1 0] [0] [1 0 0] [1 1 0] [0] 180.57/61.77 match(f(x),f(y)) = [0 0 0]x + [0 1 0]y + [1] >= [0 0 0]x + [0 1 0]y + [1] = f(match(x,y)) 180.57/61.77 [0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] [1] 180.57/61.77 180.57/61.77 [1 0 0] [0] [1 0 0] [0] 180.57/61.77 match(X(),x) = [0 1 0]x + [0] >= [0 1 0]x + [0] = proper(x) 180.57/61.77 [0 0 0] [1] [0 0 0] [1] 180.57/61.77 180.57/61.77 [1 1 0] [0] [1 0 0] [0] 180.57/61.77 start(ok(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = found(x) 180.57/61.77 [0 0 0] [0] [0 0 0] [0] 180.57/61.77 180.57/61.77 [1 0 0] [0] [1 0 0] [0] 180.57/61.77 top(found(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = top(active(x)) 180.57/61.77 [0 0 0] [0] [0 0 0] [0] 180.57/61.77 180.57/61.77 [1 1 0] [0] [1 1 0] [0] 180.57/61.77 top(mark(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = top(check(x)) 180.57/61.77 [0 0 0] [0] [0 0 0] [0] 180.57/61.77 180.57/61.77 [1 1 0] [0] [1 1 0] [0] 180.57/61.77 f(ok(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = ok(f(x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [1] 180.57/61.77 180.57/61.77 [1 1 0] [0] [1 1 0] [0] 180.57/61.77 active(f(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = f(active(x)) 180.57/61.77 [0 0 0] [1] [0 0 0] [1] 180.57/61.78 problem: 180.57/61.78 strict: 180.57/61.78 180.57/61.78 weak: 180.57/61.78 f(found(x)) -> found(f(x)) 180.57/61.78 proper(f(x)) -> f(proper(x)) 180.57/61.78 check(f(x)) -> f(check(x)) 180.57/61.78 f(mark(x)) -> mark(f(x)) 180.57/61.78 top(active(c())) -> top(mark(c())) 180.57/61.78 proper(c()) -> ok(c()) 180.57/61.78 check(x) -> start(match(f(X()),x)) 180.57/61.78 active(f(x)) -> mark(x) 180.57/61.78 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.78 match(X(),x) -> proper(x) 180.57/61.78 start(ok(x)) -> found(x) 180.57/61.78 top(found(x)) -> top(active(x)) 180.57/61.78 top(mark(x)) -> top(check(x)) 180.57/61.78 f(ok(x)) -> ok(f(x)) 180.57/61.78 active(f(x)) -> f(active(x)) 180.57/61.78 Qed 180.57/61.78 180.57/61.78 strict: 180.57/61.78 top(mark(x)) -> top(check(x)) 180.57/61.78 f(ok(x)) -> ok(f(x)) 180.57/61.78 f(found(x)) -> found(f(x)) 180.57/61.78 active(f(x)) -> f(active(x)) 180.57/61.78 weak: 180.57/61.78 proper(f(x)) -> f(proper(x)) 180.57/61.78 check(f(x)) -> f(check(x)) 180.57/61.78 f(mark(x)) -> mark(f(x)) 180.57/61.78 top(active(c())) -> top(mark(c())) 180.57/61.78 proper(c()) -> ok(c()) 180.57/61.78 check(x) -> start(match(f(X()),x)) 180.57/61.78 active(f(x)) -> mark(x) 180.57/61.78 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.78 match(X(),x) -> proper(x) 180.57/61.78 start(ok(x)) -> found(x) 180.57/61.78 top(found(x)) -> top(active(x)) 180.57/61.78 Matrix Interpretation Processor: dim=4 180.57/61.78 180.57/61.78 max_matrix: 180.57/61.78 [1 1 0 0] 180.57/61.78 [0 1 0 0] 180.57/61.78 [0 0 0 1] 180.57/61.78 [0 0 0 0] 180.57/61.78 interpretation: 180.57/61.78 [1 0 0 0] 180.57/61.78 [0 1 0 0] 180.57/61.78 [found](x0) = [0 0 0 0]x0 180.57/61.78 [0 0 0 0] , 180.57/61.78 180.57/61.78 [1 0 0 0] 180.57/61.78 [0 1 0 0] 180.57/61.78 [ok](x0) = [0 0 0 0]x0 180.57/61.78 [0 0 0 0] , 180.57/61.78 180.57/61.78 [1 1 0 0] 180.57/61.78 [0 1 0 0] 180.57/61.78 [proper](x0) = [0 0 0 0]x0 180.57/61.78 [0 0 0 0] , 180.57/61.78 180.57/61.78 [1 0 0 0] [0] 180.57/61.78 [0 1 0 0] [0] 180.57/61.78 [start](x0) = [0 0 0 0]x0 + [0] 180.57/61.78 [0 0 0 0] [1], 180.57/61.78 180.57/61.78 [1 0 0 0] [1 1 0 0] [0] 180.57/61.78 [0 0 0 0] [0 1 0 0] [0] 180.57/61.78 [match](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [1] 180.57/61.78 [0 0 0 0] [0 0 0 0] [1], 180.57/61.78 180.57/61.78 [0] 180.57/61.78 [0] 180.57/61.78 [X] = [0] 180.57/61.78 [0], 180.57/61.78 180.57/61.78 [1 1 0 0] [0] 180.57/61.78 [0 1 0 0] [1] 180.57/61.78 [check](x0) = [0 0 0 1]x0 + [0] 180.57/61.78 [0 0 0 0] [1], 180.57/61.78 180.57/61.78 [1 0 0 0] 180.57/61.78 [0 0 0 0] 180.57/61.78 [top](x0) = [0 0 0 0]x0 180.57/61.78 [0 0 0 0] , 180.57/61.78 180.57/61.78 [0] 180.57/61.78 [0] 180.57/61.78 [c] = [0] 180.57/61.78 [0], 180.57/61.78 180.57/61.78 [1 1 0 0] [0] 180.57/61.78 [0 1 0 0] [1] 180.57/61.78 [mark](x0) = [0 0 0 0]x0 + [0] 180.57/61.78 [0 0 0 0] [0], 180.57/61.78 180.57/61.78 [1 0 0 0] 180.57/61.78 [0 1 0 0] 180.57/61.78 [active](x0) = [0 0 0 0]x0 180.57/61.78 [0 0 0 0] , 180.57/61.78 180.57/61.78 [1 1 0 0] [0] 180.57/61.78 [0 1 0 0] [1] 180.57/61.78 [f](x0) = [0 0 0 0]x0 + [0] 180.57/61.78 [0 0 0 0] [0] 180.57/61.78 orientation: 180.57/61.78 [1 2 0 0] [1] [1 2 0 0] [0] 180.57/61.78 [0 1 0 0] [1] [0 1 0 0] [1] 180.57/61.78 proper(f(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = f(proper(x)) 180.57/61.78 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.78 180.57/61.78 [1 2 0 0] [1] [1 2 0 0] [1] 180.57/61.78 [0 1 0 0] [2] [0 1 0 0] [2] 180.57/61.78 check(f(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = f(check(x)) 180.57/61.78 [0 0 0 0] [1] [0 0 0 0] [0] 180.57/61.79 180.57/61.79 [1 2 0 0] [1] [1 2 0 0] [1] 180.57/61.79 [0 1 0 0] [2] [0 1 0 0] [2] 180.57/61.79 f(mark(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = mark(f(x)) 180.57/61.79 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.79 180.57/61.79 [0] [0] 180.57/61.79 [0] [0] 180.57/61.79 top(active(c())) = [0] >= [0] = top(mark(c())) 180.57/61.79 [0] [0] 180.57/61.79 180.57/61.79 [0] [0] 180.57/61.79 [0] [0] 180.57/61.79 proper(c()) = [0] >= [0] = ok(c()) 180.57/61.79 [0] [0] 180.57/61.79 180.57/61.79 [1 1 0 0] [0] [1 1 0 0] [0] 180.57/61.79 [0 1 0 0] [1] [0 1 0 0] [0] 180.57/61.79 check(x) = [0 0 0 1]x + [0] >= [0 0 0 0]x + [0] = start(match(f(X()),x)) 180.57/61.79 [0 0 0 0] [1] [0 0 0 0] [1] 180.57/61.79 180.57/61.79 [1 1 0 0] [0] [1 1 0 0] [0] 180.57/61.79 [0 1 0 0] [1] [0 1 0 0] [1] 180.57/61.79 active(f(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = mark(x) 180.57/61.79 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.79 180.57/61.79 [1 1 0 0] [1 2 0 0] [1] [1 0 0 0] [1 2 0 0] [0] 180.57/61.79 [0 0 0 0] [0 1 0 0] [1] [0 0 0 0] [0 1 0 0] [1] 180.57/61.79 match(f(x),f(y)) = [0 0 0 0]x + [0 0 0 0]y + [1] >= [0 0 0 0]x + [0 0 0 0]y + [0] = f(match(x,y)) 180.57/61.79 [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0] 180.57/61.79 180.57/61.79 [1 1 0 0] [0] [1 1 0 0] 180.57/61.79 [0 1 0 0] [0] [0 1 0 0] 180.57/61.79 match(X(),x) = [0 0 0 0]x + [1] >= [0 0 0 0]x = proper(x) 180.57/61.79 [0 0 0 0] [1] [0 0 0 0] 180.57/61.79 180.57/61.79 [1 0 0 0] [0] [1 0 0 0] 180.57/61.79 [0 1 0 0] [0] [0 1 0 0] 180.57/61.79 start(ok(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x = found(x) 180.57/61.79 [0 0 0 0] [1] [0 0 0 0] 180.57/61.79 180.57/61.79 [1 0 0 0] [1 0 0 0] 180.57/61.79 [0 0 0 0] [0 0 0 0] 180.57/61.79 top(found(x)) = [0 0 0 0]x >= [0 0 0 0]x = top(active(x)) 180.57/61.79 [0 0 0 0] [0 0 0 0] 180.57/61.79 180.57/61.79 [1 1 0 0] [1 1 0 0] 180.57/61.79 [0 0 0 0] [0 0 0 0] 180.57/61.79 top(mark(x)) = [0 0 0 0]x >= [0 0 0 0]x = top(check(x)) 180.57/61.79 [0 0 0 0] [0 0 0 0] 180.57/61.79 180.57/61.79 [1 1 0 0] [0] [1 1 0 0] [0] 180.57/61.79 [0 1 0 0] [1] [0 1 0 0] [1] 180.57/61.79 f(ok(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = ok(f(x)) 180.57/61.79 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.79 180.57/61.79 [1 1 0 0] [0] [1 1 0 0] [0] 180.57/61.79 [0 1 0 0] [1] [0 1 0 0] [1] 180.57/61.79 f(found(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = found(f(x)) 180.57/61.79 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.79 180.57/61.79 [1 1 0 0] [0] [1 1 0 0] [0] 180.57/61.79 [0 1 0 0] [1] [0 1 0 0] [1] 180.57/61.79 active(f(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = f(active(x)) 180.57/61.79 [0 0 0 0] [0] [0 0 0 0] [0] 180.57/61.79 problem: 180.57/61.79 strict: 180.57/61.79 180.57/61.79 weak: 180.57/61.79 proper(f(x)) -> f(proper(x)) 180.57/61.79 check(f(x)) -> f(check(x)) 180.57/61.79 f(mark(x)) -> mark(f(x)) 180.57/61.79 top(active(c())) -> top(mark(c())) 180.57/61.79 proper(c()) -> ok(c()) 180.57/61.79 check(x) -> start(match(f(X()),x)) 180.57/61.79 active(f(x)) -> mark(x) 180.57/61.79 match(f(x),f(y)) -> f(match(x,y)) 180.57/61.79 match(X(),x) -> proper(x) 180.57/61.79 start(ok(x)) -> found(x) 180.57/61.79 top(found(x)) -> top(active(x)) 180.57/61.79 top(mark(x)) -> top(check(x)) 180.57/61.79 f(ok(x)) -> ok(f(x)) 180.57/61.79 f(found(x)) -> found(f(x)) 180.57/61.79 active(f(x)) -> f(active(x)) 180.57/61.79 Qed 180.57/61.79 EOF