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