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