YES(O(1),O(n^2)) 212.00/60.08 YES(O(1),O(n^2)) 212.00/60.08 212.00/60.08 We are left with following problem, upon which TcT provides the 212.00/60.08 certificate YES(O(1),O(n^2)). 212.00/60.08 212.00/60.08 Strict Trs: 212.00/60.08 { active(f(x)) -> f(active(x)) 212.00/60.08 , active(f(x)) -> mark(x) 212.00/60.08 , f(mark(x)) -> mark(f(x)) 212.00/60.08 , f(ok(x)) -> ok(f(x)) 212.00/60.08 , f(found(x)) -> found(f(x)) 212.00/60.08 , top(active(c())) -> top(mark(c())) 212.00/60.08 , top(mark(x)) -> top(check(x)) 212.00/60.08 , top(found(x)) -> top(active(x)) 212.00/60.08 , check(x) -> start(match(f(X()), x)) 212.00/60.08 , check(f(x)) -> f(check(x)) 212.00/60.08 , start(ok(x)) -> found(x) 212.00/60.08 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.08 , match(X(), x) -> proper(x) 212.00/60.08 , proper(f(x)) -> f(proper(x)) 212.00/60.08 , proper(c()) -> ok(c()) } 212.00/60.08 Obligation: 212.00/60.08 derivational complexity 212.00/60.08 Answer: 212.00/60.08 YES(O(1),O(n^2)) 212.00/60.08 212.00/60.08 The weightgap principle applies (using the following nonconstant 212.00/60.08 growth matrix-interpretation) 212.00/60.08 212.00/60.08 TcT has computed the following triangular matrix interpretation. 212.00/60.08 Note that the diagonal of the component-wise maxima of 212.00/60.08 interpretation-entries contains no more than 1 non-zero entries. 212.00/60.08 212.00/60.08 [active](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [f](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [mark](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [top](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [c] = [0] 212.00/60.08 212.00/60.08 [check](x1) = [1] x1 + [1] 212.00/60.08 212.00/60.08 [start](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [match](x1, x2) = [1] x1 + [1] x2 + [0] 212.00/60.08 212.00/60.08 [X] = [0] 212.00/60.08 212.00/60.08 [proper](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [ok](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [found](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 The order satisfies the following ordering constraints: 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(active(x))] 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(x)] 212.00/60.08 212.00/60.08 [f(mark(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(f(x))] 212.00/60.08 212.00/60.08 [f(ok(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [ok(f(x))] 212.00/60.08 212.00/60.08 [f(found(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [found(f(x))] 212.00/60.08 212.00/60.08 [top(active(c()))] = [0] 212.00/60.08 >= [0] 212.00/60.08 = [top(mark(c()))] 212.00/60.08 212.00/60.08 [top(mark(x))] = [1] x + [0] 212.00/60.08 ? [1] x + [1] 212.00/60.08 = [top(check(x))] 212.00/60.08 212.00/60.08 [top(found(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [top(active(x))] 212.00/60.08 212.00/60.08 [check(x)] = [1] x + [1] 212.00/60.08 > [1] x + [0] 212.00/60.08 = [start(match(f(X()), x))] 212.00/60.08 212.00/60.08 [check(f(x))] = [1] x + [1] 212.00/60.08 >= [1] x + [1] 212.00/60.08 = [f(check(x))] 212.00/60.08 212.00/60.08 [start(ok(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [found(x)] 212.00/60.08 212.00/60.08 [match(f(x), f(y))] = [1] x + [1] y + [0] 212.00/60.08 >= [1] x + [1] y + [0] 212.00/60.08 = [f(match(x, y))] 212.00/60.08 212.00/60.08 [match(X(), x)] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [proper(x)] 212.00/60.08 212.00/60.08 [proper(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(proper(x))] 212.00/60.08 212.00/60.08 [proper(c())] = [0] 212.00/60.08 >= [0] 212.00/60.08 = [ok(c())] 212.00/60.08 212.00/60.08 212.00/60.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.00/60.08 212.00/60.08 We are left with following problem, upon which TcT provides the 212.00/60.08 certificate YES(O(1),O(n^2)). 212.00/60.08 212.00/60.08 Strict Trs: 212.00/60.08 { active(f(x)) -> f(active(x)) 212.00/60.08 , active(f(x)) -> mark(x) 212.00/60.08 , f(mark(x)) -> mark(f(x)) 212.00/60.08 , f(ok(x)) -> ok(f(x)) 212.00/60.08 , f(found(x)) -> found(f(x)) 212.00/60.08 , top(active(c())) -> top(mark(c())) 212.00/60.08 , top(mark(x)) -> top(check(x)) 212.00/60.08 , top(found(x)) -> top(active(x)) 212.00/60.08 , check(f(x)) -> f(check(x)) 212.00/60.08 , start(ok(x)) -> found(x) 212.00/60.08 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.08 , match(X(), x) -> proper(x) 212.00/60.08 , proper(f(x)) -> f(proper(x)) 212.00/60.08 , proper(c()) -> ok(c()) } 212.00/60.08 Weak Trs: { check(x) -> start(match(f(X()), x)) } 212.00/60.08 Obligation: 212.00/60.08 derivational complexity 212.00/60.08 Answer: 212.00/60.08 YES(O(1),O(n^2)) 212.00/60.08 212.00/60.08 The weightgap principle applies (using the following nonconstant 212.00/60.08 growth matrix-interpretation) 212.00/60.08 212.00/60.08 TcT has computed the following triangular matrix interpretation. 212.00/60.08 Note that the diagonal of the component-wise maxima of 212.00/60.08 interpretation-entries contains no more than 1 non-zero entries. 212.00/60.08 212.00/60.08 [active](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [f](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [mark](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [top](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [c] = [0] 212.00/60.08 212.00/60.08 [check](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [start](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [match](x1, x2) = [1] x1 + [1] x2 + [0] 212.00/60.08 212.00/60.08 [X] = [0] 212.00/60.08 212.00/60.08 [proper](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [ok](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [found](x1) = [1] x1 + [1] 212.00/60.08 212.00/60.08 The order satisfies the following ordering constraints: 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(active(x))] 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(x)] 212.00/60.08 212.00/60.08 [f(mark(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(f(x))] 212.00/60.08 212.00/60.08 [f(ok(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [ok(f(x))] 212.00/60.08 212.00/60.08 [f(found(x))] = [1] x + [1] 212.00/60.08 >= [1] x + [1] 212.00/60.08 = [found(f(x))] 212.00/60.08 212.00/60.08 [top(active(c()))] = [0] 212.00/60.08 >= [0] 212.00/60.08 = [top(mark(c()))] 212.00/60.08 212.00/60.08 [top(mark(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [top(check(x))] 212.00/60.08 212.00/60.08 [top(found(x))] = [1] x + [1] 212.00/60.08 > [1] x + [0] 212.00/60.08 = [top(active(x))] 212.00/60.08 212.00/60.08 [check(x)] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [start(match(f(X()), x))] 212.00/60.08 212.00/60.08 [check(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(check(x))] 212.00/60.08 212.00/60.08 [start(ok(x))] = [1] x + [0] 212.00/60.08 ? [1] x + [1] 212.00/60.08 = [found(x)] 212.00/60.08 212.00/60.08 [match(f(x), f(y))] = [1] x + [1] y + [0] 212.00/60.08 >= [1] x + [1] y + [0] 212.00/60.08 = [f(match(x, y))] 212.00/60.08 212.00/60.08 [match(X(), x)] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [proper(x)] 212.00/60.08 212.00/60.08 [proper(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(proper(x))] 212.00/60.08 212.00/60.08 [proper(c())] = [0] 212.00/60.08 >= [0] 212.00/60.08 = [ok(c())] 212.00/60.08 212.00/60.08 212.00/60.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.00/60.08 212.00/60.08 We are left with following problem, upon which TcT provides the 212.00/60.08 certificate YES(O(1),O(n^2)). 212.00/60.08 212.00/60.08 Strict Trs: 212.00/60.08 { active(f(x)) -> f(active(x)) 212.00/60.08 , active(f(x)) -> mark(x) 212.00/60.08 , f(mark(x)) -> mark(f(x)) 212.00/60.08 , f(ok(x)) -> ok(f(x)) 212.00/60.08 , f(found(x)) -> found(f(x)) 212.00/60.08 , top(active(c())) -> top(mark(c())) 212.00/60.08 , top(mark(x)) -> top(check(x)) 212.00/60.08 , check(f(x)) -> f(check(x)) 212.00/60.08 , start(ok(x)) -> found(x) 212.00/60.08 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.08 , match(X(), x) -> proper(x) 212.00/60.08 , proper(f(x)) -> f(proper(x)) 212.00/60.08 , proper(c()) -> ok(c()) } 212.00/60.08 Weak Trs: 212.00/60.08 { top(found(x)) -> top(active(x)) 212.00/60.08 , check(x) -> start(match(f(X()), x)) } 212.00/60.08 Obligation: 212.00/60.08 derivational complexity 212.00/60.08 Answer: 212.00/60.08 YES(O(1),O(n^2)) 212.00/60.08 212.00/60.08 The weightgap principle applies (using the following nonconstant 212.00/60.08 growth matrix-interpretation) 212.00/60.08 212.00/60.08 TcT has computed the following triangular matrix interpretation. 212.00/60.08 Note that the diagonal of the component-wise maxima of 212.00/60.08 interpretation-entries contains no more than 1 non-zero entries. 212.00/60.08 212.00/60.08 [active](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [f](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [mark](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [top](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [c] = [0] 212.00/60.08 212.00/60.08 [check](x1) = [1] x1 + [1] 212.00/60.08 212.00/60.08 [start](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [match](x1, x2) = [1] x1 + [1] x2 + [0] 212.00/60.08 212.00/60.08 [X] = [1] 212.00/60.08 212.00/60.08 [proper](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [ok](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [found](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 The order satisfies the following ordering constraints: 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(active(x))] 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(x)] 212.00/60.08 212.00/60.08 [f(mark(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(f(x))] 212.00/60.08 212.00/60.08 [f(ok(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [ok(f(x))] 212.00/60.08 212.00/60.08 [f(found(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [found(f(x))] 212.00/60.08 212.00/60.08 [top(active(c()))] = [0] 212.00/60.08 >= [0] 212.00/60.08 = [top(mark(c()))] 212.00/60.08 212.00/60.08 [top(mark(x))] = [1] x + [0] 212.00/60.08 ? [1] x + [1] 212.00/60.08 = [top(check(x))] 212.00/60.08 212.00/60.08 [top(found(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [top(active(x))] 212.00/60.08 212.00/60.08 [check(x)] = [1] x + [1] 212.00/60.08 >= [1] x + [1] 212.00/60.08 = [start(match(f(X()), x))] 212.00/60.08 212.00/60.08 [check(f(x))] = [1] x + [1] 212.00/60.08 >= [1] x + [1] 212.00/60.08 = [f(check(x))] 212.00/60.08 212.00/60.08 [start(ok(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [found(x)] 212.00/60.08 212.00/60.08 [match(f(x), f(y))] = [1] x + [1] y + [0] 212.00/60.08 >= [1] x + [1] y + [0] 212.00/60.08 = [f(match(x, y))] 212.00/60.08 212.00/60.08 [match(X(), x)] = [1] x + [1] 212.00/60.08 > [1] x + [0] 212.00/60.08 = [proper(x)] 212.00/60.08 212.00/60.08 [proper(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(proper(x))] 212.00/60.08 212.00/60.08 [proper(c())] = [0] 212.00/60.08 >= [0] 212.00/60.08 = [ok(c())] 212.00/60.08 212.00/60.08 212.00/60.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.00/60.08 212.00/60.08 We are left with following problem, upon which TcT provides the 212.00/60.08 certificate YES(O(1),O(n^2)). 212.00/60.08 212.00/60.08 Strict Trs: 212.00/60.08 { active(f(x)) -> f(active(x)) 212.00/60.08 , active(f(x)) -> mark(x) 212.00/60.08 , f(mark(x)) -> mark(f(x)) 212.00/60.08 , f(ok(x)) -> ok(f(x)) 212.00/60.08 , f(found(x)) -> found(f(x)) 212.00/60.08 , top(active(c())) -> top(mark(c())) 212.00/60.08 , top(mark(x)) -> top(check(x)) 212.00/60.08 , check(f(x)) -> f(check(x)) 212.00/60.08 , start(ok(x)) -> found(x) 212.00/60.08 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.08 , proper(f(x)) -> f(proper(x)) 212.00/60.08 , proper(c()) -> ok(c()) } 212.00/60.08 Weak Trs: 212.00/60.08 { top(found(x)) -> top(active(x)) 212.00/60.08 , check(x) -> start(match(f(X()), x)) 212.00/60.08 , match(X(), x) -> proper(x) } 212.00/60.08 Obligation: 212.00/60.08 derivational complexity 212.00/60.08 Answer: 212.00/60.08 YES(O(1),O(n^2)) 212.00/60.08 212.00/60.08 The weightgap principle applies (using the following nonconstant 212.00/60.08 growth matrix-interpretation) 212.00/60.08 212.00/60.08 TcT has computed the following triangular matrix interpretation. 212.00/60.08 Note that the diagonal of the component-wise maxima of 212.00/60.08 interpretation-entries contains no more than 1 non-zero entries. 212.00/60.08 212.00/60.08 [active](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [f](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [mark](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [top](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [c] = [0] 212.00/60.08 212.00/60.08 [check](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [start](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [match](x1, x2) = [1] x1 + [1] x2 + [0] 212.00/60.08 212.00/60.08 [X] = [0] 212.00/60.08 212.00/60.08 [proper](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [ok](x1) = [1] x1 + [1] 212.00/60.08 212.00/60.08 [found](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 The order satisfies the following ordering constraints: 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(active(x))] 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(x)] 212.00/60.08 212.00/60.08 [f(mark(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(f(x))] 212.00/60.08 212.00/60.08 [f(ok(x))] = [1] x + [1] 212.00/60.08 >= [1] x + [1] 212.00/60.08 = [ok(f(x))] 212.00/60.08 212.00/60.08 [f(found(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [found(f(x))] 212.00/60.08 212.00/60.08 [top(active(c()))] = [0] 212.00/60.08 >= [0] 212.00/60.08 = [top(mark(c()))] 212.00/60.08 212.00/60.08 [top(mark(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [top(check(x))] 212.00/60.08 212.00/60.08 [top(found(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [top(active(x))] 212.00/60.08 212.00/60.08 [check(x)] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [start(match(f(X()), x))] 212.00/60.08 212.00/60.08 [check(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(check(x))] 212.00/60.08 212.00/60.08 [start(ok(x))] = [1] x + [1] 212.00/60.08 > [1] x + [0] 212.00/60.08 = [found(x)] 212.00/60.08 212.00/60.08 [match(f(x), f(y))] = [1] x + [1] y + [0] 212.00/60.08 >= [1] x + [1] y + [0] 212.00/60.08 = [f(match(x, y))] 212.00/60.08 212.00/60.08 [match(X(), x)] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [proper(x)] 212.00/60.08 212.00/60.08 [proper(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(proper(x))] 212.00/60.08 212.00/60.08 [proper(c())] = [0] 212.00/60.08 ? [1] 212.00/60.08 = [ok(c())] 212.00/60.08 212.00/60.08 212.00/60.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.00/60.08 212.00/60.08 We are left with following problem, upon which TcT provides the 212.00/60.08 certificate YES(O(1),O(n^2)). 212.00/60.08 212.00/60.08 Strict Trs: 212.00/60.08 { active(f(x)) -> f(active(x)) 212.00/60.08 , active(f(x)) -> mark(x) 212.00/60.08 , f(mark(x)) -> mark(f(x)) 212.00/60.08 , f(ok(x)) -> ok(f(x)) 212.00/60.08 , f(found(x)) -> found(f(x)) 212.00/60.08 , top(active(c())) -> top(mark(c())) 212.00/60.08 , top(mark(x)) -> top(check(x)) 212.00/60.08 , check(f(x)) -> f(check(x)) 212.00/60.08 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.08 , proper(f(x)) -> f(proper(x)) 212.00/60.08 , proper(c()) -> ok(c()) } 212.00/60.08 Weak Trs: 212.00/60.08 { top(found(x)) -> top(active(x)) 212.00/60.08 , check(x) -> start(match(f(X()), x)) 212.00/60.08 , start(ok(x)) -> found(x) 212.00/60.08 , match(X(), x) -> proper(x) } 212.00/60.08 Obligation: 212.00/60.08 derivational complexity 212.00/60.08 Answer: 212.00/60.08 YES(O(1),O(n^2)) 212.00/60.08 212.00/60.08 The weightgap principle applies (using the following nonconstant 212.00/60.08 growth matrix-interpretation) 212.00/60.08 212.00/60.08 TcT has computed the following triangular matrix interpretation. 212.00/60.08 Note that the diagonal of the component-wise maxima of 212.00/60.08 interpretation-entries contains no more than 1 non-zero entries. 212.00/60.08 212.00/60.08 [active](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [f](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [mark](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [top](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [c] = [0] 212.00/60.08 212.00/60.08 [check](x1) = [1] x1 + [2] 212.00/60.08 212.00/60.08 [start](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [match](x1, x2) = [1] x1 + [1] x2 + [0] 212.00/60.08 212.00/60.08 [X] = [2] 212.00/60.08 212.00/60.08 [proper](x1) = [1] x1 + [1] 212.00/60.08 212.00/60.08 [ok](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 [found](x1) = [1] x1 + [0] 212.00/60.08 212.00/60.08 The order satisfies the following ordering constraints: 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [f(active(x))] 212.00/60.08 212.00/60.08 [active(f(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(x)] 212.00/60.08 212.00/60.08 [f(mark(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [mark(f(x))] 212.00/60.08 212.00/60.08 [f(ok(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [ok(f(x))] 212.00/60.08 212.00/60.08 [f(found(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [found(f(x))] 212.00/60.08 212.00/60.08 [top(active(c()))] = [0] 212.00/60.08 >= [0] 212.00/60.08 = [top(mark(c()))] 212.00/60.08 212.00/60.08 [top(mark(x))] = [1] x + [0] 212.00/60.08 ? [1] x + [2] 212.00/60.08 = [top(check(x))] 212.00/60.08 212.00/60.08 [top(found(x))] = [1] x + [0] 212.00/60.08 >= [1] x + [0] 212.00/60.08 = [top(active(x))] 212.00/60.08 212.00/60.08 [check(x)] = [1] x + [2] 212.00/60.08 >= [1] x + [2] 212.00/60.08 = [start(match(f(X()), x))] 212.00/60.09 212.00/60.09 [check(f(x))] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [f(check(x))] 212.00/60.09 212.00/60.09 [start(ok(x))] = [1] x + [0] 212.00/60.09 >= [1] x + [0] 212.00/60.09 = [found(x)] 212.00/60.09 212.00/60.09 [match(f(x), f(y))] = [1] x + [1] y + [0] 212.00/60.09 >= [1] x + [1] y + [0] 212.00/60.09 = [f(match(x, y))] 212.00/60.09 212.00/60.09 [match(X(), x)] = [1] x + [2] 212.00/60.09 > [1] x + [1] 212.00/60.09 = [proper(x)] 212.00/60.09 212.00/60.09 [proper(f(x))] = [1] x + [1] 212.00/60.09 >= [1] x + [1] 212.00/60.09 = [f(proper(x))] 212.00/60.09 212.00/60.09 [proper(c())] = [1] 212.00/60.09 > [0] 212.00/60.09 = [ok(c())] 212.00/60.09 212.00/60.09 212.00/60.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.00/60.09 212.00/60.09 We are left with following problem, upon which TcT provides the 212.00/60.09 certificate YES(O(1),O(n^2)). 212.00/60.09 212.00/60.09 Strict Trs: 212.00/60.09 { active(f(x)) -> f(active(x)) 212.00/60.09 , active(f(x)) -> mark(x) 212.00/60.09 , f(mark(x)) -> mark(f(x)) 212.00/60.09 , f(ok(x)) -> ok(f(x)) 212.00/60.09 , f(found(x)) -> found(f(x)) 212.00/60.09 , top(active(c())) -> top(mark(c())) 212.00/60.09 , top(mark(x)) -> top(check(x)) 212.00/60.09 , check(f(x)) -> f(check(x)) 212.00/60.09 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.09 , proper(f(x)) -> f(proper(x)) } 212.00/60.09 Weak Trs: 212.00/60.09 { top(found(x)) -> top(active(x)) 212.00/60.09 , check(x) -> start(match(f(X()), x)) 212.00/60.09 , start(ok(x)) -> found(x) 212.00/60.09 , match(X(), x) -> proper(x) 212.00/60.09 , proper(c()) -> ok(c()) } 212.00/60.09 Obligation: 212.00/60.09 derivational complexity 212.00/60.09 Answer: 212.00/60.09 YES(O(1),O(n^2)) 212.00/60.09 212.00/60.09 The weightgap principle applies (using the following nonconstant 212.00/60.09 growth matrix-interpretation) 212.00/60.09 212.00/60.09 TcT has computed the following triangular matrix interpretation. 212.00/60.09 Note that the diagonal of the component-wise maxima of 212.00/60.09 interpretation-entries contains no more than 1 non-zero entries. 212.00/60.09 212.00/60.09 [active](x1) = [1] x1 + [1] 212.00/60.09 212.00/60.09 [f](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [mark](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [top](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [c] = [0] 212.00/60.09 212.00/60.09 [check](x1) = [1] x1 + [2] 212.00/60.09 212.00/60.09 [start](x1) = [1] x1 + [2] 212.00/60.09 212.00/60.09 [match](x1, x2) = [1] x1 + [1] x2 + [0] 212.00/60.09 212.00/60.09 [X] = [0] 212.00/60.09 212.00/60.09 [proper](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [ok](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [found](x1) = [1] x1 + [1] 212.00/60.09 212.00/60.09 The order satisfies the following ordering constraints: 212.00/60.09 212.00/60.09 [active(f(x))] = [1] x + [1] 212.00/60.09 >= [1] x + [1] 212.00/60.09 = [f(active(x))] 212.00/60.09 212.00/60.09 [active(f(x))] = [1] x + [1] 212.00/60.09 > [1] x + [0] 212.00/60.09 = [mark(x)] 212.00/60.09 212.00/60.09 [f(mark(x))] = [1] x + [0] 212.00/60.09 >= [1] x + [0] 212.00/60.09 = [mark(f(x))] 212.00/60.09 212.00/60.09 [f(ok(x))] = [1] x + [0] 212.00/60.09 >= [1] x + [0] 212.00/60.09 = [ok(f(x))] 212.00/60.09 212.00/60.09 [f(found(x))] = [1] x + [1] 212.00/60.09 >= [1] x + [1] 212.00/60.09 = [found(f(x))] 212.00/60.09 212.00/60.09 [top(active(c()))] = [1] 212.00/60.09 > [0] 212.00/60.09 = [top(mark(c()))] 212.00/60.09 212.00/60.09 [top(mark(x))] = [1] x + [0] 212.00/60.09 ? [1] x + [2] 212.00/60.09 = [top(check(x))] 212.00/60.09 212.00/60.09 [top(found(x))] = [1] x + [1] 212.00/60.09 >= [1] x + [1] 212.00/60.09 = [top(active(x))] 212.00/60.09 212.00/60.09 [check(x)] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [start(match(f(X()), x))] 212.00/60.09 212.00/60.09 [check(f(x))] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [f(check(x))] 212.00/60.09 212.00/60.09 [start(ok(x))] = [1] x + [2] 212.00/60.09 > [1] x + [1] 212.00/60.09 = [found(x)] 212.00/60.09 212.00/60.09 [match(f(x), f(y))] = [1] x + [1] y + [0] 212.00/60.09 >= [1] x + [1] y + [0] 212.00/60.09 = [f(match(x, y))] 212.00/60.09 212.00/60.09 [match(X(), x)] = [1] x + [0] 212.00/60.09 >= [1] x + [0] 212.00/60.09 = [proper(x)] 212.00/60.09 212.00/60.09 [proper(f(x))] = [1] x + [0] 212.00/60.09 >= [1] x + [0] 212.00/60.09 = [f(proper(x))] 212.00/60.09 212.00/60.09 [proper(c())] = [0] 212.00/60.09 >= [0] 212.00/60.09 = [ok(c())] 212.00/60.09 212.00/60.09 212.00/60.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.00/60.09 212.00/60.09 We are left with following problem, upon which TcT provides the 212.00/60.09 certificate YES(O(1),O(n^2)). 212.00/60.09 212.00/60.09 Strict Trs: 212.00/60.09 { active(f(x)) -> f(active(x)) 212.00/60.09 , f(mark(x)) -> mark(f(x)) 212.00/60.09 , f(ok(x)) -> ok(f(x)) 212.00/60.09 , f(found(x)) -> found(f(x)) 212.00/60.09 , top(mark(x)) -> top(check(x)) 212.00/60.09 , check(f(x)) -> f(check(x)) 212.00/60.09 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.09 , proper(f(x)) -> f(proper(x)) } 212.00/60.09 Weak Trs: 212.00/60.09 { active(f(x)) -> mark(x) 212.00/60.09 , top(active(c())) -> top(mark(c())) 212.00/60.09 , top(found(x)) -> top(active(x)) 212.00/60.09 , check(x) -> start(match(f(X()), x)) 212.00/60.09 , start(ok(x)) -> found(x) 212.00/60.09 , match(X(), x) -> proper(x) 212.00/60.09 , proper(c()) -> ok(c()) } 212.00/60.09 Obligation: 212.00/60.09 derivational complexity 212.00/60.09 Answer: 212.00/60.09 YES(O(1),O(n^2)) 212.00/60.09 212.00/60.09 The weightgap principle applies (using the following nonconstant 212.00/60.09 growth matrix-interpretation) 212.00/60.09 212.00/60.09 TcT has computed the following triangular matrix interpretation. 212.00/60.09 Note that the diagonal of the component-wise maxima of 212.00/60.09 interpretation-entries contains no more than 1 non-zero entries. 212.00/60.09 212.00/60.09 [active](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [f](x1) = [1] x1 + [2] 212.00/60.09 212.00/60.09 [mark](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [top](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [c] = [0] 212.00/60.09 212.00/60.09 [check](x1) = [1] x1 + [2] 212.00/60.09 212.00/60.09 [start](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [match](x1, x2) = [1] x1 + [1] x2 + [0] 212.00/60.09 212.00/60.09 [X] = [0] 212.00/60.09 212.00/60.09 [proper](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [ok](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 [found](x1) = [1] x1 + [0] 212.00/60.09 212.00/60.09 The order satisfies the following ordering constraints: 212.00/60.09 212.00/60.09 [active(f(x))] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [f(active(x))] 212.00/60.09 212.00/60.09 [active(f(x))] = [1] x + [2] 212.00/60.09 > [1] x + [0] 212.00/60.09 = [mark(x)] 212.00/60.09 212.00/60.09 [f(mark(x))] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [mark(f(x))] 212.00/60.09 212.00/60.09 [f(ok(x))] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [ok(f(x))] 212.00/60.09 212.00/60.09 [f(found(x))] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [found(f(x))] 212.00/60.09 212.00/60.09 [top(active(c()))] = [0] 212.00/60.09 >= [0] 212.00/60.09 = [top(mark(c()))] 212.00/60.09 212.00/60.09 [top(mark(x))] = [1] x + [0] 212.00/60.09 ? [1] x + [2] 212.00/60.09 = [top(check(x))] 212.00/60.09 212.00/60.09 [top(found(x))] = [1] x + [0] 212.00/60.09 >= [1] x + [0] 212.00/60.09 = [top(active(x))] 212.00/60.09 212.00/60.09 [check(x)] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [start(match(f(X()), x))] 212.00/60.09 212.00/60.09 [check(f(x))] = [1] x + [4] 212.00/60.09 >= [1] x + [4] 212.00/60.09 = [f(check(x))] 212.00/60.09 212.00/60.09 [start(ok(x))] = [1] x + [0] 212.00/60.09 >= [1] x + [0] 212.00/60.09 = [found(x)] 212.00/60.09 212.00/60.09 [match(f(x), f(y))] = [1] x + [1] y + [4] 212.00/60.09 > [1] x + [1] y + [2] 212.00/60.09 = [f(match(x, y))] 212.00/60.09 212.00/60.09 [match(X(), x)] = [1] x + [0] 212.00/60.09 >= [1] x + [0] 212.00/60.09 = [proper(x)] 212.00/60.09 212.00/60.09 [proper(f(x))] = [1] x + [2] 212.00/60.09 >= [1] x + [2] 212.00/60.09 = [f(proper(x))] 212.00/60.09 212.00/60.09 [proper(c())] = [0] 212.00/60.09 >= [0] 212.00/60.09 = [ok(c())] 212.00/60.09 212.00/60.09 212.00/60.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 212.00/60.09 212.00/60.09 We are left with following problem, upon which TcT provides the 212.00/60.09 certificate YES(O(1),O(n^2)). 212.00/60.09 212.00/60.09 Strict Trs: 212.00/60.09 { active(f(x)) -> f(active(x)) 212.00/60.09 , f(mark(x)) -> mark(f(x)) 212.00/60.09 , f(ok(x)) -> ok(f(x)) 212.00/60.09 , f(found(x)) -> found(f(x)) 212.00/60.09 , top(mark(x)) -> top(check(x)) 212.00/60.09 , check(f(x)) -> f(check(x)) 212.00/60.09 , proper(f(x)) -> f(proper(x)) } 212.00/60.09 Weak Trs: 212.00/60.09 { active(f(x)) -> mark(x) 212.00/60.09 , top(active(c())) -> top(mark(c())) 212.00/60.09 , top(found(x)) -> top(active(x)) 212.00/60.09 , check(x) -> start(match(f(X()), x)) 212.00/60.09 , start(ok(x)) -> found(x) 212.00/60.09 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.09 , match(X(), x) -> proper(x) 212.00/60.09 , proper(c()) -> ok(c()) } 212.00/60.09 Obligation: 212.00/60.09 derivational complexity 212.00/60.09 Answer: 212.00/60.09 YES(O(1),O(n^2)) 212.00/60.09 212.00/60.09 We use the processor 'matrix interpretation of dimension 2' to 212.00/60.09 orient following rules strictly. 212.00/60.09 212.00/60.09 Trs: { active(f(x)) -> f(active(x)) } 212.00/60.09 212.00/60.09 The induced complexity on above rules (modulo remaining rules) is 212.00/60.09 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.00/60.09 component(s). 212.00/60.09 212.00/60.09 Sub-proof: 212.00/60.09 ---------- 212.00/60.09 TcT has computed the following triangular matrix interpretation. 212.00/60.09 212.00/60.09 [active](x1) = [1 2] x1 + [2] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [f](x1) = [1 2] x1 + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [mark](x1) = [1 2] x1 + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [top](x1) = [1 1] x1 + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 212.00/60.09 [c] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [check](x1) = [1 2] x1 + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [start](x1) = [1 2] x1 + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [match](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 212.00/60.09 [0 0] [0 1] [0] 212.00/60.09 212.00/60.09 [X] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [proper](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [ok](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [found](x1) = [1 2] x1 + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 The order satisfies the following ordering constraints: 212.00/60.09 212.00/60.09 [active(f(x))] = [1 4] x + [4] 212.00/60.09 [0 1] [1] 212.00/60.09 > [1 4] x + [2] 212.00/60.09 [0 1] [1] 212.00/60.09 = [f(active(x))] 212.00/60.09 212.00/60.09 [active(f(x))] = [1 4] x + [4] 212.00/60.09 [0 1] [1] 212.00/60.09 > [1 2] x + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 = [mark(x)] 212.00/60.09 212.00/60.09 [f(mark(x))] = [1 4] x + [3] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 4] x + [3] 212.00/60.09 [0 1] [2] 212.00/60.09 = [mark(f(x))] 212.00/60.09 212.00/60.09 [f(ok(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [ok(f(x))] 212.00/60.09 212.00/60.09 [f(found(x))] = [1 4] x + [3] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 4] x + [3] 212.00/60.09 [0 1] [2] 212.00/60.09 = [found(f(x))] 212.00/60.09 212.00/60.09 [top(active(c()))] = [2] 212.00/60.09 [0] 212.00/60.09 >= [2] 212.00/60.09 [0] 212.00/60.09 = [top(mark(c()))] 212.00/60.09 212.00/60.09 [top(mark(x))] = [1 3] x + [2] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 3] x + [2] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(check(x))] 212.00/60.09 212.00/60.09 [top(found(x))] = [1 3] x + [2] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 3] x + [2] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(active(x))] 212.00/60.09 212.00/60.09 [check(x)] = [1 2] x + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 2] x + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 = [start(match(f(X()), x))] 212.00/60.09 212.00/60.09 [check(f(x))] = [1 4] x + [3] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 4] x + [3] 212.00/60.09 [0 1] [2] 212.00/60.09 = [f(check(x))] 212.00/60.09 212.00/60.09 [start(ok(x))] = [1 2] x + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 2] x + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 = [found(x)] 212.00/60.09 212.00/60.09 [match(f(x), f(y))] = [1 2] x + [1 2] y + [0] 212.00/60.09 [0 0] [0 1] [1] 212.00/60.09 >= [1 0] x + [1 2] y + [0] 212.00/60.09 [0 0] [0 1] [1] 212.00/60.09 = [f(match(x, y))] 212.00/60.09 212.00/60.09 [match(X(), x)] = [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [proper(x)] 212.00/60.09 212.00/60.09 [proper(f(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [f(proper(x))] 212.00/60.09 212.00/60.09 [proper(c())] = [0] 212.00/60.09 [0] 212.00/60.09 >= [0] 212.00/60.09 [0] 212.00/60.09 = [ok(c())] 212.00/60.09 212.00/60.09 212.00/60.09 We return to the main proof. 212.00/60.09 212.00/60.09 We are left with following problem, upon which TcT provides the 212.00/60.09 certificate YES(O(1),O(n^2)). 212.00/60.09 212.00/60.09 Strict Trs: 212.00/60.09 { f(mark(x)) -> mark(f(x)) 212.00/60.09 , f(ok(x)) -> ok(f(x)) 212.00/60.09 , f(found(x)) -> found(f(x)) 212.00/60.09 , top(mark(x)) -> top(check(x)) 212.00/60.09 , check(f(x)) -> f(check(x)) 212.00/60.09 , proper(f(x)) -> f(proper(x)) } 212.00/60.09 Weak Trs: 212.00/60.09 { active(f(x)) -> f(active(x)) 212.00/60.09 , active(f(x)) -> mark(x) 212.00/60.09 , top(active(c())) -> top(mark(c())) 212.00/60.09 , top(found(x)) -> top(active(x)) 212.00/60.09 , check(x) -> start(match(f(X()), x)) 212.00/60.09 , start(ok(x)) -> found(x) 212.00/60.09 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.09 , match(X(), x) -> proper(x) 212.00/60.09 , proper(c()) -> ok(c()) } 212.00/60.09 Obligation: 212.00/60.09 derivational complexity 212.00/60.09 Answer: 212.00/60.09 YES(O(1),O(n^2)) 212.00/60.09 212.00/60.09 We use the processor 'matrix interpretation of dimension 2' to 212.00/60.09 orient following rules strictly. 212.00/60.09 212.00/60.09 Trs: { f(mark(x)) -> mark(f(x)) } 212.00/60.09 212.00/60.09 The induced complexity on above rules (modulo remaining rules) is 212.00/60.09 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.00/60.09 component(s). 212.00/60.09 212.00/60.09 Sub-proof: 212.00/60.09 ---------- 212.00/60.09 TcT has computed the following triangular matrix interpretation. 212.00/60.09 212.00/60.09 [active](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [f](x1) = [1 1] x1 + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 212.00/60.09 [mark](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [top](x1) = [1 0] x1 + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 212.00/60.09 [c] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [check](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [start](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [match](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 212.00/60.09 [0 0] [0 1] [0] 212.00/60.09 212.00/60.09 [X] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [proper](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [ok](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [found](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 The order satisfies the following ordering constraints: 212.00/60.09 212.00/60.09 [active(f(x))] = [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [f(active(x))] 212.00/60.09 212.00/60.09 [active(f(x))] = [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [mark(x)] 212.00/60.09 212.00/60.09 [f(mark(x))] = [1 1] x + [1] 212.00/60.09 [0 1] [3] 212.00/60.09 > [1 1] x + [0] 212.00/60.09 [0 1] [3] 212.00/60.09 = [mark(f(x))] 212.00/60.09 212.00/60.09 [f(ok(x))] = [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [ok(f(x))] 212.00/60.09 212.00/60.09 [f(found(x))] = [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [found(f(x))] 212.00/60.09 212.00/60.09 [top(active(c()))] = [0] 212.00/60.09 [0] 212.00/60.09 >= [0] 212.00/60.09 [0] 212.00/60.09 = [top(mark(c()))] 212.00/60.09 212.00/60.09 [top(mark(x))] = [1 0] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(check(x))] 212.00/60.09 212.00/60.09 [top(found(x))] = [1 0] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(active(x))] 212.00/60.09 212.00/60.09 [check(x)] = [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [start(match(f(X()), x))] 212.00/60.09 212.00/60.09 [check(f(x))] = [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [f(check(x))] 212.00/60.09 212.00/60.09 [start(ok(x))] = [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [found(x)] 212.00/60.09 212.00/60.09 [match(f(x), f(y))] = [1 1] x + [1 1] y + [0] 212.00/60.09 [0 0] [0 1] [2] 212.00/60.09 >= [1 0] x + [1 1] y + [0] 212.00/60.09 [0 0] [0 1] [2] 212.00/60.09 = [f(match(x, y))] 212.00/60.09 212.00/60.09 [match(X(), x)] = [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [proper(x)] 212.00/60.09 212.00/60.09 [proper(f(x))] = [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [f(proper(x))] 212.00/60.09 212.00/60.09 [proper(c())] = [0] 212.00/60.09 [0] 212.00/60.09 >= [0] 212.00/60.09 [0] 212.00/60.09 = [ok(c())] 212.00/60.09 212.00/60.09 212.00/60.09 We return to the main proof. 212.00/60.09 212.00/60.09 We are left with following problem, upon which TcT provides the 212.00/60.09 certificate YES(O(1),O(n^2)). 212.00/60.09 212.00/60.09 Strict Trs: 212.00/60.09 { f(ok(x)) -> ok(f(x)) 212.00/60.09 , f(found(x)) -> found(f(x)) 212.00/60.09 , top(mark(x)) -> top(check(x)) 212.00/60.09 , check(f(x)) -> f(check(x)) 212.00/60.09 , proper(f(x)) -> f(proper(x)) } 212.00/60.09 Weak Trs: 212.00/60.09 { active(f(x)) -> f(active(x)) 212.00/60.09 , active(f(x)) -> mark(x) 212.00/60.09 , f(mark(x)) -> mark(f(x)) 212.00/60.09 , top(active(c())) -> top(mark(c())) 212.00/60.09 , top(found(x)) -> top(active(x)) 212.00/60.09 , check(x) -> start(match(f(X()), x)) 212.00/60.09 , start(ok(x)) -> found(x) 212.00/60.09 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.09 , match(X(), x) -> proper(x) 212.00/60.09 , proper(c()) -> ok(c()) } 212.00/60.09 Obligation: 212.00/60.09 derivational complexity 212.00/60.09 Answer: 212.00/60.09 YES(O(1),O(n^2)) 212.00/60.09 212.00/60.09 We use the processor 'matrix interpretation of dimension 2' to 212.00/60.09 orient following rules strictly. 212.00/60.09 212.00/60.09 Trs: { check(f(x)) -> f(check(x)) } 212.00/60.09 212.00/60.09 The induced complexity on above rules (modulo remaining rules) is 212.00/60.09 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.00/60.09 component(s). 212.00/60.09 212.00/60.09 Sub-proof: 212.00/60.09 ---------- 212.00/60.09 TcT has computed the following triangular matrix interpretation. 212.00/60.09 212.00/60.09 [active](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [f](x1) = [1 2] x1 + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 212.00/60.09 [mark](x1) = [1 2] x1 + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 212.00/60.09 [top](x1) = [1 0] x1 + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 212.00/60.09 [c] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [check](x1) = [1 2] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [start](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [match](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 212.00/60.09 [0 0] [0 1] [0] 212.00/60.09 212.00/60.09 [X] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [proper](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [ok](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [found](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 The order satisfies the following ordering constraints: 212.00/60.09 212.00/60.09 [active(f(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [f(active(x))] 212.00/60.09 212.00/60.09 [active(f(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [mark(x)] 212.00/60.09 212.00/60.09 [f(mark(x))] = [1 4] x + [4] 212.00/60.09 [0 1] [4] 212.00/60.09 >= [1 4] x + [4] 212.00/60.09 [0 1] [4] 212.00/60.09 = [mark(f(x))] 212.00/60.09 212.00/60.09 [f(ok(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [ok(f(x))] 212.00/60.09 212.00/60.09 [f(found(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [found(f(x))] 212.00/60.09 212.00/60.09 [top(active(c()))] = [0] 212.00/60.09 [0] 212.00/60.09 >= [0] 212.00/60.09 [0] 212.00/60.09 = [top(mark(c()))] 212.00/60.09 212.00/60.09 [top(mark(x))] = [1 2] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(check(x))] 212.00/60.09 212.00/60.09 [top(found(x))] = [1 0] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(active(x))] 212.00/60.09 212.00/60.09 [check(x)] = [1 2] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [start(match(f(X()), x))] 212.00/60.09 212.00/60.09 [check(f(x))] = [1 4] x + [4] 212.00/60.09 [0 1] [2] 212.00/60.09 > [1 4] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [f(check(x))] 212.00/60.09 212.00/60.09 [start(ok(x))] = [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [found(x)] 212.00/60.09 212.00/60.09 [match(f(x), f(y))] = [1 2] x + [1 2] y + [0] 212.00/60.09 [0 0] [0 1] [2] 212.00/60.09 >= [1 0] x + [1 2] y + [0] 212.00/60.09 [0 0] [0 1] [2] 212.00/60.09 = [f(match(x, y))] 212.00/60.09 212.00/60.09 [match(X(), x)] = [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [proper(x)] 212.00/60.09 212.00/60.09 [proper(f(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 = [f(proper(x))] 212.00/60.09 212.00/60.09 [proper(c())] = [0] 212.00/60.09 [0] 212.00/60.09 >= [0] 212.00/60.09 [0] 212.00/60.09 = [ok(c())] 212.00/60.09 212.00/60.09 212.00/60.09 We return to the main proof. 212.00/60.09 212.00/60.09 We are left with following problem, upon which TcT provides the 212.00/60.09 certificate YES(O(1),O(n^2)). 212.00/60.09 212.00/60.09 Strict Trs: 212.00/60.09 { f(ok(x)) -> ok(f(x)) 212.00/60.09 , f(found(x)) -> found(f(x)) 212.00/60.09 , top(mark(x)) -> top(check(x)) 212.00/60.09 , proper(f(x)) -> f(proper(x)) } 212.00/60.09 Weak Trs: 212.00/60.09 { active(f(x)) -> f(active(x)) 212.00/60.09 , active(f(x)) -> mark(x) 212.00/60.09 , f(mark(x)) -> mark(f(x)) 212.00/60.09 , top(active(c())) -> top(mark(c())) 212.00/60.09 , top(found(x)) -> top(active(x)) 212.00/60.09 , check(x) -> start(match(f(X()), x)) 212.00/60.09 , check(f(x)) -> f(check(x)) 212.00/60.09 , start(ok(x)) -> found(x) 212.00/60.09 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.09 , match(X(), x) -> proper(x) 212.00/60.09 , proper(c()) -> ok(c()) } 212.00/60.09 Obligation: 212.00/60.09 derivational complexity 212.00/60.09 Answer: 212.00/60.09 YES(O(1),O(n^2)) 212.00/60.09 212.00/60.09 We use the processor 'matrix interpretation of dimension 2' to 212.00/60.09 orient following rules strictly. 212.00/60.09 212.00/60.09 Trs: { proper(f(x)) -> f(proper(x)) } 212.00/60.09 212.00/60.09 The induced complexity on above rules (modulo remaining rules) is 212.00/60.09 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.00/60.09 component(s). 212.00/60.09 212.00/60.09 Sub-proof: 212.00/60.09 ---------- 212.00/60.09 TcT has computed the following triangular matrix interpretation. 212.00/60.09 212.00/60.09 [active](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [f](x1) = [1 2] x1 + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [mark](x1) = [1 1] x1 + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [top](x1) = [1 0] x1 + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 212.00/60.09 [c] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [check](x1) = [1 1] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [start](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [match](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 212.00/60.09 [0 0] [0 1] [0] 212.00/60.09 212.00/60.09 [X] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [proper](x1) = [1 1] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [ok](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [found](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 The order satisfies the following ordering constraints: 212.00/60.09 212.00/60.09 [active(f(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [f(active(x))] 212.00/60.09 212.00/60.09 [active(f(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [mark(x)] 212.00/60.09 212.00/60.09 [f(mark(x))] = [1 3] x + [2] 212.00/60.09 [0 1] [2] 212.00/60.09 > [1 3] x + [1] 212.00/60.09 [0 1] [2] 212.00/60.09 = [mark(f(x))] 212.00/60.09 212.00/60.09 [f(ok(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [ok(f(x))] 212.00/60.09 212.00/60.09 [f(found(x))] = [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 2] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [found(f(x))] 212.00/60.09 212.00/60.09 [top(active(c()))] = [0] 212.00/60.09 [0] 212.00/60.09 >= [0] 212.00/60.09 [0] 212.00/60.09 = [top(mark(c()))] 212.00/60.09 212.00/60.09 [top(mark(x))] = [1 1] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(check(x))] 212.00/60.09 212.00/60.09 [top(found(x))] = [1 0] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(active(x))] 212.00/60.09 212.00/60.09 [check(x)] = [1 1] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [start(match(f(X()), x))] 212.00/60.09 212.00/60.09 [check(f(x))] = [1 3] x + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 > [1 3] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [f(check(x))] 212.00/60.09 212.00/60.09 [start(ok(x))] = [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 0] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [found(x)] 212.00/60.09 212.00/60.09 [match(f(x), f(y))] = [1 2] x + [1 3] y + [1] 212.00/60.09 [0 0] [0 1] [1] 212.00/60.09 > [1 0] x + [1 3] y + [0] 212.00/60.09 [0 0] [0 1] [1] 212.00/60.09 = [f(match(x, y))] 212.00/60.09 212.00/60.09 [match(X(), x)] = [1 1] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 >= [1 1] x + [0] 212.00/60.09 [0 1] [0] 212.00/60.09 = [proper(x)] 212.00/60.09 212.00/60.09 [proper(f(x))] = [1 3] x + [1] 212.00/60.09 [0 1] [1] 212.00/60.09 > [1 3] x + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 = [f(proper(x))] 212.00/60.09 212.00/60.09 [proper(c())] = [0] 212.00/60.09 [0] 212.00/60.09 >= [0] 212.00/60.09 [0] 212.00/60.09 = [ok(c())] 212.00/60.09 212.00/60.09 212.00/60.09 We return to the main proof. 212.00/60.09 212.00/60.09 We are left with following problem, upon which TcT provides the 212.00/60.09 certificate YES(O(1),O(n^2)). 212.00/60.09 212.00/60.09 Strict Trs: 212.00/60.09 { f(ok(x)) -> ok(f(x)) 212.00/60.09 , f(found(x)) -> found(f(x)) 212.00/60.09 , top(mark(x)) -> top(check(x)) } 212.00/60.09 Weak Trs: 212.00/60.09 { active(f(x)) -> f(active(x)) 212.00/60.09 , active(f(x)) -> mark(x) 212.00/60.09 , f(mark(x)) -> mark(f(x)) 212.00/60.09 , top(active(c())) -> top(mark(c())) 212.00/60.09 , top(found(x)) -> top(active(x)) 212.00/60.09 , check(x) -> start(match(f(X()), x)) 212.00/60.09 , check(f(x)) -> f(check(x)) 212.00/60.09 , start(ok(x)) -> found(x) 212.00/60.09 , match(f(x), f(y)) -> f(match(x, y)) 212.00/60.09 , match(X(), x) -> proper(x) 212.00/60.09 , proper(f(x)) -> f(proper(x)) 212.00/60.09 , proper(c()) -> ok(c()) } 212.00/60.09 Obligation: 212.00/60.09 derivational complexity 212.00/60.09 Answer: 212.00/60.09 YES(O(1),O(n^2)) 212.00/60.09 212.00/60.09 We use the processor 'matrix interpretation of dimension 2' to 212.00/60.09 orient following rules strictly. 212.00/60.09 212.00/60.09 Trs: { f(ok(x)) -> ok(f(x)) } 212.00/60.09 212.00/60.09 The induced complexity on above rules (modulo remaining rules) is 212.00/60.09 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.00/60.09 component(s). 212.00/60.09 212.00/60.09 Sub-proof: 212.00/60.09 ---------- 212.00/60.09 TcT has computed the following triangular matrix interpretation. 212.00/60.09 212.00/60.09 [active](x1) = [1 0] x1 + [2] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [f](x1) = [1 2] x1 + [0] 212.00/60.09 [0 1] [2] 212.00/60.09 212.00/60.09 [mark](x1) = [1 1] x1 + [2] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [top](x1) = [1 0] x1 + [0] 212.00/60.09 [0 0] [0] 212.00/60.09 212.00/60.09 [c] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [check](x1) = [1 1] x1 + [2] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [start](x1) = [1 0] x1 + [2] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 [match](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 212.00/60.09 [0 0] [0 1] [1] 212.00/60.09 212.00/60.09 [X] = [0] 212.00/60.09 [0] 212.00/60.09 212.00/60.09 [proper](x1) = [1 1] x1 + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [ok](x1) = [1 0] x1 + [0] 212.00/60.09 [0 1] [1] 212.00/60.09 212.00/60.09 [found](x1) = [1 0] x1 + [2] 212.00/60.09 [0 1] [0] 212.00/60.09 212.00/60.09 The order satisfies the following ordering constraints: 212.00/60.09 212.00/60.09 [active(f(x))] = [1 2] x + [2] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 2] x + [2] 212.00/60.09 [0 1] [2] 212.00/60.09 = [f(active(x))] 212.00/60.09 212.00/60.09 [active(f(x))] = [1 2] x + [2] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 1] x + [2] 212.00/60.09 [0 1] [1] 212.00/60.09 = [mark(x)] 212.00/60.09 212.00/60.09 [f(mark(x))] = [1 3] x + [4] 212.00/60.09 [0 1] [3] 212.00/60.09 >= [1 3] x + [4] 212.00/60.09 [0 1] [3] 212.00/60.09 = [mark(f(x))] 212.00/60.09 212.00/60.09 [f(ok(x))] = [1 2] x + [2] 212.00/60.09 [0 1] [3] 212.00/60.09 > [1 2] x + [0] 212.00/60.09 [0 1] [3] 212.00/60.09 = [ok(f(x))] 212.00/60.09 212.00/60.09 [f(found(x))] = [1 2] x + [2] 212.00/60.09 [0 1] [2] 212.00/60.09 >= [1 2] x + [2] 212.00/60.09 [0 1] [2] 212.00/60.09 = [found(f(x))] 212.00/60.09 212.00/60.09 [top(active(c()))] = [2] 212.00/60.09 [0] 212.00/60.09 >= [2] 212.00/60.09 [0] 212.00/60.09 = [top(mark(c()))] 212.00/60.09 212.00/60.09 [top(mark(x))] = [1 1] x + [2] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 1] x + [2] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(check(x))] 212.00/60.09 212.00/60.09 [top(found(x))] = [1 0] x + [2] 212.00/60.09 [0 0] [0] 212.00/60.09 >= [1 0] x + [2] 212.00/60.09 [0 0] [0] 212.00/60.09 = [top(active(x))] 212.00/60.09 212.00/60.09 [check(x)] = [1 1] x + [2] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 1] x + [2] 212.00/60.09 [0 1] [1] 212.00/60.09 = [start(match(f(X()), x))] 212.00/60.09 212.00/60.09 [check(f(x))] = [1 3] x + [4] 212.00/60.09 [0 1] [3] 212.00/60.09 >= [1 3] x + [4] 212.00/60.09 [0 1] [3] 212.00/60.09 = [f(check(x))] 212.00/60.09 212.00/60.09 [start(ok(x))] = [1 0] x + [2] 212.00/60.09 [0 1] [1] 212.00/60.09 >= [1 0] x + [2] 212.00/60.09 [0 1] [0] 212.00/60.09 = [found(x)] 212.00/60.09 212.00/60.09 [match(f(x), f(y))] = [1 2] x + [1 3] y + [2] 212.00/60.09 [0 0] [0 1] [3] 212.00/60.09 >= [1 0] x + [1 3] y + [2] 212.00/60.09 [0 0] [0 1] [3] 212.00/60.09 = [f(match(x, y))] 212.00/60.10 212.00/60.10 [match(X(), x)] = [1 1] x + [0] 212.00/60.10 [0 1] [1] 212.00/60.10 >= [1 1] x + [0] 212.00/60.10 [0 1] [1] 212.00/60.10 = [proper(x)] 212.00/60.10 212.00/60.10 [proper(f(x))] = [1 3] x + [2] 212.00/60.10 [0 1] [3] 212.00/60.10 >= [1 3] x + [2] 212.00/60.10 [0 1] [3] 212.00/60.10 = [f(proper(x))] 212.00/60.10 212.00/60.10 [proper(c())] = [0] 212.00/60.10 [1] 212.00/60.10 >= [0] 212.00/60.10 [1] 212.00/60.10 = [ok(c())] 212.00/60.10 212.00/60.10 212.00/60.10 We return to the main proof. 212.23/60.10 212.23/60.10 We are left with following problem, upon which TcT provides the 212.23/60.10 certificate YES(O(1),O(n^2)). 212.23/60.10 212.23/60.10 Strict Trs: 212.23/60.10 { f(found(x)) -> found(f(x)) 212.23/60.10 , top(mark(x)) -> top(check(x)) } 212.23/60.10 Weak Trs: 212.23/60.10 { active(f(x)) -> f(active(x)) 212.23/60.10 , active(f(x)) -> mark(x) 212.23/60.10 , f(mark(x)) -> mark(f(x)) 212.23/60.10 , f(ok(x)) -> ok(f(x)) 212.23/60.10 , top(active(c())) -> top(mark(c())) 212.23/60.10 , top(found(x)) -> top(active(x)) 212.23/60.10 , check(x) -> start(match(f(X()), x)) 212.23/60.10 , check(f(x)) -> f(check(x)) 212.23/60.10 , start(ok(x)) -> found(x) 212.23/60.10 , match(f(x), f(y)) -> f(match(x, y)) 212.23/60.10 , match(X(), x) -> proper(x) 212.23/60.10 , proper(f(x)) -> f(proper(x)) 212.23/60.10 , proper(c()) -> ok(c()) } 212.23/60.10 Obligation: 212.23/60.10 derivational complexity 212.23/60.10 Answer: 212.23/60.10 YES(O(1),O(n^2)) 212.23/60.10 212.23/60.10 We use the processor 'matrix interpretation of dimension 2' to 212.23/60.10 orient following rules strictly. 212.23/60.10 212.23/60.10 Trs: { f(found(x)) -> found(f(x)) } 212.23/60.10 212.23/60.10 The induced complexity on above rules (modulo remaining rules) is 212.23/60.10 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.23/60.10 component(s). 212.23/60.10 212.23/60.10 Sub-proof: 212.23/60.10 ---------- 212.23/60.10 TcT has computed the following triangular matrix interpretation. 212.23/60.10 212.23/60.10 [active](x1) = [1 0] x1 + [0] 212.23/60.10 [0 1] [0] 212.23/60.10 212.23/60.10 [f](x1) = [1 1] x1 + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 212.23/60.10 [mark](x1) = [1 1] x1 + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 212.23/60.10 [top](x1) = [1 0] x1 + [0] 212.23/60.10 [0 0] [0] 212.23/60.10 212.23/60.10 [c] = [0] 212.23/60.10 [0] 212.23/60.10 212.23/60.10 [check](x1) = [1 1] x1 + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 212.23/60.10 [start](x1) = [1 0] x1 + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 212.23/60.10 [match](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 212.23/60.10 [0 0] [0 1] [0] 212.23/60.10 212.23/60.10 [X] = [0] 212.23/60.10 [0] 212.23/60.10 212.23/60.10 [proper](x1) = [1 0] x1 + [0] 212.23/60.10 [0 1] [0] 212.23/60.10 212.23/60.10 [ok](x1) = [1 0] x1 + [0] 212.23/60.10 [0 1] [0] 212.23/60.10 212.23/60.10 [found](x1) = [1 0] x1 + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 212.23/60.10 The order satisfies the following ordering constraints: 212.23/60.10 212.23/60.10 [active(f(x))] = [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 >= [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 = [f(active(x))] 212.23/60.10 212.23/60.10 [active(f(x))] = [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 >= [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 = [mark(x)] 212.23/60.10 212.23/60.10 [f(mark(x))] = [1 2] x + [1] 212.23/60.10 [0 1] [2] 212.23/60.10 >= [1 2] x + [1] 212.23/60.10 [0 1] [2] 212.23/60.10 = [mark(f(x))] 212.23/60.10 212.23/60.10 [f(ok(x))] = [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 >= [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 = [ok(f(x))] 212.23/60.10 212.23/60.10 [f(found(x))] = [1 1] x + [1] 212.23/60.10 [0 1] [2] 212.23/60.10 > [1 1] x + [0] 212.23/60.10 [0 1] [2] 212.23/60.10 = [found(f(x))] 212.23/60.10 212.23/60.10 [top(active(c()))] = [0] 212.23/60.10 [0] 212.23/60.10 >= [0] 212.23/60.10 [0] 212.23/60.10 = [top(mark(c()))] 212.23/60.10 212.23/60.10 [top(mark(x))] = [1 1] x + [0] 212.23/60.10 [0 0] [0] 212.23/60.10 >= [1 1] x + [0] 212.23/60.10 [0 0] [0] 212.23/60.10 = [top(check(x))] 212.23/60.10 212.23/60.10 [top(found(x))] = [1 0] x + [0] 212.23/60.10 [0 0] [0] 212.23/60.10 >= [1 0] x + [0] 212.23/60.10 [0 0] [0] 212.23/60.10 = [top(active(x))] 212.23/60.10 212.23/60.10 [check(x)] = [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 >= [1 0] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 = [start(match(f(X()), x))] 212.23/60.10 212.23/60.10 [check(f(x))] = [1 2] x + [1] 212.23/60.10 [0 1] [2] 212.23/60.10 >= [1 2] x + [1] 212.23/60.10 [0 1] [2] 212.23/60.10 = [f(check(x))] 212.23/60.10 212.23/60.10 [start(ok(x))] = [1 0] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 >= [1 0] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 = [found(x)] 212.23/60.10 212.23/60.10 [match(f(x), f(y))] = [1 1] x + [1 1] y + [0] 212.23/60.10 [0 0] [0 1] [1] 212.23/60.10 >= [1 0] x + [1 1] y + [0] 212.23/60.10 [0 0] [0 1] [1] 212.23/60.10 = [f(match(x, y))] 212.23/60.10 212.23/60.10 [match(X(), x)] = [1 0] x + [0] 212.23/60.10 [0 1] [0] 212.23/60.10 >= [1 0] x + [0] 212.23/60.10 [0 1] [0] 212.23/60.10 = [proper(x)] 212.23/60.10 212.23/60.10 [proper(f(x))] = [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 >= [1 1] x + [0] 212.23/60.10 [0 1] [1] 212.23/60.10 = [f(proper(x))] 212.23/60.10 212.23/60.10 [proper(c())] = [0] 212.23/60.10 [0] 212.23/60.10 >= [0] 212.23/60.10 [0] 212.23/60.10 = [ok(c())] 212.23/60.10 212.23/60.10 212.23/60.10 We return to the main proof. 212.23/60.10 212.23/60.10 We are left with following problem, upon which TcT provides the 212.23/60.10 certificate YES(O(1),O(n^2)). 212.23/60.10 212.23/60.10 Strict Trs: { top(mark(x)) -> top(check(x)) } 212.23/60.10 Weak Trs: 212.23/60.10 { active(f(x)) -> f(active(x)) 212.23/60.10 , active(f(x)) -> mark(x) 212.23/60.10 , f(mark(x)) -> mark(f(x)) 212.23/60.10 , f(ok(x)) -> ok(f(x)) 212.23/60.10 , f(found(x)) -> found(f(x)) 212.23/60.10 , top(active(c())) -> top(mark(c())) 212.23/60.10 , top(found(x)) -> top(active(x)) 212.23/60.10 , check(x) -> start(match(f(X()), x)) 212.23/60.10 , check(f(x)) -> f(check(x)) 212.23/60.10 , start(ok(x)) -> found(x) 212.23/60.10 , match(f(x), f(y)) -> f(match(x, y)) 212.23/60.10 , match(X(), x) -> proper(x) 212.23/60.10 , proper(f(x)) -> f(proper(x)) 212.23/60.10 , proper(c()) -> ok(c()) } 212.23/60.10 Obligation: 212.23/60.10 derivational complexity 212.23/60.10 Answer: 212.23/60.10 YES(O(1),O(n^2)) 212.23/60.10 212.23/60.10 We use the processor 'matrix interpretation of dimension 3' to 212.23/60.10 orient following rules strictly. 212.23/60.10 212.23/60.10 Trs: { top(mark(x)) -> top(check(x)) } 212.23/60.10 212.23/60.10 The induced complexity on above rules (modulo remaining rules) is 212.23/60.10 YES(?,O(n^2)) . These rules are moved into the corresponding weak 212.23/60.10 component(s). 212.23/60.10 212.23/60.10 Sub-proof: 212.23/60.10 ---------- 212.23/60.10 TcT has computed the following triangular matrix interpretation. 212.23/60.10 Note that the diagonal of the component-wise maxima of 212.23/60.10 interpretation-entries contains no more than 2 non-zero entries. 212.23/60.10 212.23/60.10 [1 0 1] [0] 212.23/60.10 [active](x1) = [0 1 0] x1 + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 212.23/60.10 [1 0 1] [0] 212.23/60.10 [f](x1) = [0 0 0] x1 + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 212.23/60.10 [1 0 1] [1] 212.23/60.10 [mark](x1) = [0 0 0] x1 + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 212.23/60.10 [1 2 0] [0] 212.23/60.10 [top](x1) = [0 0 0] x1 + [0] 212.23/60.10 [0 0 0] [0] 212.23/60.10 212.23/60.10 [0] 212.23/60.10 [c] = [2] 212.23/60.10 [0] 212.23/60.10 212.23/60.10 [1 0 1] [0] 212.23/60.10 [check](x1) = [0 0 0] x1 + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 212.23/60.10 [1 2 0] [0] 212.23/60.10 [start](x1) = [0 0 0] x1 + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 212.23/60.10 [1 0 0] [1 0 1] [0] 212.23/60.10 [match](x1, x2) = [0 1 0] x1 + [0 0 0] x2 + [0] 212.23/60.10 [0 0 0] [0 0 0] [1] 212.23/60.10 212.23/60.10 [0] 212.23/60.10 [X] = [2] 212.23/60.10 [0] 212.23/60.10 212.23/60.10 [1 0 1] [0] 212.23/60.10 [proper](x1) = [0 0 0] x1 + [2] 212.23/60.10 [0 0 0] [1] 212.23/60.10 212.23/60.10 [1 0 1] [0] 212.23/60.10 [ok](x1) = [0 1 0] x1 + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 212.23/60.10 [1 2 1] [0] 212.23/60.10 [found](x1) = [0 0 0] x1 + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 212.23/60.10 The order satisfies the following ordering constraints: 212.23/60.10 212.23/60.10 [active(f(x))] = [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [f(active(x))] 212.23/60.10 212.23/60.10 [active(f(x))] = [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [mark(x)] 212.23/60.10 212.23/60.10 [f(mark(x))] = [1 0 1] [2] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [2] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [mark(f(x))] 212.23/60.10 212.23/60.10 [f(ok(x))] = [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [ok(f(x))] 212.23/60.10 212.23/60.10 [f(found(x))] = [1 2 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [found(f(x))] 212.23/60.10 212.23/60.10 [top(active(c()))] = [4] 212.23/60.10 [0] 212.23/60.10 [0] 212.23/60.10 > [1] 212.23/60.10 [0] 212.23/60.10 [0] 212.23/60.10 = [top(mark(c()))] 212.23/60.10 212.23/60.10 [top(mark(x))] = [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [0] 212.23/60.10 > [1 0 1] [0] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [0] 212.23/60.10 = [top(check(x))] 212.23/60.10 212.23/60.10 [top(found(x))] = [1 2 1] [0] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [0] 212.23/60.10 >= [1 2 1] [0] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [0] 212.23/60.10 = [top(active(x))] 212.23/60.10 212.23/60.10 [check(x)] = [1 0 1] [0] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [0] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [start(match(f(X()), x))] 212.23/60.10 212.23/60.10 [check(f(x))] = [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [f(check(x))] 212.23/60.10 212.23/60.10 [start(ok(x))] = [1 2 1] [0] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 2 1] [0] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [found(x)] 212.23/60.10 212.23/60.10 [match(f(x), f(y))] = [1 0 1] [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0 0 0] y + [0] 212.23/60.10 [0 0 0] [0 0 0] [1] 212.23/60.10 >= [1 0 0] [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0 0 0] y + [0] 212.23/60.10 [0 0 0] [0 0 0] [1] 212.23/60.10 = [f(match(x, y))] 212.23/60.10 212.23/60.10 [match(X(), x)] = [1 0 1] [0] 212.23/60.10 [0 0 0] x + [2] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [0] 212.23/60.10 [0 0 0] x + [2] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [proper(x)] 212.23/60.10 212.23/60.10 [proper(f(x))] = [1 0 1] [1] 212.23/60.10 [0 0 0] x + [2] 212.23/60.10 [0 0 0] [1] 212.23/60.10 >= [1 0 1] [1] 212.23/60.10 [0 0 0] x + [0] 212.23/60.10 [0 0 0] [1] 212.23/60.10 = [f(proper(x))] 212.23/60.10 212.23/60.10 [proper(c())] = [0] 212.23/60.10 [2] 212.23/60.10 [1] 212.23/60.10 >= [0] 212.23/60.10 [2] 212.23/60.10 [1] 212.23/60.10 = [ok(c())] 212.23/60.10 212.23/60.10 212.23/60.10 We return to the main proof. 212.23/60.10 212.23/60.10 We are left with following problem, upon which TcT provides the 212.23/60.10 certificate YES(O(1),O(1)). 212.23/60.10 212.23/60.10 Weak Trs: 212.23/60.10 { active(f(x)) -> f(active(x)) 212.23/60.10 , active(f(x)) -> mark(x) 212.23/60.10 , f(mark(x)) -> mark(f(x)) 212.23/60.10 , f(ok(x)) -> ok(f(x)) 212.23/60.10 , f(found(x)) -> found(f(x)) 212.23/60.10 , top(active(c())) -> top(mark(c())) 212.23/60.10 , top(mark(x)) -> top(check(x)) 212.23/60.10 , top(found(x)) -> top(active(x)) 212.23/60.10 , check(x) -> start(match(f(X()), x)) 212.23/60.10 , check(f(x)) -> f(check(x)) 212.23/60.10 , start(ok(x)) -> found(x) 212.23/60.10 , match(f(x), f(y)) -> f(match(x, y)) 212.23/60.10 , match(X(), x) -> proper(x) 212.23/60.10 , proper(f(x)) -> f(proper(x)) 212.23/60.10 , proper(c()) -> ok(c()) } 212.23/60.10 Obligation: 212.23/60.10 derivational complexity 212.23/60.10 Answer: 212.23/60.10 YES(O(1),O(1)) 212.23/60.10 212.23/60.10 Empty rules are trivially bounded 212.23/60.10 212.23/60.10 Hurray, we answered YES(O(1),O(n^2)) 212.23/60.12 EOF