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