YES(O(1),O(n^2)) 519.14/148.09 YES(O(1),O(n^2)) 519.14/148.09 519.14/148.09 We are left with following problem, upon which TcT provides the 519.14/148.09 certificate YES(O(1),O(n^2)). 519.14/148.09 519.14/148.09 Strict Trs: 519.14/148.09 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.14/148.09 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.14/148.09 , active(b()) -> mark(a()) 519.14/148.09 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.14/148.09 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.14/148.09 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.14/148.09 , proper(a()) -> ok(a()) 519.14/148.09 , proper(b()) -> ok(b()) 519.14/148.09 , top(mark(X)) -> top(proper(X)) 519.14/148.09 , top(ok(X)) -> top(active(X)) } 519.14/148.09 Obligation: 519.14/148.09 innermost runtime complexity 519.14/148.09 Answer: 519.14/148.09 YES(O(1),O(n^2)) 519.14/148.09 519.14/148.09 We add the following dependency tuples: 519.14/148.09 519.14/148.09 Strict DPs: 519.14/148.09 { active^#(f(X1, X2, X3)) -> 519.14/148.09 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.14/148.09 , active^#(f(a(), X, X)) -> c_2(f^#(X, b(), b())) 519.14/148.09 , active^#(b()) -> c_3() 519.14/148.09 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.14/148.09 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.14/148.09 , proper^#(f(X1, X2, X3)) -> 519.14/148.09 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.14/148.09 proper^#(X1), 519.14/148.09 proper^#(X2), 519.14/148.09 proper^#(X3)) 519.14/148.09 , proper^#(a()) -> c_7() 519.14/148.09 , proper^#(b()) -> c_8() 519.14/148.09 , top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.14/148.09 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.09 519.14/148.09 and mark the set of starting terms. 519.14/148.09 519.14/148.09 We are left with following problem, upon which TcT provides the 519.14/148.09 certificate YES(O(1),O(n^2)). 519.14/148.09 519.14/148.09 Strict DPs: 519.14/148.09 { active^#(f(X1, X2, X3)) -> 519.14/148.09 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.14/148.09 , active^#(f(a(), X, X)) -> c_2(f^#(X, b(), b())) 519.14/148.09 , active^#(b()) -> c_3() 519.14/148.09 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.14/148.09 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.14/148.09 , proper^#(f(X1, X2, X3)) -> 519.14/148.09 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.14/148.09 proper^#(X1), 519.14/148.09 proper^#(X2), 519.14/148.09 proper^#(X3)) 519.14/148.09 , proper^#(a()) -> c_7() 519.14/148.09 , proper^#(b()) -> c_8() 519.14/148.09 , top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.14/148.09 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.09 Weak Trs: 519.14/148.09 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.14/148.09 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.14/148.09 , active(b()) -> mark(a()) 519.14/148.09 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.14/148.09 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.14/148.09 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.14/148.09 , proper(a()) -> ok(a()) 519.14/148.09 , proper(b()) -> ok(b()) 519.14/148.09 , top(mark(X)) -> top(proper(X)) 519.14/148.09 , top(ok(X)) -> top(active(X)) } 519.14/148.09 Obligation: 519.14/148.09 innermost runtime complexity 519.14/148.09 Answer: 519.14/148.09 YES(O(1),O(n^2)) 519.14/148.09 519.14/148.09 We estimate the number of application of {2,3,7,8} by applications 519.14/148.09 of Pre({2,3,7,8}) = {1,6,9,10}. Here rules are labeled as follows: 519.14/148.09 519.14/148.09 DPs: 519.14/148.09 { 1: active^#(f(X1, X2, X3)) -> 519.14/148.09 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.14/148.09 , 2: active^#(f(a(), X, X)) -> c_2(f^#(X, b(), b())) 519.14/148.09 , 3: active^#(b()) -> c_3() 519.14/148.09 , 4: f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.14/148.09 , 5: f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.14/148.09 , 6: proper^#(f(X1, X2, X3)) -> 519.14/148.09 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.14/148.09 proper^#(X1), 519.14/148.09 proper^#(X2), 519.14/148.09 proper^#(X3)) 519.14/148.09 , 7: proper^#(a()) -> c_7() 519.14/148.09 , 8: proper^#(b()) -> c_8() 519.14/148.09 , 9: top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.14/148.09 , 10: top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.09 519.14/148.09 We are left with following problem, upon which TcT provides the 519.14/148.09 certificate YES(O(1),O(n^2)). 519.14/148.09 519.14/148.09 Strict DPs: 519.14/148.09 { active^#(f(X1, X2, X3)) -> 519.14/148.09 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.14/148.09 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.14/148.09 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.14/148.09 , proper^#(f(X1, X2, X3)) -> 519.14/148.09 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.14/148.09 proper^#(X1), 519.14/148.09 proper^#(X2), 519.14/148.09 proper^#(X3)) 519.14/148.09 , top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.14/148.09 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.09 Weak DPs: 519.14/148.09 { active^#(f(a(), X, X)) -> c_2(f^#(X, b(), b())) 519.14/148.09 , active^#(b()) -> c_3() 519.14/148.09 , proper^#(a()) -> c_7() 519.14/148.09 , proper^#(b()) -> c_8() } 519.14/148.09 Weak Trs: 519.14/148.09 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.14/148.09 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.14/148.09 , active(b()) -> mark(a()) 519.14/148.09 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.14/148.09 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.14/148.09 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.14/148.09 , proper(a()) -> ok(a()) 519.14/148.09 , proper(b()) -> ok(b()) 519.14/148.09 , top(mark(X)) -> top(proper(X)) 519.14/148.09 , top(ok(X)) -> top(active(X)) } 519.14/148.09 Obligation: 519.14/148.09 innermost runtime complexity 519.14/148.09 Answer: 519.14/148.09 YES(O(1),O(n^2)) 519.14/148.09 519.14/148.09 The following weak DPs constitute a sub-graph of the DG that is 519.14/148.09 closed under successors. The DPs are removed. 519.14/148.09 519.14/148.09 { active^#(f(a(), X, X)) -> c_2(f^#(X, b(), b())) 519.14/148.09 , active^#(b()) -> c_3() 519.14/148.09 , proper^#(a()) -> c_7() 519.14/148.09 , proper^#(b()) -> c_8() } 519.14/148.09 519.14/148.09 We are left with following problem, upon which TcT provides the 519.14/148.09 certificate YES(O(1),O(n^2)). 519.14/148.09 519.14/148.09 Strict DPs: 519.14/148.09 { active^#(f(X1, X2, X3)) -> 519.14/148.09 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.14/148.09 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.14/148.09 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.14/148.09 , proper^#(f(X1, X2, X3)) -> 519.14/148.09 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.14/148.09 proper^#(X1), 519.14/148.09 proper^#(X2), 519.14/148.09 proper^#(X3)) 519.14/148.09 , top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.14/148.09 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.09 Weak Trs: 519.14/148.09 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.14/148.09 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.14/148.09 , active(b()) -> mark(a()) 519.14/148.09 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.14/148.09 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.14/148.09 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.14/148.09 , proper(a()) -> ok(a()) 519.14/148.09 , proper(b()) -> ok(b()) 519.14/148.09 , top(mark(X)) -> top(proper(X)) 519.14/148.09 , top(ok(X)) -> top(active(X)) } 519.14/148.09 Obligation: 519.14/148.09 innermost runtime complexity 519.14/148.09 Answer: 519.14/148.09 YES(O(1),O(n^2)) 519.14/148.09 519.14/148.09 We replace rewrite rules by usable rules: 519.14/148.09 519.14/148.09 Weak Usable Rules: 519.14/148.09 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.14/148.09 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.14/148.09 , active(b()) -> mark(a()) 519.14/148.09 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.14/148.09 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.14/148.09 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.14/148.09 , proper(a()) -> ok(a()) 519.14/148.09 , proper(b()) -> ok(b()) } 519.14/148.09 519.14/148.09 We are left with following problem, upon which TcT provides the 519.14/148.09 certificate YES(O(1),O(n^2)). 519.14/148.09 519.14/148.09 Strict DPs: 519.14/148.09 { active^#(f(X1, X2, X3)) -> 519.14/148.09 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.14/148.09 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.14/148.09 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.14/148.09 , proper^#(f(X1, X2, X3)) -> 519.14/148.09 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.14/148.09 proper^#(X1), 519.14/148.09 proper^#(X2), 519.14/148.09 proper^#(X3)) 519.14/148.09 , top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.14/148.09 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.09 Weak Trs: 519.14/148.09 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.14/148.09 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.14/148.09 , active(b()) -> mark(a()) 519.14/148.09 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.14/148.09 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.14/148.09 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.14/148.09 , proper(a()) -> ok(a()) 519.14/148.09 , proper(b()) -> ok(b()) } 519.14/148.09 Obligation: 519.14/148.09 innermost runtime complexity 519.14/148.09 Answer: 519.14/148.09 YES(O(1),O(n^2)) 519.14/148.09 519.14/148.09 We decompose the input problem according to the dependency graph 519.14/148.09 into the upper component 519.14/148.09 519.14/148.09 { top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.14/148.09 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.09 519.14/148.09 and lower component 519.14/148.09 519.14/148.09 { active^#(f(X1, X2, X3)) -> 519.14/148.09 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.14/148.09 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.14/148.09 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.14/148.09 , proper^#(f(X1, X2, X3)) -> 519.14/148.09 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.14/148.09 proper^#(X1), 519.14/148.09 proper^#(X2), 519.14/148.09 proper^#(X3)) } 519.14/148.09 519.14/148.09 Further, following extension rules are added to the lower 519.14/148.09 component. 519.14/148.09 519.14/148.09 { top^#(mark(X)) -> proper^#(X) 519.14/148.09 , top^#(mark(X)) -> top^#(proper(X)) 519.14/148.09 , top^#(ok(X)) -> active^#(X) 519.14/148.09 , top^#(ok(X)) -> top^#(active(X)) } 519.14/148.09 519.14/148.09 TcT solves the upper component with certificate YES(O(1),O(n^1)). 519.14/148.09 519.14/148.09 Sub-proof: 519.14/148.09 ---------- 519.14/148.09 We are left with following problem, upon which TcT provides the 519.14/148.09 certificate YES(O(1),O(n^1)). 519.14/148.09 519.14/148.09 Strict DPs: 519.14/148.09 { top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.14/148.09 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.09 Weak Trs: 519.14/148.09 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.14/148.09 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.14/148.09 , active(b()) -> mark(a()) 519.14/148.09 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.14/148.09 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.14/148.09 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.14/148.09 , proper(a()) -> ok(a()) 519.14/148.09 , proper(b()) -> ok(b()) } 519.14/148.09 Obligation: 519.14/148.09 innermost runtime complexity 519.14/148.09 Answer: 519.14/148.09 YES(O(1),O(n^1)) 519.14/148.09 519.14/148.09 We use the processor 'matrix interpretation of dimension 2' to 519.14/148.09 orient following rules strictly. 519.14/148.09 519.14/148.09 DPs: 519.14/148.09 { 1: top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) } 519.14/148.09 Trs: { active(f(a(), X, X)) -> mark(f(X, b(), b())) } 519.14/148.09 519.14/148.09 Sub-proof: 519.14/148.09 ---------- 519.14/148.09 The following argument positions are usable: 519.14/148.09 Uargs(c_9) = {1}, Uargs(c_10) = {1} 519.14/148.09 519.14/148.09 TcT has computed the following constructor-based matrix 519.14/148.09 interpretation satisfying not(EDA) and not(IDA(1)). 519.14/148.09 519.14/148.09 [active](x1) = [0 1] x1 + [0] 519.14/148.09 [1 0] [0] 519.14/148.09 519.14/148.09 [f](x1, x2, x3) = [1 1] x1 + [1 0] x2 + [1 1] x3 + [0] 519.14/148.09 [1 1] [0 1] [1 1] [0] 519.14/148.09 519.14/148.09 [a] = [0] 519.14/148.09 [3] 519.14/148.09 519.14/148.09 [mark](x1) = [0 0] x1 + [0] 519.14/148.09 [1 0] [1] 519.14/148.09 519.14/148.09 [b] = [1] 519.14/148.09 [0] 519.14/148.09 519.14/148.09 [proper](x1) = [0 1] x1 + [0] 519.14/148.09 [1 0] [0] 519.14/148.09 519.14/148.09 [ok](x1) = [0 1] x1 + [0] 519.14/148.09 [1 0] [0] 519.14/148.09 519.14/148.09 [active^#](x1) = [0] 519.14/148.09 [0] 519.14/148.09 519.14/148.09 [proper^#](x1) = [0] 519.14/148.09 [0] 519.14/148.09 519.14/148.09 [top^#](x1) = [0 4] x1 + [0] 519.14/148.09 [4 0] [4] 519.14/148.09 519.14/148.09 [c_9](x1, x2) = [1 0] x1 + [1] 519.14/148.09 [0 0] [3] 519.14/148.09 519.14/148.09 [c_10](x1, x2) = [1 0] x1 + [0] 519.14/148.09 [0 0] [3] 519.14/148.09 519.14/148.09 The order satisfies the following ordering constraints: 519.14/148.09 519.14/148.09 [active(f(X1, X2, X3))] = [1 1] X1 + [0 1] X2 + [1 1] X3 + [0] 519.14/148.09 [1 1] [1 0] [1 1] [0] 519.14/148.09 >= [1 1] X1 + [0 1] X2 + [1 1] X3 + [0] 519.14/148.09 [1 1] [1 0] [1 1] [0] 519.14/148.09 = [f(X1, active(X2), X3)] 519.14/148.09 519.14/148.09 [active(f(a(), X, X))] = [1 2] X + [3] 519.14/148.09 [2 1] [3] 519.14/148.09 > [0 0] X + [0] 519.14/148.09 [1 1] [3] 519.14/148.09 = [mark(f(X, b(), b()))] 519.14/148.09 519.14/148.09 [active(b())] = [0] 519.14/148.09 [1] 519.14/148.09 >= [0] 519.14/148.09 [1] 519.14/148.09 = [mark(a())] 519.14/148.09 519.14/148.09 [f(X1, mark(X2), X3)] = [1 1] X1 + [0 0] X2 + [1 1] X3 + [0] 519.14/148.09 [1 1] [1 0] [1 1] [1] 519.14/148.09 >= [0 0] X1 + [0 0] X2 + [0 0] X3 + [0] 519.14/148.09 [1 1] [1 0] [1 1] [1] 519.14/148.09 = [mark(f(X1, X2, X3))] 519.14/148.09 519.14/148.09 [f(ok(X1), ok(X2), ok(X3))] = [1 1] X1 + [0 1] X2 + [1 1] X3 + [0] 519.14/148.09 [1 1] [1 0] [1 1] [0] 519.14/148.09 >= [1 1] X1 + [0 1] X2 + [1 1] X3 + [0] 519.14/148.09 [1 1] [1 0] [1 1] [0] 519.14/148.09 = [ok(f(X1, X2, X3))] 519.14/148.09 519.14/148.09 [proper(f(X1, X2, X3))] = [1 1] X1 + [0 1] X2 + [1 1] X3 + [0] 519.14/148.09 [1 1] [1 0] [1 1] [0] 519.14/148.09 >= [1 1] X1 + [0 1] X2 + [1 1] X3 + [0] 519.14/148.09 [1 1] [1 0] [1 1] [0] 519.14/148.09 = [f(proper(X1), proper(X2), proper(X3))] 519.14/148.09 519.14/148.09 [proper(a())] = [3] 519.14/148.09 [0] 519.14/148.09 >= [3] 519.14/148.09 [0] 519.14/148.09 = [ok(a())] 519.14/148.09 519.14/148.09 [proper(b())] = [0] 519.14/148.09 [1] 519.14/148.09 >= [0] 519.14/148.09 [1] 519.14/148.09 = [ok(b())] 519.14/148.09 519.14/148.09 [top^#(mark(X))] = [4 0] X + [4] 519.14/148.09 [0 0] [4] 519.14/148.09 > [4 0] X + [1] 519.14/148.09 [0 0] [3] 519.14/148.09 = [c_9(top^#(proper(X)), proper^#(X))] 519.14/148.09 519.14/148.09 [top^#(ok(X))] = [4 0] X + [0] 519.14/148.09 [0 4] [4] 519.14/148.09 >= [4 0] X + [0] 519.14/148.09 [0 0] [3] 519.14/148.09 = [c_10(top^#(active(X)), active^#(X))] 519.14/148.09 519.14/148.09 519.14/148.09 The strictly oriented rules are moved into the weak component. 519.14/148.09 519.14/148.09 We are left with following problem, upon which TcT provides the 519.14/148.09 certificate YES(O(1),O(n^1)). 519.14/148.09 519.14/148.09 Strict DPs: { top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.10 Weak DPs: { top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) } 519.14/148.10 Weak Trs: 519.14/148.10 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.14/148.10 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.14/148.10 , active(b()) -> mark(a()) 519.14/148.10 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.14/148.10 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.14/148.10 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.14/148.10 , proper(a()) -> ok(a()) 519.14/148.10 , proper(b()) -> ok(b()) } 519.14/148.10 Obligation: 519.14/148.10 innermost runtime complexity 519.14/148.10 Answer: 519.14/148.10 YES(O(1),O(n^1)) 519.14/148.10 519.14/148.10 We use the processor 'matrix interpretation of dimension 2' to 519.14/148.10 orient following rules strictly. 519.14/148.10 519.14/148.10 DPs: 519.14/148.10 { 1: top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.14/148.10 Trs: 519.14/148.10 { active(b()) -> mark(a()) 519.14/148.10 , proper(a()) -> ok(a()) } 519.14/148.10 519.14/148.10 Sub-proof: 519.14/148.10 ---------- 519.14/148.10 The following argument positions are usable: 519.14/148.10 Uargs(c_9) = {1}, Uargs(c_10) = {1} 519.14/148.10 519.14/148.10 TcT has computed the following constructor-based matrix 519.14/148.10 interpretation satisfying not(EDA) and not(IDA(1)). 519.14/148.10 519.14/148.10 [active](x1) = [1 1] x1 + [0] 519.14/148.10 [0 0] [0] 519.14/148.10 519.14/148.10 [f](x1, x2, x3) = [0 4] x1 + [1 0] x2 + [0 3] x3 + [0] 519.14/148.10 [0 0] [0 1] [0 0] [0] 519.14/148.10 519.14/148.10 [a] = [0] 519.14/148.10 [3] 519.14/148.10 519.14/148.10 [mark](x1) = [1 2] x1 + [0] 519.14/148.10 [0 0] [0] 519.14/148.10 519.14/148.10 [b] = [7] 519.14/148.10 [1] 519.14/148.10 519.14/148.10 [proper](x1) = [1 1] x1 + [0] 519.14/148.10 [0 1] [0] 519.14/148.10 519.14/148.10 [ok](x1) = [1 0] x1 + [1] 519.14/148.10 [0 1] [0] 519.14/148.10 519.14/148.10 [active^#](x1) = [0] 519.14/148.10 [0] 519.14/148.10 519.14/148.10 [proper^#](x1) = [0] 519.14/148.10 [0] 519.14/148.10 519.14/148.10 [top^#](x1) = [1 1] x1 + [0] 519.14/148.10 [0 0] [4] 519.14/148.10 519.14/148.10 [c_9](x1, x2) = [1 0] x1 + [0] 519.14/148.10 [0 0] [3] 519.14/148.10 519.14/148.10 [c_10](x1, x2) = [1 0] x1 + [0] 519.14/148.10 [0 0] [3] 519.14/148.10 519.14/148.10 The order satisfies the following ordering constraints: 519.14/148.10 519.14/148.10 [active(f(X1, X2, X3))] = [0 4] X1 + [1 1] X2 + [0 3] X3 + [0] 519.14/148.10 [0 0] [0 0] [0 0] [0] 519.14/148.10 >= [0 4] X1 + [1 1] X2 + [0 3] X3 + [0] 519.14/148.10 [0 0] [0 0] [0 0] [0] 519.14/148.10 = [f(X1, active(X2), X3)] 519.14/148.10 519.14/148.10 [active(f(a(), X, X))] = [1 4] X + [12] 519.14/148.10 [0 0] [0] 519.14/148.10 >= [0 4] X + [12] 519.14/148.10 [0 0] [0] 519.14/148.10 = [mark(f(X, b(), b()))] 519.14/148.10 519.14/148.10 [active(b())] = [8] 519.14/148.10 [0] 519.14/148.10 > [6] 519.14/148.10 [0] 519.14/148.10 = [mark(a())] 519.14/148.10 519.14/148.10 [f(X1, mark(X2), X3)] = [0 4] X1 + [1 2] X2 + [0 3] X3 + [0] 519.14/148.10 [0 0] [0 0] [0 0] [0] 519.14/148.10 >= [0 4] X1 + [1 2] X2 + [0 3] X3 + [0] 519.14/148.10 [0 0] [0 0] [0 0] [0] 519.14/148.10 = [mark(f(X1, X2, X3))] 519.14/148.10 519.14/148.10 [f(ok(X1), ok(X2), ok(X3))] = [0 4] X1 + [1 0] X2 + [0 3] X3 + [1] 519.14/148.10 [0 0] [0 1] [0 0] [0] 519.14/148.10 >= [0 4] X1 + [1 0] X2 + [0 3] X3 + [1] 519.14/148.10 [0 0] [0 1] [0 0] [0] 519.14/148.10 = [ok(f(X1, X2, X3))] 519.14/148.10 519.14/148.10 [proper(f(X1, X2, X3))] = [0 4] X1 + [1 1] X2 + [0 3] X3 + [0] 519.14/148.10 [0 0] [0 1] [0 0] [0] 519.14/148.10 >= [0 4] X1 + [1 1] X2 + [0 3] X3 + [0] 519.14/148.10 [0 0] [0 1] [0 0] [0] 519.14/148.10 = [f(proper(X1), proper(X2), proper(X3))] 519.14/148.10 519.14/148.10 [proper(a())] = [3] 519.14/148.10 [3] 519.14/148.10 > [1] 519.14/148.10 [3] 519.14/148.10 = [ok(a())] 519.14/148.10 519.14/148.10 [proper(b())] = [8] 519.14/148.10 [1] 519.14/148.10 >= [8] 519.14/148.10 [1] 519.14/148.10 = [ok(b())] 519.14/148.10 519.14/148.10 [top^#(mark(X))] = [1 2] X + [0] 519.14/148.10 [0 0] [4] 519.14/148.10 >= [1 2] X + [0] 519.14/148.10 [0 0] [3] 519.14/148.10 = [c_9(top^#(proper(X)), proper^#(X))] 519.14/148.10 519.14/148.10 [top^#(ok(X))] = [1 1] X + [1] 519.14/148.10 [0 0] [4] 519.14/148.10 > [1 1] X + [0] 519.14/148.10 [0 0] [3] 519.14/148.10 = [c_10(top^#(active(X)), active^#(X))] 519.14/148.10 519.14/148.10 519.14/148.10 The strictly oriented rules are moved into the weak component. 519.14/148.10 519.14/148.10 We are left with following problem, upon which TcT provides the 519.14/148.10 certificate YES(O(1),O(1)). 519.14/148.10 519.14/148.10 Weak DPs: 519.14/148.10 { top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.29/148.10 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.29/148.10 Weak Trs: 519.29/148.10 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.10 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.10 , active(b()) -> mark(a()) 519.29/148.10 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.10 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.10 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.10 , proper(a()) -> ok(a()) 519.29/148.10 , proper(b()) -> ok(b()) } 519.29/148.10 Obligation: 519.29/148.10 innermost runtime complexity 519.29/148.10 Answer: 519.29/148.10 YES(O(1),O(1)) 519.29/148.10 519.29/148.10 The following weak DPs constitute a sub-graph of the DG that is 519.29/148.10 closed under successors. The DPs are removed. 519.29/148.10 519.29/148.10 { top^#(mark(X)) -> c_9(top^#(proper(X)), proper^#(X)) 519.29/148.10 , top^#(ok(X)) -> c_10(top^#(active(X)), active^#(X)) } 519.29/148.10 519.29/148.10 We are left with following problem, upon which TcT provides the 519.29/148.10 certificate YES(O(1),O(1)). 519.29/148.10 519.29/148.10 Weak Trs: 519.29/148.10 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.10 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.10 , active(b()) -> mark(a()) 519.29/148.10 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.10 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.10 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.10 , proper(a()) -> ok(a()) 519.29/148.10 , proper(b()) -> ok(b()) } 519.29/148.10 Obligation: 519.29/148.10 innermost runtime complexity 519.29/148.10 Answer: 519.29/148.10 YES(O(1),O(1)) 519.29/148.10 519.29/148.10 No rule is usable, rules are removed from the input problem. 519.29/148.10 519.29/148.10 We are left with following problem, upon which TcT provides the 519.29/148.10 certificate YES(O(1),O(1)). 519.29/148.10 519.29/148.10 Rules: Empty 519.29/148.10 Obligation: 519.29/148.10 innermost runtime complexity 519.29/148.10 Answer: 519.29/148.10 YES(O(1),O(1)) 519.29/148.10 519.29/148.10 Empty rules are trivially bounded 519.29/148.10 519.29/148.10 We return to the main proof. 519.29/148.10 519.29/148.10 We are left with following problem, upon which TcT provides the 519.29/148.10 certificate YES(O(1),O(n^1)). 519.29/148.10 519.29/148.10 Strict DPs: 519.29/148.10 { active^#(f(X1, X2, X3)) -> 519.29/148.10 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.29/148.10 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.29/148.10 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.29/148.10 , proper^#(f(X1, X2, X3)) -> 519.29/148.10 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.29/148.10 proper^#(X1), 519.29/148.10 proper^#(X2), 519.29/148.10 proper^#(X3)) } 519.29/148.10 Weak DPs: 519.29/148.10 { top^#(mark(X)) -> proper^#(X) 519.29/148.10 , top^#(mark(X)) -> top^#(proper(X)) 519.29/148.10 , top^#(ok(X)) -> active^#(X) 519.29/148.10 , top^#(ok(X)) -> top^#(active(X)) } 519.29/148.10 Weak Trs: 519.29/148.10 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.10 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.10 , active(b()) -> mark(a()) 519.29/148.10 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.10 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.10 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.10 , proper(a()) -> ok(a()) 519.29/148.10 , proper(b()) -> ok(b()) } 519.29/148.10 Obligation: 519.29/148.10 innermost runtime complexity 519.29/148.10 Answer: 519.29/148.10 YES(O(1),O(n^1)) 519.29/148.10 519.29/148.10 We use the processor 'matrix interpretation of dimension 2' to 519.29/148.10 orient following rules strictly. 519.29/148.10 519.29/148.10 DPs: 519.29/148.10 { 1: active^#(f(X1, X2, X3)) -> 519.29/148.10 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.29/148.10 , 3: f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) } 519.29/148.10 519.29/148.10 Sub-proof: 519.29/148.10 ---------- 519.29/148.10 The following argument positions are usable: 519.29/148.10 Uargs(c_1) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, 519.29/148.10 Uargs(c_6) = {1, 2, 3, 4} 519.29/148.10 519.29/148.10 TcT has computed the following constructor-based matrix 519.29/148.10 interpretation satisfying not(EDA) and not(IDA(1)). 519.29/148.10 519.29/148.10 [active](x1) = [1 0] x1 + [0] 519.29/148.10 [0 1] [0] 519.29/148.10 519.29/148.10 [f](x1, x2, x3) = [5 0] x1 + [4 0] x2 + [2 0] x3 + [1] 519.29/148.10 [0 3] [0 1] [0 0] [0] 519.29/148.10 519.29/148.10 [a] = [0] 519.29/148.10 [0] 519.29/148.10 519.29/148.10 [mark](x1) = [1 0] x1 + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 519.29/148.10 [b] = [0] 519.29/148.10 [0] 519.29/148.10 519.29/148.10 [proper](x1) = [1 0] x1 + [0] 519.29/148.10 [3 0] [1] 519.29/148.10 519.29/148.10 [ok](x1) = [1 1] x1 + [0] 519.29/148.10 [0 0] [1] 519.29/148.10 519.29/148.10 [active^#](x1) = [2 3] x1 + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 519.29/148.10 [c_1](x1, x2) = [2 1] x1 + [1 0] x2 + [1] 519.29/148.10 [0 0] [0 0] [0] 519.29/148.10 519.29/148.10 [f^#](x1, x2, x3) = [1 1] x1 + [0] 519.29/148.10 [0 2] [0] 519.29/148.10 519.29/148.10 [c_4](x1) = [1 0] x1 + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 519.29/148.10 [c_5](x1) = [1 0] x1 + [0] 519.29/148.10 [0 0] [1] 519.29/148.10 519.29/148.10 [proper^#](x1) = [1 0] x1 + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 519.29/148.10 [c_6](x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [2 519.29/148.10 0] x4 + [0] 519.29/148.10 [0 0] [0 0] [0 0] [0 519.29/148.10 0] [0] 519.29/148.10 519.29/148.10 [top^#](x1) = [3 0] x1 + [0] 519.29/148.10 [4 0] [0] 519.29/148.10 519.29/148.10 The order satisfies the following ordering constraints: 519.29/148.10 519.29/148.10 [active(f(X1, X2, X3))] = [5 0] X1 + [4 0] X2 + [2 0] X3 + [1] 519.29/148.10 [0 3] [0 1] [0 0] [0] 519.29/148.10 >= [5 0] X1 + [4 0] X2 + [2 0] X3 + [1] 519.29/148.10 [0 3] [0 1] [0 0] [0] 519.29/148.10 = [f(X1, active(X2), X3)] 519.29/148.10 519.29/148.10 [active(f(a(), X, X))] = [6 0] X + [1] 519.29/148.10 [0 1] [0] 519.29/148.10 >= [5 0] X + [1] 519.29/148.10 [0 0] [0] 519.29/148.10 = [mark(f(X, b(), b()))] 519.29/148.10 519.29/148.10 [active(b())] = [0] 519.29/148.10 [0] 519.29/148.10 >= [0] 519.29/148.10 [0] 519.29/148.10 = [mark(a())] 519.29/148.10 519.29/148.10 [f(X1, mark(X2), X3)] = [5 0] X1 + [4 0] X2 + [2 0] X3 + [1] 519.29/148.10 [0 3] [0 0] [0 0] [0] 519.29/148.10 >= [5 0] X1 + [4 0] X2 + [2 0] X3 + [1] 519.29/148.10 [0 0] [0 0] [0 0] [0] 519.29/148.10 = [mark(f(X1, X2, X3))] 519.29/148.10 519.29/148.10 [f(ok(X1), ok(X2), ok(X3))] = [5 5] X1 + [4 4] X2 + [2 2] X3 + [1] 519.29/148.10 [0 0] [0 0] [0 0] [4] 519.29/148.10 >= [5 3] X1 + [4 1] X2 + [2 0] X3 + [1] 519.29/148.10 [0 0] [0 0] [0 0] [1] 519.29/148.10 = [ok(f(X1, X2, X3))] 519.29/148.10 519.29/148.10 [proper(f(X1, X2, X3))] = [ 5 0] X1 + [ 4 0] X2 + [2 0] X3 + [1] 519.29/148.10 [15 0] [12 0] [6 0] [4] 519.29/148.10 >= [5 0] X1 + [4 0] X2 + [2 0] X3 + [1] 519.29/148.10 [9 0] [3 0] [0 0] [4] 519.29/148.10 = [f(proper(X1), proper(X2), proper(X3))] 519.29/148.10 519.29/148.10 [proper(a())] = [0] 519.29/148.10 [1] 519.29/148.10 >= [0] 519.29/148.10 [1] 519.29/148.10 = [ok(a())] 519.29/148.10 519.29/148.10 [proper(b())] = [0] 519.29/148.10 [1] 519.29/148.10 >= [0] 519.29/148.10 [1] 519.29/148.10 = [ok(b())] 519.29/148.10 519.29/148.10 [active^#(f(X1, X2, X3))] = [10 9] X1 + [8 3] X2 + [4 0] X3 + [2] 519.29/148.10 [ 0 0] [0 0] [0 0] [0] 519.29/148.10 > [2 4] X1 + [2 3] X2 + [1] 519.29/148.10 [0 0] [0 0] [0] 519.29/148.10 = [c_1(f^#(X1, active(X2), X3), active^#(X2))] 519.29/148.10 519.29/148.10 [f^#(X1, mark(X2), X3)] = [1 1] X1 + [0] 519.29/148.10 [0 2] [0] 519.29/148.10 >= [1 1] X1 + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 = [c_4(f^#(X1, X2, X3))] 519.29/148.10 519.29/148.10 [f^#(ok(X1), ok(X2), ok(X3))] = [1 1] X1 + [1] 519.29/148.10 [0 0] [2] 519.29/148.10 > [1 1] X1 + [0] 519.29/148.10 [0 0] [1] 519.29/148.10 = [c_5(f^#(X1, X2, X3))] 519.29/148.10 519.29/148.10 [proper^#(f(X1, X2, X3))] = [5 0] X1 + [4 0] X2 + [2 0] X3 + [1] 519.29/148.10 [0 0] [0 0] [0 0] [0] 519.29/148.10 >= [5 0] X1 + [2 0] X2 + [2 0] X3 + [1] 519.29/148.10 [0 0] [0 0] [0 0] [0] 519.29/148.10 = [c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.29/148.10 proper^#(X1), 519.29/148.10 proper^#(X2), 519.29/148.10 proper^#(X3))] 519.29/148.10 519.29/148.10 [top^#(mark(X))] = [3 0] X + [0] 519.29/148.10 [4 0] [0] 519.29/148.10 >= [1 0] X + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 = [proper^#(X)] 519.29/148.10 519.29/148.10 [top^#(mark(X))] = [3 0] X + [0] 519.29/148.10 [4 0] [0] 519.29/148.10 >= [3 0] X + [0] 519.29/148.10 [4 0] [0] 519.29/148.10 = [top^#(proper(X))] 519.29/148.10 519.29/148.10 [top^#(ok(X))] = [3 3] X + [0] 519.29/148.10 [4 4] [0] 519.29/148.10 >= [2 3] X + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 = [active^#(X)] 519.29/148.10 519.29/148.10 [top^#(ok(X))] = [3 3] X + [0] 519.29/148.10 [4 4] [0] 519.29/148.10 >= [3 0] X + [0] 519.29/148.10 [4 0] [0] 519.29/148.10 = [top^#(active(X))] 519.29/148.10 519.29/148.10 519.29/148.10 The strictly oriented rules are moved into the weak component. 519.29/148.10 519.29/148.10 We are left with following problem, upon which TcT provides the 519.29/148.10 certificate YES(O(1),O(n^1)). 519.29/148.10 519.29/148.10 Strict DPs: 519.29/148.10 { f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.29/148.10 , proper^#(f(X1, X2, X3)) -> 519.29/148.10 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.29/148.10 proper^#(X1), 519.29/148.10 proper^#(X2), 519.29/148.10 proper^#(X3)) } 519.29/148.10 Weak DPs: 519.29/148.10 { active^#(f(X1, X2, X3)) -> 519.29/148.10 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.29/148.10 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.29/148.10 , top^#(mark(X)) -> proper^#(X) 519.29/148.10 , top^#(mark(X)) -> top^#(proper(X)) 519.29/148.10 , top^#(ok(X)) -> active^#(X) 519.29/148.10 , top^#(ok(X)) -> top^#(active(X)) } 519.29/148.10 Weak Trs: 519.29/148.10 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.10 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.10 , active(b()) -> mark(a()) 519.29/148.10 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.10 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.10 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.10 , proper(a()) -> ok(a()) 519.29/148.10 , proper(b()) -> ok(b()) } 519.29/148.10 Obligation: 519.29/148.10 innermost runtime complexity 519.29/148.10 Answer: 519.29/148.10 YES(O(1),O(n^1)) 519.29/148.10 519.29/148.10 We use the processor 'matrix interpretation of dimension 2' to 519.29/148.10 orient following rules strictly. 519.29/148.10 519.29/148.10 DPs: 519.29/148.10 { 1: f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.29/148.10 , 5: top^#(mark(X)) -> proper^#(X) 519.29/148.10 , 6: top^#(mark(X)) -> top^#(proper(X)) } 519.29/148.10 Trs: 519.29/148.10 { active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.10 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) } 519.29/148.10 519.29/148.10 Sub-proof: 519.29/148.10 ---------- 519.29/148.10 The following argument positions are usable: 519.29/148.10 Uargs(c_1) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, 519.29/148.10 Uargs(c_6) = {1, 2, 3, 4} 519.29/148.10 519.29/148.10 TcT has computed the following constructor-based matrix 519.29/148.10 interpretation satisfying not(EDA) and not(IDA(1)). 519.29/148.10 519.29/148.10 [active](x1) = [1 0] x1 + [0] 519.29/148.10 [0 2] [0] 519.29/148.10 519.29/148.10 [f](x1, x2, x3) = [1 4] x1 + [4 0] x2 + [4 4] x3 + [0] 519.29/148.10 [0 0] [4 0] [0 0] [0] 519.29/148.10 519.29/148.10 [a] = [0] 519.29/148.10 [3] 519.29/148.10 519.29/148.10 [mark](x1) = [1 0] x1 + [1] 519.29/148.10 [0 0] [0] 519.29/148.10 519.29/148.10 [b] = [1] 519.29/148.10 [0] 519.29/148.10 519.29/148.10 [proper](x1) = [1 0] x1 + [0] 519.29/148.10 [0 1] [0] 519.29/148.10 519.29/148.10 [ok](x1) = [1 0] x1 + [0] 519.29/148.10 [0 1] [0] 519.29/148.10 519.29/148.10 [active^#](x1) = [2 0] x1 + [0] 519.29/148.10 [2 0] [0] 519.29/148.10 519.29/148.10 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 519.29/148.10 [0 0] [0 0] [0] 519.29/148.10 519.29/148.10 [f^#](x1, x2, x3) = [1 0] x2 + [0] 519.29/148.10 [1 0] [0] 519.29/148.10 519.29/148.10 [c_4](x1) = [1 0] x1 + [0] 519.29/148.10 [0 0] [1] 519.29/148.10 519.29/148.10 [c_5](x1) = [1 0] x1 + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 519.29/148.10 [proper^#](x1) = [1 0] x1 + [0] 519.29/148.10 [2 0] [0] 519.29/148.10 519.29/148.10 [c_6](x1, x2, x3, x4) = [1 2] x1 + [1 0] x2 + [1 0] x3 + [2 519.29/148.10 0] x4 + [0] 519.29/148.10 [0 0] [0 0] [0 0] [0 519.29/148.10 0] [0] 519.29/148.10 519.29/148.10 [top^#](x1) = [4 0] x1 + [0] 519.29/148.10 [4 0] [4] 519.29/148.10 519.29/148.10 The order satisfies the following ordering constraints: 519.29/148.10 519.29/148.10 [active(f(X1, X2, X3))] = [1 4] X1 + [4 0] X2 + [4 4] X3 + [0] 519.29/148.10 [0 0] [8 0] [0 0] [0] 519.29/148.10 >= [1 4] X1 + [4 0] X2 + [4 4] X3 + [0] 519.29/148.10 [0 0] [4 0] [0 0] [0] 519.29/148.10 = [f(X1, active(X2), X3)] 519.29/148.10 519.29/148.10 [active(f(a(), X, X))] = [8 4] X + [12] 519.29/148.10 [8 0] [0] 519.29/148.10 > [1 4] X + [9] 519.29/148.10 [0 0] [0] 519.29/148.10 = [mark(f(X, b(), b()))] 519.29/148.10 519.29/148.10 [active(b())] = [1] 519.29/148.10 [0] 519.29/148.10 >= [1] 519.29/148.10 [0] 519.29/148.10 = [mark(a())] 519.29/148.10 519.29/148.10 [f(X1, mark(X2), X3)] = [1 4] X1 + [4 0] X2 + [4 4] X3 + [4] 519.29/148.10 [0 0] [4 0] [0 0] [4] 519.29/148.10 > [1 4] X1 + [4 0] X2 + [4 4] X3 + [1] 519.29/148.10 [0 0] [0 0] [0 0] [0] 519.29/148.10 = [mark(f(X1, X2, X3))] 519.29/148.10 519.29/148.10 [f(ok(X1), ok(X2), ok(X3))] = [1 4] X1 + [4 0] X2 + [4 4] X3 + [0] 519.29/148.10 [0 0] [4 0] [0 0] [0] 519.29/148.10 >= [1 4] X1 + [4 0] X2 + [4 4] X3 + [0] 519.29/148.10 [0 0] [4 0] [0 0] [0] 519.29/148.10 = [ok(f(X1, X2, X3))] 519.29/148.10 519.29/148.10 [proper(f(X1, X2, X3))] = [1 4] X1 + [4 0] X2 + [4 4] X3 + [0] 519.29/148.10 [0 0] [4 0] [0 0] [0] 519.29/148.10 >= [1 4] X1 + [4 0] X2 + [4 4] X3 + [0] 519.29/148.10 [0 0] [4 0] [0 0] [0] 519.29/148.10 = [f(proper(X1), proper(X2), proper(X3))] 519.29/148.10 519.29/148.10 [proper(a())] = [0] 519.29/148.10 [3] 519.29/148.10 >= [0] 519.29/148.10 [3] 519.29/148.10 = [ok(a())] 519.29/148.10 519.29/148.10 [proper(b())] = [1] 519.29/148.10 [0] 519.29/148.10 >= [1] 519.29/148.10 [0] 519.29/148.10 = [ok(b())] 519.29/148.10 519.29/148.10 [active^#(f(X1, X2, X3))] = [2 8] X1 + [8 0] X2 + [8 8] X3 + [0] 519.29/148.10 [2 8] [8 0] [8 8] [0] 519.29/148.10 >= [3 0] X2 + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 = [c_1(f^#(X1, active(X2), X3), active^#(X2))] 519.29/148.10 519.29/148.10 [f^#(X1, mark(X2), X3)] = [1 0] X2 + [1] 519.29/148.10 [1 0] [1] 519.29/148.10 > [1 0] X2 + [0] 519.29/148.10 [0 0] [1] 519.29/148.10 = [c_4(f^#(X1, X2, X3))] 519.29/148.10 519.29/148.10 [f^#(ok(X1), ok(X2), ok(X3))] = [1 0] X2 + [0] 519.29/148.10 [1 0] [0] 519.29/148.10 >= [1 0] X2 + [0] 519.29/148.10 [0 0] [0] 519.29/148.10 = [c_5(f^#(X1, X2, X3))] 519.29/148.10 519.29/148.10 [proper^#(f(X1, X2, X3))] = [1 4] X1 + [4 0] X2 + [4 4] X3 + [0] 519.29/148.10 [2 8] [8 0] [8 8] [0] 519.29/148.10 >= [1 0] X1 + [4 0] X2 + [2 0] X3 + [0] 519.29/148.10 [0 0] [0 0] [0 0] [0] 519.29/148.10 = [c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.29/148.10 proper^#(X1), 519.29/148.10 proper^#(X2), 519.29/148.10 proper^#(X3))] 519.29/148.10 519.29/148.10 [top^#(mark(X))] = [4 0] X + [4] 519.29/148.10 [4 0] [8] 519.29/148.10 > [1 0] X + [0] 519.29/148.10 [2 0] [0] 519.29/148.10 = [proper^#(X)] 519.29/148.10 519.29/148.10 [top^#(mark(X))] = [4 0] X + [4] 519.29/148.10 [4 0] [8] 519.29/148.10 > [4 0] X + [0] 519.29/148.10 [4 0] [4] 519.29/148.10 = [top^#(proper(X))] 519.29/148.10 519.29/148.10 [top^#(ok(X))] = [4 0] X + [0] 519.29/148.10 [4 0] [4] 519.29/148.10 >= [2 0] X + [0] 519.29/148.10 [2 0] [0] 519.29/148.10 = [active^#(X)] 519.29/148.10 519.29/148.10 [top^#(ok(X))] = [4 0] X + [0] 519.29/148.10 [4 0] [4] 519.29/148.10 >= [4 0] X + [0] 519.29/148.10 [4 0] [4] 519.29/148.10 = [top^#(active(X))] 519.29/148.10 519.29/148.10 519.29/148.10 The strictly oriented rules are moved into the weak component. 519.29/148.10 519.29/148.10 We are left with following problem, upon which TcT provides the 519.29/148.10 certificate YES(O(1),O(n^1)). 519.29/148.10 519.29/148.10 Strict DPs: 519.29/148.10 { proper^#(f(X1, X2, X3)) -> 519.29/148.10 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.29/148.10 proper^#(X1), 519.29/148.10 proper^#(X2), 519.29/148.10 proper^#(X3)) } 519.29/148.10 Weak DPs: 519.29/148.10 { active^#(f(X1, X2, X3)) -> 519.29/148.10 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.29/148.10 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.29/148.10 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.29/148.10 , top^#(mark(X)) -> proper^#(X) 519.29/148.10 , top^#(mark(X)) -> top^#(proper(X)) 519.29/148.10 , top^#(ok(X)) -> active^#(X) 519.29/148.10 , top^#(ok(X)) -> top^#(active(X)) } 519.29/148.10 Weak Trs: 519.29/148.10 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.10 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.10 , active(b()) -> mark(a()) 519.29/148.10 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.10 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.10 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.10 , proper(a()) -> ok(a()) 519.29/148.10 , proper(b()) -> ok(b()) } 519.29/148.10 Obligation: 519.29/148.10 innermost runtime complexity 519.29/148.10 Answer: 519.29/148.10 YES(O(1),O(n^1)) 519.29/148.10 519.29/148.10 The following weak DPs constitute a sub-graph of the DG that is 519.29/148.11 closed under successors. The DPs are removed. 519.29/148.11 519.29/148.11 { active^#(f(X1, X2, X3)) -> 519.29/148.11 c_1(f^#(X1, active(X2), X3), active^#(X2)) 519.29/148.11 , f^#(X1, mark(X2), X3) -> c_4(f^#(X1, X2, X3)) 519.29/148.11 , f^#(ok(X1), ok(X2), ok(X3)) -> c_5(f^#(X1, X2, X3)) 519.29/148.11 , top^#(ok(X)) -> active^#(X) } 519.29/148.11 519.29/148.11 We are left with following problem, upon which TcT provides the 519.29/148.11 certificate YES(O(1),O(n^1)). 519.29/148.11 519.29/148.11 Strict DPs: 519.29/148.11 { proper^#(f(X1, X2, X3)) -> 519.29/148.11 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.29/148.11 proper^#(X1), 519.29/148.11 proper^#(X2), 519.29/148.11 proper^#(X3)) } 519.29/148.11 Weak DPs: 519.29/148.11 { top^#(mark(X)) -> proper^#(X) 519.29/148.11 , top^#(mark(X)) -> top^#(proper(X)) 519.29/148.11 , top^#(ok(X)) -> top^#(active(X)) } 519.29/148.11 Weak Trs: 519.29/148.11 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.11 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.11 , active(b()) -> mark(a()) 519.29/148.11 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.11 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.11 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.11 , proper(a()) -> ok(a()) 519.29/148.11 , proper(b()) -> ok(b()) } 519.29/148.11 Obligation: 519.29/148.11 innermost runtime complexity 519.29/148.11 Answer: 519.29/148.11 YES(O(1),O(n^1)) 519.29/148.11 519.29/148.11 Due to missing edges in the dependency-graph, the right-hand sides 519.29/148.11 of following rules could be simplified: 519.29/148.11 519.29/148.11 { proper^#(f(X1, X2, X3)) -> 519.29/148.11 c_6(f^#(proper(X1), proper(X2), proper(X3)), 519.29/148.11 proper^#(X1), 519.29/148.11 proper^#(X2), 519.29/148.11 proper^#(X3)) } 519.29/148.11 519.29/148.11 We are left with following problem, upon which TcT provides the 519.29/148.11 certificate YES(O(1),O(n^1)). 519.29/148.11 519.29/148.11 Strict DPs: 519.29/148.11 { proper^#(f(X1, X2, X3)) -> 519.29/148.11 c_1(proper^#(X1), proper^#(X2), proper^#(X3)) } 519.29/148.11 Weak DPs: 519.29/148.11 { top^#(mark(X)) -> c_2(proper^#(X)) 519.29/148.11 , top^#(mark(X)) -> c_3(top^#(proper(X))) 519.29/148.11 , top^#(ok(X)) -> c_4(top^#(active(X))) } 519.29/148.11 Weak Trs: 519.29/148.11 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.11 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.11 , active(b()) -> mark(a()) 519.29/148.11 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.11 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.11 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.11 , proper(a()) -> ok(a()) 519.29/148.11 , proper(b()) -> ok(b()) } 519.29/148.11 Obligation: 519.29/148.11 innermost runtime complexity 519.29/148.11 Answer: 519.29/148.11 YES(O(1),O(n^1)) 519.29/148.11 519.29/148.11 We use the processor 'matrix interpretation of dimension 1' to 519.29/148.11 orient following rules strictly. 519.29/148.11 519.29/148.11 DPs: 519.29/148.11 { 1: proper^#(f(X1, X2, X3)) -> 519.29/148.11 c_1(proper^#(X1), proper^#(X2), proper^#(X3)) } 519.29/148.11 519.29/148.11 Sub-proof: 519.29/148.11 ---------- 519.29/148.11 The following argument positions are usable: 519.29/148.11 Uargs(c_1) = {1, 2, 3}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 519.29/148.11 Uargs(c_4) = {1} 519.29/148.11 519.29/148.11 TcT has computed the following constructor-based matrix 519.29/148.11 interpretation satisfying not(EDA). 519.29/148.11 519.29/148.11 [active](x1) = [1] x1 + [0] 519.29/148.11 519.29/148.11 [f](x1, x2, x3) = [2] x1 + [4] x2 + [1] x3 + [1] 519.29/148.11 519.29/148.11 [a] = [0] 519.29/148.11 519.29/148.11 [mark](x1) = [1] x1 + [0] 519.29/148.11 519.29/148.11 [b] = [0] 519.29/148.11 519.29/148.11 [proper](x1) = [1] x1 + [0] 519.29/148.11 519.29/148.11 [ok](x1) = [1] x1 + [0] 519.29/148.11 519.29/148.11 [active^#](x1) = [7] x1 + [0] 519.29/148.11 519.29/148.11 [c_1](x1, x2) = [7] x1 + [7] x2 + [0] 519.29/148.11 519.29/148.11 [f^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 519.29/148.11 519.29/148.11 [c_4](x1) = [7] x1 + [0] 519.29/148.11 519.29/148.11 [c_5](x1) = [7] x1 + [0] 519.29/148.11 519.29/148.11 [proper^#](x1) = [1] x1 + [0] 519.29/148.11 519.29/148.11 [c_6](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] 519.29/148.11 519.29/148.11 [top^#](x1) = [2] x1 + [0] 519.29/148.11 519.29/148.11 [c] = [0] 519.29/148.11 519.29/148.11 [c_1](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [0] 519.29/148.11 519.29/148.11 [c_2](x1) = [1] x1 + [0] 519.29/148.11 519.29/148.11 [c_3](x1) = [1] x1 + [0] 519.29/148.11 519.29/148.11 [c_4](x1) = [1] x1 + [0] 519.29/148.11 519.29/148.11 The order satisfies the following ordering constraints: 519.29/148.11 519.29/148.11 [active(f(X1, X2, X3))] = [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 >= [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 = [f(X1, active(X2), X3)] 519.29/148.11 519.29/148.11 [active(f(a(), X, X))] = [5] X + [1] 519.29/148.11 >= [2] X + [1] 519.29/148.11 = [mark(f(X, b(), b()))] 519.29/148.11 519.29/148.11 [active(b())] = [0] 519.29/148.11 >= [0] 519.29/148.11 = [mark(a())] 519.29/148.11 519.29/148.11 [f(X1, mark(X2), X3)] = [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 >= [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 = [mark(f(X1, X2, X3))] 519.29/148.11 519.29/148.11 [f(ok(X1), ok(X2), ok(X3))] = [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 >= [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 = [ok(f(X1, X2, X3))] 519.29/148.11 519.29/148.11 [proper(f(X1, X2, X3))] = [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 >= [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 = [f(proper(X1), proper(X2), proper(X3))] 519.29/148.11 519.29/148.11 [proper(a())] = [0] 519.29/148.11 >= [0] 519.29/148.11 = [ok(a())] 519.29/148.11 519.29/148.11 [proper(b())] = [0] 519.29/148.11 >= [0] 519.29/148.11 = [ok(b())] 519.29/148.11 519.29/148.11 [proper^#(f(X1, X2, X3))] = [2] X1 + [4] X2 + [1] X3 + [1] 519.29/148.11 > [1] X1 + [2] X2 + [1] X3 + [0] 519.29/148.11 = [c_1(proper^#(X1), proper^#(X2), proper^#(X3))] 519.29/148.11 519.29/148.11 [top^#(mark(X))] = [2] X + [0] 519.29/148.11 >= [1] X + [0] 519.29/148.11 = [c_2(proper^#(X))] 519.29/148.11 519.29/148.11 [top^#(mark(X))] = [2] X + [0] 519.29/148.11 >= [2] X + [0] 519.29/148.11 = [c_3(top^#(proper(X)))] 519.29/148.11 519.29/148.11 [top^#(ok(X))] = [2] X + [0] 519.29/148.11 >= [2] X + [0] 519.29/148.11 = [c_4(top^#(active(X)))] 519.29/148.11 519.29/148.11 519.29/148.11 The strictly oriented rules are moved into the weak component. 519.29/148.11 519.29/148.11 We are left with following problem, upon which TcT provides the 519.29/148.11 certificate YES(O(1),O(1)). 519.29/148.11 519.29/148.11 Weak DPs: 519.29/148.11 { proper^#(f(X1, X2, X3)) -> 519.29/148.11 c_1(proper^#(X1), proper^#(X2), proper^#(X3)) 519.29/148.11 , top^#(mark(X)) -> c_2(proper^#(X)) 519.29/148.11 , top^#(mark(X)) -> c_3(top^#(proper(X))) 519.29/148.11 , top^#(ok(X)) -> c_4(top^#(active(X))) } 519.29/148.11 Weak Trs: 519.29/148.11 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.11 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.11 , active(b()) -> mark(a()) 519.29/148.11 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.11 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.11 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.11 , proper(a()) -> ok(a()) 519.29/148.11 , proper(b()) -> ok(b()) } 519.29/148.11 Obligation: 519.29/148.11 innermost runtime complexity 519.29/148.11 Answer: 519.29/148.11 YES(O(1),O(1)) 519.29/148.11 519.29/148.11 The following weak DPs constitute a sub-graph of the DG that is 519.29/148.11 closed under successors. The DPs are removed. 519.29/148.11 519.29/148.11 { proper^#(f(X1, X2, X3)) -> 519.29/148.11 c_1(proper^#(X1), proper^#(X2), proper^#(X3)) 519.29/148.11 , top^#(mark(X)) -> c_2(proper^#(X)) 519.29/148.11 , top^#(mark(X)) -> c_3(top^#(proper(X))) 519.29/148.11 , top^#(ok(X)) -> c_4(top^#(active(X))) } 519.29/148.11 519.29/148.11 We are left with following problem, upon which TcT provides the 519.29/148.11 certificate YES(O(1),O(1)). 519.29/148.11 519.29/148.11 Weak Trs: 519.29/148.11 { active(f(X1, X2, X3)) -> f(X1, active(X2), X3) 519.29/148.11 , active(f(a(), X, X)) -> mark(f(X, b(), b())) 519.29/148.11 , active(b()) -> mark(a()) 519.29/148.11 , f(X1, mark(X2), X3) -> mark(f(X1, X2, X3)) 519.29/148.11 , f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3)) 519.29/148.11 , proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3)) 519.29/148.11 , proper(a()) -> ok(a()) 519.29/148.11 , proper(b()) -> ok(b()) } 519.29/148.11 Obligation: 519.29/148.11 innermost runtime complexity 519.29/148.11 Answer: 519.29/148.11 YES(O(1),O(1)) 519.29/148.11 519.29/148.11 No rule is usable, rules are removed from the input problem. 519.29/148.11 519.29/148.11 We are left with following problem, upon which TcT provides the 519.29/148.11 certificate YES(O(1),O(1)). 519.29/148.11 519.29/148.11 Rules: Empty 519.29/148.11 Obligation: 519.29/148.11 innermost runtime complexity 519.29/148.11 Answer: 519.29/148.11 YES(O(1),O(1)) 519.29/148.11 519.29/148.11 Empty rules are trivially bounded 519.29/148.11 519.29/148.11 Hurray, we answered YES(O(1),O(n^2)) 519.29/148.14 EOF