YES(?,O(n^1)) 56.00/19.49 YES(?,O(n^1)) 56.00/19.49 56.00/19.49 We are left with following problem, upon which TcT provides the 56.00/19.49 certificate YES(?,O(n^1)). 56.00/19.49 56.00/19.49 Strict Trs: 56.00/19.49 { active(g(X)) -> mark(h(X)) 56.00/19.49 , active(h(d())) -> mark(g(c())) 56.00/19.49 , active(c()) -> mark(d()) 56.00/19.49 , g(ok(X)) -> ok(g(X)) 56.00/19.49 , h(ok(X)) -> ok(h(X)) 56.00/19.49 , proper(g(X)) -> g(proper(X)) 56.00/19.49 , proper(h(X)) -> h(proper(X)) 56.00/19.49 , proper(c()) -> ok(c()) 56.00/19.49 , proper(d()) -> ok(d()) 56.00/19.49 , top(mark(X)) -> top(proper(X)) 56.00/19.49 , top(ok(X)) -> top(active(X)) } 56.00/19.49 Obligation: 56.00/19.49 runtime complexity 56.00/19.49 Answer: 56.00/19.49 YES(?,O(n^1)) 56.00/19.49 56.00/19.49 We add the following weak dependency pairs: 56.00/19.49 56.00/19.49 Strict DPs: 56.00/19.49 { active^#(g(X)) -> c_1(h^#(X)) 56.00/19.49 , active^#(h(d())) -> c_2(g^#(c())) 56.00/19.49 , active^#(c()) -> c_3() 56.00/19.49 , h^#(ok(X)) -> c_5(h^#(X)) 56.00/19.49 , g^#(ok(X)) -> c_4(g^#(X)) 56.00/19.49 , proper^#(g(X)) -> c_6(g^#(proper(X))) 56.00/19.49 , proper^#(h(X)) -> c_7(h^#(proper(X))) 56.00/19.49 , proper^#(c()) -> c_8() 56.00/19.49 , proper^#(d()) -> c_9() 56.00/19.49 , top^#(mark(X)) -> c_10(top^#(proper(X))) 56.00/19.49 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.00/19.49 56.00/19.49 and mark the set of starting terms. 56.00/19.49 56.00/19.49 We are left with following problem, upon which TcT provides the 56.00/19.49 certificate YES(?,O(n^1)). 56.00/19.49 56.00/19.49 Strict DPs: 56.00/19.49 { active^#(g(X)) -> c_1(h^#(X)) 56.00/19.49 , active^#(h(d())) -> c_2(g^#(c())) 56.00/19.49 , active^#(c()) -> c_3() 56.00/19.49 , h^#(ok(X)) -> c_5(h^#(X)) 56.00/19.49 , g^#(ok(X)) -> c_4(g^#(X)) 56.00/19.49 , proper^#(g(X)) -> c_6(g^#(proper(X))) 56.00/19.49 , proper^#(h(X)) -> c_7(h^#(proper(X))) 56.00/19.49 , proper^#(c()) -> c_8() 56.00/19.49 , proper^#(d()) -> c_9() 56.00/19.49 , top^#(mark(X)) -> c_10(top^#(proper(X))) 56.00/19.49 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.00/19.49 Strict Trs: 56.00/19.49 { active(g(X)) -> mark(h(X)) 56.00/19.49 , active(h(d())) -> mark(g(c())) 56.00/19.49 , active(c()) -> mark(d()) 56.00/19.49 , g(ok(X)) -> ok(g(X)) 56.00/19.49 , h(ok(X)) -> ok(h(X)) 56.00/19.49 , proper(g(X)) -> g(proper(X)) 56.00/19.49 , proper(h(X)) -> h(proper(X)) 56.00/19.49 , proper(c()) -> ok(c()) 56.00/19.49 , proper(d()) -> ok(d()) 56.00/19.49 , top(mark(X)) -> top(proper(X)) 56.00/19.49 , top(ok(X)) -> top(active(X)) } 56.00/19.49 Obligation: 56.00/19.49 runtime complexity 56.00/19.49 Answer: 56.00/19.49 YES(?,O(n^1)) 56.00/19.49 56.00/19.49 We replace rewrite rules by usable rules: 56.00/19.49 56.00/19.49 Strict Usable Rules: 56.00/19.49 { active(g(X)) -> mark(h(X)) 56.00/19.49 , active(h(d())) -> mark(g(c())) 56.00/19.49 , active(c()) -> mark(d()) 56.00/19.49 , g(ok(X)) -> ok(g(X)) 56.00/19.49 , h(ok(X)) -> ok(h(X)) 56.00/19.49 , proper(g(X)) -> g(proper(X)) 56.00/19.49 , proper(h(X)) -> h(proper(X)) 56.00/19.49 , proper(c()) -> ok(c()) 56.00/19.49 , proper(d()) -> ok(d()) } 56.00/19.49 56.00/19.49 We are left with following problem, upon which TcT provides the 56.00/19.49 certificate YES(?,O(n^1)). 56.00/19.49 56.00/19.49 Strict DPs: 56.00/19.49 { active^#(g(X)) -> c_1(h^#(X)) 56.00/19.49 , active^#(h(d())) -> c_2(g^#(c())) 56.00/19.49 , active^#(c()) -> c_3() 56.00/19.49 , h^#(ok(X)) -> c_5(h^#(X)) 56.00/19.49 , g^#(ok(X)) -> c_4(g^#(X)) 56.00/19.49 , proper^#(g(X)) -> c_6(g^#(proper(X))) 56.00/19.49 , proper^#(h(X)) -> c_7(h^#(proper(X))) 56.00/19.49 , proper^#(c()) -> c_8() 56.00/19.49 , proper^#(d()) -> c_9() 56.00/19.49 , top^#(mark(X)) -> c_10(top^#(proper(X))) 56.00/19.49 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.00/19.49 Strict Trs: 56.00/19.49 { active(g(X)) -> mark(h(X)) 56.00/19.49 , active(h(d())) -> mark(g(c())) 56.00/19.49 , active(c()) -> mark(d()) 56.00/19.49 , g(ok(X)) -> ok(g(X)) 56.00/19.49 , h(ok(X)) -> ok(h(X)) 56.00/19.49 , proper(g(X)) -> g(proper(X)) 56.00/19.49 , proper(h(X)) -> h(proper(X)) 56.00/19.49 , proper(c()) -> ok(c()) 56.00/19.49 , proper(d()) -> ok(d()) } 56.00/19.49 Obligation: 56.00/19.49 runtime complexity 56.00/19.49 Answer: 56.00/19.49 YES(?,O(n^1)) 56.00/19.49 56.00/19.49 Consider the dependency graph: 56.00/19.49 56.00/19.49 1: active^#(g(X)) -> c_1(h^#(X)) -->_1 h^#(ok(X)) -> c_5(h^#(X)) :4 56.00/19.49 56.00/19.49 2: active^#(h(d())) -> c_2(g^#(c())) 56.00/19.49 56.00/19.49 3: active^#(c()) -> c_3() 56.00/19.49 56.00/19.49 4: h^#(ok(X)) -> c_5(h^#(X)) -->_1 h^#(ok(X)) -> c_5(h^#(X)) :4 56.00/19.49 56.00/19.49 5: g^#(ok(X)) -> c_4(g^#(X)) -->_1 g^#(ok(X)) -> c_4(g^#(X)) :5 56.00/19.49 56.00/19.49 6: proper^#(g(X)) -> c_6(g^#(proper(X))) 56.00/19.49 -->_1 g^#(ok(X)) -> c_4(g^#(X)) :5 56.00/19.49 56.00/19.49 7: proper^#(h(X)) -> c_7(h^#(proper(X))) 56.00/19.49 -->_1 h^#(ok(X)) -> c_5(h^#(X)) :4 56.00/19.49 56.00/19.49 8: proper^#(c()) -> c_8() 56.00/19.49 56.00/19.49 9: proper^#(d()) -> c_9() 56.00/19.49 56.00/19.49 10: top^#(mark(X)) -> c_10(top^#(proper(X))) 56.00/19.49 -->_1 top^#(ok(X)) -> c_11(top^#(active(X))) :11 56.00/19.49 -->_1 top^#(mark(X)) -> c_10(top^#(proper(X))) :10 56.00/19.49 56.00/19.49 11: top^#(ok(X)) -> c_11(top^#(active(X))) 56.00/19.49 -->_1 top^#(ok(X)) -> c_11(top^#(active(X))) :11 56.00/19.49 -->_1 top^#(mark(X)) -> c_10(top^#(proper(X))) :10 56.00/19.49 56.00/19.49 56.00/19.49 Only the nodes {3,4,5,8,9,10,11} are reachable from nodes 56.00/19.49 {3,4,5,8,9,10,11} that start derivation from marked basic terms. 56.00/19.49 The nodes not reachable are removed from the problem. 56.00/19.49 56.00/19.49 We are left with following problem, upon which TcT provides the 56.00/19.49 certificate YES(?,O(n^1)). 56.00/19.49 56.00/19.49 Strict DPs: 56.00/19.49 { active^#(c()) -> c_3() 56.00/19.49 , h^#(ok(X)) -> c_5(h^#(X)) 56.00/19.49 , g^#(ok(X)) -> c_4(g^#(X)) 56.00/19.49 , proper^#(c()) -> c_8() 56.00/19.49 , proper^#(d()) -> c_9() 56.00/19.49 , top^#(mark(X)) -> c_10(top^#(proper(X))) 56.00/19.49 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.00/19.49 Strict Trs: 56.00/19.49 { active(g(X)) -> mark(h(X)) 56.00/19.49 , active(h(d())) -> mark(g(c())) 56.00/19.49 , active(c()) -> mark(d()) 56.00/19.49 , g(ok(X)) -> ok(g(X)) 56.00/19.49 , h(ok(X)) -> ok(h(X)) 56.00/19.49 , proper(g(X)) -> g(proper(X)) 56.00/19.49 , proper(h(X)) -> h(proper(X)) 56.00/19.49 , proper(c()) -> ok(c()) 56.00/19.49 , proper(d()) -> ok(d()) } 56.00/19.49 Obligation: 56.00/19.49 runtime complexity 56.00/19.49 Answer: 56.00/19.49 YES(?,O(n^1)) 56.00/19.49 56.00/19.49 We estimate the number of application of {1,4,5} by applications of 56.00/19.49 Pre({1,4,5}) = {}. Here rules are labeled as follows: 56.00/19.49 56.00/19.49 DPs: 56.00/19.49 { 1: active^#(c()) -> c_3() 56.00/19.49 , 2: h^#(ok(X)) -> c_5(h^#(X)) 56.00/19.49 , 3: g^#(ok(X)) -> c_4(g^#(X)) 56.00/19.49 , 4: proper^#(c()) -> c_8() 56.00/19.49 , 5: proper^#(d()) -> c_9() 56.00/19.49 , 6: top^#(mark(X)) -> c_10(top^#(proper(X))) 56.00/19.49 , 7: top^#(ok(X)) -> c_11(top^#(active(X))) } 56.00/19.49 56.00/19.49 We are left with following problem, upon which TcT provides the 56.00/19.49 certificate YES(?,O(n^1)). 56.00/19.49 56.00/19.49 Strict DPs: 56.00/19.49 { h^#(ok(X)) -> c_5(h^#(X)) 56.00/19.49 , g^#(ok(X)) -> c_4(g^#(X)) 56.00/19.49 , top^#(mark(X)) -> c_10(top^#(proper(X))) 56.00/19.49 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.00/19.49 Strict Trs: 56.00/19.49 { active(g(X)) -> mark(h(X)) 56.00/19.49 , active(h(d())) -> mark(g(c())) 56.00/19.49 , active(c()) -> mark(d()) 56.00/19.49 , g(ok(X)) -> ok(g(X)) 56.00/19.49 , h(ok(X)) -> ok(h(X)) 56.00/19.49 , proper(g(X)) -> g(proper(X)) 56.00/19.49 , proper(h(X)) -> h(proper(X)) 56.00/19.49 , proper(c()) -> ok(c()) 56.00/19.49 , proper(d()) -> ok(d()) } 56.00/19.49 Weak DPs: 56.00/19.49 { active^#(c()) -> c_3() 56.00/19.49 , proper^#(c()) -> c_8() 56.00/19.49 , proper^#(d()) -> c_9() } 56.00/19.49 Obligation: 56.00/19.49 runtime complexity 56.00/19.49 Answer: 56.00/19.49 YES(?,O(n^1)) 56.00/19.49 56.00/19.49 We employ 'linear path analysis' using the following approximated 56.00/19.49 dependency graph: 56.00/19.49 ->{1} [ YES(O(1),O(n^1)) ] 56.00/19.49 56.00/19.49 ->{2} [ YES(O(1),O(n^1)) ] 56.00/19.49 56.00/19.49 ->{3,4} [ YES(O(1),O(n^1)) ] 56.00/19.49 56.00/19.49 ->{5} [ YES(O(1),O(1)) ] 56.00/19.49 56.00/19.49 ->{6} [ YES(O(1),O(1)) ] 56.00/19.49 56.00/19.49 ->{7} [ YES(O(1),O(1)) ] 56.00/19.49 56.00/19.49 56.00/19.49 Here dependency-pairs are as follows: 56.00/19.49 56.00/19.49 Strict DPs: 56.00/19.49 { 1: h^#(ok(X)) -> c_5(h^#(X)) 56.00/19.49 , 2: g^#(ok(X)) -> c_4(g^#(X)) 56.00/19.49 , 3: top^#(mark(X)) -> c_10(top^#(proper(X))) 56.00/19.49 , 4: top^#(ok(X)) -> c_11(top^#(active(X))) } 56.00/19.49 Weak DPs: 56.00/19.49 { 5: active^#(c()) -> c_3() 56.00/19.49 , 6: proper^#(c()) -> c_8() 56.00/19.49 , 7: proper^#(d()) -> c_9() } 56.00/19.49 56.00/19.49 * Path {1}: YES(O(1),O(n^1)) 56.00/19.49 -------------------------- 56.00/19.49 56.00/19.49 We are left with following problem, upon which TcT provides the 56.00/19.49 certificate YES(O(1),O(n^1)). 56.00/19.49 56.00/19.49 Strict DPs: { h^#(ok(X)) -> c_5(h^#(X)) } 56.00/19.49 Strict Trs: 56.00/19.49 { active(g(X)) -> mark(h(X)) 56.00/19.49 , active(h(d())) -> mark(g(c())) 56.00/19.49 , active(c()) -> mark(d()) 56.00/19.49 , g(ok(X)) -> ok(g(X)) 56.00/19.49 , h(ok(X)) -> ok(h(X)) 56.00/19.49 , proper(g(X)) -> g(proper(X)) 56.00/19.49 , proper(h(X)) -> h(proper(X)) 56.00/19.49 , proper(c()) -> ok(c()) 56.00/19.49 , proper(d()) -> ok(d()) } 56.00/19.49 Obligation: 56.00/19.49 runtime complexity 56.00/19.49 Answer: 56.00/19.49 YES(O(1),O(n^1)) 56.00/19.49 56.00/19.49 No rule is usable, rules are removed from the input problem. 56.00/19.49 56.00/19.49 We are left with following problem, upon which TcT provides the 56.00/19.49 certificate YES(O(1),O(n^1)). 56.00/19.49 56.00/19.49 Strict DPs: { h^#(ok(X)) -> c_5(h^#(X)) } 56.00/19.49 Obligation: 56.00/19.49 runtime complexity 56.00/19.49 Answer: 56.00/19.49 YES(O(1),O(n^1)) 56.00/19.49 56.00/19.49 We use the processor 'matrix interpretation of dimension 1' to 56.00/19.49 orient following rules strictly. 56.00/19.49 56.00/19.49 DPs: 56.00/19.49 { 1: h^#(ok(X)) -> c_5(h^#(X)) } 56.00/19.49 56.00/19.49 Sub-proof: 56.00/19.49 ---------- 56.00/19.49 The following argument positions are usable: 56.00/19.49 Uargs(c_5) = {1} 56.00/19.49 56.00/19.49 TcT has computed the following constructor-based matrix 56.00/19.49 interpretation satisfying not(EDA). 56.00/19.49 56.00/19.49 [ok](x1) = [1] x1 + [4] 56.00/19.49 56.00/19.49 [h^#](x1) = [2] x1 + [0] 56.00/19.49 56.00/19.49 [c_5](x1) = [1] x1 + [5] 56.00/19.49 56.00/19.49 The order satisfies the following ordering constraints: 56.13/19.50 56.13/19.50 [h^#(ok(X))] = [2] X + [8] 56.13/19.50 > [2] X + [5] 56.13/19.50 = [c_5(h^#(X))] 56.13/19.50 56.13/19.50 56.13/19.50 The strictly oriented rules are moved into the weak component. 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(1)). 56.13/19.50 56.13/19.50 Weak DPs: { h^#(ok(X)) -> c_5(h^#(X)) } 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(1)) 56.13/19.50 56.13/19.50 The following weak DPs constitute a sub-graph of the DG that is 56.13/19.50 closed under successors. The DPs are removed. 56.13/19.50 56.13/19.50 { h^#(ok(X)) -> c_5(h^#(X)) } 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(1)). 56.13/19.50 56.13/19.50 Rules: Empty 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(1)) 56.13/19.50 56.13/19.50 Empty rules are trivially bounded 56.13/19.50 56.13/19.50 * Path {2}: YES(O(1),O(n^1)) 56.13/19.50 -------------------------- 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(n^1)). 56.13/19.50 56.13/19.50 Strict DPs: { g^#(ok(X)) -> c_4(g^#(X)) } 56.13/19.50 Strict Trs: 56.13/19.50 { active(g(X)) -> mark(h(X)) 56.13/19.50 , active(h(d())) -> mark(g(c())) 56.13/19.50 , active(c()) -> mark(d()) 56.13/19.50 , g(ok(X)) -> ok(g(X)) 56.13/19.50 , h(ok(X)) -> ok(h(X)) 56.13/19.50 , proper(g(X)) -> g(proper(X)) 56.13/19.50 , proper(h(X)) -> h(proper(X)) 56.13/19.50 , proper(c()) -> ok(c()) 56.13/19.50 , proper(d()) -> ok(d()) } 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(n^1)) 56.13/19.50 56.13/19.50 No rule is usable, rules are removed from the input problem. 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(n^1)). 56.13/19.50 56.13/19.50 Strict DPs: { g^#(ok(X)) -> c_4(g^#(X)) } 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(n^1)) 56.13/19.50 56.13/19.50 We use the processor 'matrix interpretation of dimension 1' to 56.13/19.50 orient following rules strictly. 56.13/19.50 56.13/19.50 DPs: 56.13/19.50 { 1: g^#(ok(X)) -> c_4(g^#(X)) } 56.13/19.50 56.13/19.50 Sub-proof: 56.13/19.50 ---------- 56.13/19.50 The following argument positions are usable: 56.13/19.50 Uargs(c_4) = {1} 56.13/19.50 56.13/19.50 TcT has computed the following constructor-based matrix 56.13/19.50 interpretation satisfying not(EDA). 56.13/19.50 56.13/19.50 [ok](x1) = [1] x1 + [4] 56.13/19.50 56.13/19.50 [g^#](x1) = [2] x1 + [0] 56.13/19.50 56.13/19.50 [c_4](x1) = [1] x1 + [5] 56.13/19.50 56.13/19.50 The order satisfies the following ordering constraints: 56.13/19.50 56.13/19.50 [g^#(ok(X))] = [2] X + [8] 56.13/19.50 > [2] X + [5] 56.13/19.50 = [c_4(g^#(X))] 56.13/19.50 56.13/19.50 56.13/19.50 The strictly oriented rules are moved into the weak component. 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(1)). 56.13/19.50 56.13/19.50 Weak DPs: { g^#(ok(X)) -> c_4(g^#(X)) } 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(1)) 56.13/19.50 56.13/19.50 The following weak DPs constitute a sub-graph of the DG that is 56.13/19.50 closed under successors. The DPs are removed. 56.13/19.50 56.13/19.50 { g^#(ok(X)) -> c_4(g^#(X)) } 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(1)). 56.13/19.50 56.13/19.50 Rules: Empty 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(1)) 56.13/19.50 56.13/19.50 Empty rules are trivially bounded 56.13/19.50 56.13/19.50 * Path {3,4}: YES(O(1),O(n^1)) 56.13/19.50 ---------------------------- 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(n^1)). 56.13/19.50 56.13/19.50 Strict DPs: 56.13/19.50 { top^#(mark(X)) -> c_10(top^#(proper(X))) 56.13/19.50 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.13/19.50 Strict Trs: 56.13/19.50 { active(g(X)) -> mark(h(X)) 56.13/19.50 , active(h(d())) -> mark(g(c())) 56.13/19.50 , active(c()) -> mark(d()) 56.13/19.50 , g(ok(X)) -> ok(g(X)) 56.13/19.50 , h(ok(X)) -> ok(h(X)) 56.13/19.50 , proper(g(X)) -> g(proper(X)) 56.13/19.50 , proper(h(X)) -> h(proper(X)) 56.13/19.50 , proper(c()) -> ok(c()) 56.13/19.50 , proper(d()) -> ok(d()) } 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(n^1)) 56.13/19.50 56.13/19.50 The weightgap principle applies (using the following nonconstant 56.13/19.50 growth matrix-interpretation) 56.13/19.50 56.13/19.50 TcT has computed the following matrix interpretation satisfying 56.13/19.50 not(EDA) and not(IDA(1)). 56.13/19.50 56.13/19.50 [active](x1) = [1] x1 + [1] 56.13/19.50 56.13/19.50 [g](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [mark](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [h](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [c] = [0] 56.13/19.50 56.13/19.50 [d] = [0] 56.13/19.50 56.13/19.50 [proper](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [ok](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [top^#](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [c_10](x1) = [1] x1 + [7] 56.13/19.50 56.13/19.50 [c_11](x1) = [1] x1 + [1] 56.13/19.50 56.13/19.50 The order satisfies the following ordering constraints: 56.13/19.50 56.13/19.50 [active(g(X))] = [1] X + [1] 56.13/19.50 > [1] X + [0] 56.13/19.50 = [mark(h(X))] 56.13/19.50 56.13/19.50 [active(h(d()))] = [1] 56.13/19.50 > [0] 56.13/19.50 = [mark(g(c()))] 56.13/19.50 56.13/19.50 [active(c())] = [1] 56.13/19.50 > [0] 56.13/19.50 = [mark(d())] 56.13/19.50 56.13/19.50 [g(ok(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [ok(g(X))] 56.13/19.50 56.13/19.50 [h(ok(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [ok(h(X))] 56.13/19.50 56.13/19.50 [proper(g(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [g(proper(X))] 56.13/19.50 56.13/19.50 [proper(h(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [h(proper(X))] 56.13/19.50 56.13/19.50 [proper(c())] = [0] 56.13/19.50 >= [0] 56.13/19.50 = [ok(c())] 56.13/19.50 56.13/19.50 [proper(d())] = [0] 56.13/19.50 >= [0] 56.13/19.50 = [ok(d())] 56.13/19.50 56.13/19.50 [top^#(mark(X))] = [1] X + [0] 56.13/19.50 ? [1] X + [7] 56.13/19.50 = [c_10(top^#(proper(X)))] 56.13/19.50 56.13/19.50 [top^#(ok(X))] = [1] X + [0] 56.13/19.50 ? [1] X + [2] 56.13/19.50 = [c_11(top^#(active(X)))] 56.13/19.50 56.13/19.50 56.13/19.50 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(n^1)). 56.13/19.50 56.13/19.50 Strict DPs: 56.13/19.50 { top^#(mark(X)) -> c_10(top^#(proper(X))) 56.13/19.50 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.13/19.50 Strict Trs: 56.13/19.50 { g(ok(X)) -> ok(g(X)) 56.13/19.50 , h(ok(X)) -> ok(h(X)) 56.13/19.50 , proper(g(X)) -> g(proper(X)) 56.13/19.50 , proper(h(X)) -> h(proper(X)) 56.13/19.50 , proper(c()) -> ok(c()) 56.13/19.50 , proper(d()) -> ok(d()) } 56.13/19.50 Weak Trs: 56.13/19.50 { active(g(X)) -> mark(h(X)) 56.13/19.50 , active(h(d())) -> mark(g(c())) 56.13/19.50 , active(c()) -> mark(d()) } 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(n^1)) 56.13/19.50 56.13/19.50 The weightgap principle applies (using the following nonconstant 56.13/19.50 growth matrix-interpretation) 56.13/19.50 56.13/19.50 TcT has computed the following matrix interpretation satisfying 56.13/19.50 not(EDA) and not(IDA(1)). 56.13/19.50 56.13/19.50 [active](x1) = [1] x1 + [1] 56.13/19.50 56.13/19.50 [g](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [mark](x1) = [1] x1 + [1] 56.13/19.50 56.13/19.50 [h](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [c] = [0] 56.13/19.50 56.13/19.50 [d] = [0] 56.13/19.50 56.13/19.50 [proper](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [ok](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [top^#](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [c_10](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [c_11](x1) = [1] x1 + [1] 56.13/19.50 56.13/19.50 The order satisfies the following ordering constraints: 56.13/19.50 56.13/19.50 [active(g(X))] = [1] X + [1] 56.13/19.50 >= [1] X + [1] 56.13/19.50 = [mark(h(X))] 56.13/19.50 56.13/19.50 [active(h(d()))] = [1] 56.13/19.50 >= [1] 56.13/19.50 = [mark(g(c()))] 56.13/19.50 56.13/19.50 [active(c())] = [1] 56.13/19.50 >= [1] 56.13/19.50 = [mark(d())] 56.13/19.50 56.13/19.50 [g(ok(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [ok(g(X))] 56.13/19.50 56.13/19.50 [h(ok(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [ok(h(X))] 56.13/19.50 56.13/19.50 [proper(g(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [g(proper(X))] 56.13/19.50 56.13/19.50 [proper(h(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [h(proper(X))] 56.13/19.50 56.13/19.50 [proper(c())] = [0] 56.13/19.50 >= [0] 56.13/19.50 = [ok(c())] 56.13/19.50 56.13/19.50 [proper(d())] = [0] 56.13/19.50 >= [0] 56.13/19.50 = [ok(d())] 56.13/19.50 56.13/19.50 [top^#(mark(X))] = [1] X + [1] 56.13/19.50 > [1] X + [0] 56.13/19.50 = [c_10(top^#(proper(X)))] 56.13/19.50 56.13/19.50 [top^#(ok(X))] = [1] X + [0] 56.13/19.50 ? [1] X + [2] 56.13/19.50 = [c_11(top^#(active(X)))] 56.13/19.50 56.13/19.50 56.13/19.50 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(n^1)). 56.13/19.50 56.13/19.50 Strict DPs: { top^#(ok(X)) -> c_11(top^#(active(X))) } 56.13/19.50 Strict Trs: 56.13/19.50 { g(ok(X)) -> ok(g(X)) 56.13/19.50 , h(ok(X)) -> ok(h(X)) 56.13/19.50 , proper(g(X)) -> g(proper(X)) 56.13/19.50 , proper(h(X)) -> h(proper(X)) 56.13/19.50 , proper(c()) -> ok(c()) 56.13/19.50 , proper(d()) -> ok(d()) } 56.13/19.50 Weak DPs: { top^#(mark(X)) -> c_10(top^#(proper(X))) } 56.13/19.50 Weak Trs: 56.13/19.50 { active(g(X)) -> mark(h(X)) 56.13/19.50 , active(h(d())) -> mark(g(c())) 56.13/19.50 , active(c()) -> mark(d()) } 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(n^1)) 56.13/19.50 56.13/19.50 The weightgap principle applies (using the following nonconstant 56.13/19.50 growth matrix-interpretation) 56.13/19.50 56.13/19.50 TcT has computed the following matrix interpretation satisfying 56.13/19.50 not(EDA) and not(IDA(1)). 56.13/19.50 56.13/19.50 [active](x1) = [1] x1 + [1] 56.13/19.50 56.13/19.50 [g](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [mark](x1) = [1] x1 + [1] 56.13/19.50 56.13/19.50 [h](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [c] = [0] 56.13/19.50 56.13/19.50 [d] = [0] 56.13/19.50 56.13/19.50 [proper](x1) = [1] x1 + [1] 56.13/19.50 56.13/19.50 [ok](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [top^#](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [c_10](x1) = [1] x1 + [0] 56.13/19.50 56.13/19.50 [c_11](x1) = [1] x1 + [2] 56.13/19.50 56.13/19.50 The order satisfies the following ordering constraints: 56.13/19.50 56.13/19.50 [active(g(X))] = [1] X + [1] 56.13/19.50 >= [1] X + [1] 56.13/19.50 = [mark(h(X))] 56.13/19.50 56.13/19.50 [active(h(d()))] = [1] 56.13/19.50 >= [1] 56.13/19.50 = [mark(g(c()))] 56.13/19.50 56.13/19.50 [active(c())] = [1] 56.13/19.50 >= [1] 56.13/19.50 = [mark(d())] 56.13/19.50 56.13/19.50 [g(ok(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [ok(g(X))] 56.13/19.50 56.13/19.50 [h(ok(X))] = [1] X + [0] 56.13/19.50 >= [1] X + [0] 56.13/19.50 = [ok(h(X))] 56.13/19.50 56.13/19.50 [proper(g(X))] = [1] X + [1] 56.13/19.50 >= [1] X + [1] 56.13/19.50 = [g(proper(X))] 56.13/19.50 56.13/19.50 [proper(h(X))] = [1] X + [1] 56.13/19.50 >= [1] X + [1] 56.13/19.50 = [h(proper(X))] 56.13/19.50 56.13/19.50 [proper(c())] = [1] 56.13/19.50 > [0] 56.13/19.50 = [ok(c())] 56.13/19.50 56.13/19.50 [proper(d())] = [1] 56.13/19.50 > [0] 56.13/19.50 = [ok(d())] 56.13/19.50 56.13/19.50 [top^#(mark(X))] = [1] X + [1] 56.13/19.50 >= [1] X + [1] 56.13/19.50 = [c_10(top^#(proper(X)))] 56.13/19.50 56.13/19.50 [top^#(ok(X))] = [1] X + [0] 56.13/19.50 ? [1] X + [3] 56.13/19.50 = [c_11(top^#(active(X)))] 56.13/19.50 56.13/19.50 56.13/19.50 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 56.13/19.50 56.13/19.50 We are left with following problem, upon which TcT provides the 56.13/19.50 certificate YES(O(1),O(n^1)). 56.13/19.50 56.13/19.50 Strict DPs: { top^#(ok(X)) -> c_11(top^#(active(X))) } 56.13/19.50 Strict Trs: 56.13/19.50 { g(ok(X)) -> ok(g(X)) 56.13/19.50 , h(ok(X)) -> ok(h(X)) 56.13/19.50 , proper(g(X)) -> g(proper(X)) 56.13/19.50 , proper(h(X)) -> h(proper(X)) } 56.13/19.50 Weak DPs: { top^#(mark(X)) -> c_10(top^#(proper(X))) } 56.13/19.50 Weak Trs: 56.13/19.50 { active(g(X)) -> mark(h(X)) 56.13/19.50 , active(h(d())) -> mark(g(c())) 56.13/19.50 , active(c()) -> mark(d()) 56.13/19.50 , proper(c()) -> ok(c()) 56.13/19.50 , proper(d()) -> ok(d()) } 56.13/19.50 Obligation: 56.13/19.50 runtime complexity 56.13/19.50 Answer: 56.13/19.50 YES(O(1),O(n^1)) 56.13/19.50 56.13/19.50 The weightgap principle applies (using the following nonconstant 56.13/19.50 growth matrix-interpretation) 56.13/19.50 56.13/19.50 TcT has computed the following matrix interpretation satisfying 56.13/19.50 not(EDA) and not(IDA(1)). 56.13/19.50 56.13/19.50 [active](x1) = [1 0] x1 + [1] 56.13/19.50 [0 0] [0] 56.13/19.50 56.13/19.50 [g](x1) = [1 0] x1 + [0] 56.13/19.50 [0 0] [0] 56.13/19.50 56.13/19.50 [mark](x1) = [1 2] x1 + [0] 56.13/19.50 [0 0] [0] 56.13/19.50 56.13/19.50 [h](x1) = [1 0] x1 + [0] 56.13/19.50 [0 0] [0] 56.13/19.50 56.13/19.50 [c] = [1] 56.13/19.50 [1] 56.13/19.50 56.13/19.50 [d] = [0] 56.13/19.50 [1] 56.13/19.50 56.13/19.50 [proper](x1) = [1 0] x1 + [0] 56.13/19.50 [0 1] [0] 56.13/19.50 56.13/19.50 [ok](x1) = [1 0] x1 + [0] 56.13/19.50 [0 0] [1] 56.13/19.50 56.13/19.50 [top^#](x1) = [1 2] x1 + [6] 56.13/19.50 [0 0] [0] 56.13/19.50 56.13/19.51 [c_10](x1) = [1 0] x1 + [0] 56.13/19.51 [0 1] [0] 56.13/19.51 56.13/19.51 [c_11](x1) = [1 0] x1 + [0] 56.13/19.51 [0 1] [0] 56.13/19.51 56.13/19.51 The order satisfies the following ordering constraints: 56.13/19.51 56.13/19.51 [active(g(X))] = [1 0] X + [1] 56.13/19.51 [0 0] [0] 56.13/19.51 > [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 = [mark(h(X))] 56.13/19.51 56.13/19.51 [active(h(d()))] = [1] 56.13/19.51 [0] 56.13/19.51 >= [1] 56.13/19.51 [0] 56.13/19.51 = [mark(g(c()))] 56.13/19.51 56.13/19.51 [active(c())] = [2] 56.13/19.51 [0] 56.13/19.51 >= [2] 56.13/19.51 [0] 56.13/19.51 = [mark(d())] 56.13/19.51 56.13/19.51 [g(ok(X))] = [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 ? [1 0] X + [0] 56.13/19.51 [0 0] [1] 56.13/19.51 = [ok(g(X))] 56.13/19.51 56.13/19.51 [h(ok(X))] = [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 ? [1 0] X + [0] 56.13/19.51 [0 0] [1] 56.13/19.51 = [ok(h(X))] 56.13/19.51 56.13/19.51 [proper(g(X))] = [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 >= [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 = [g(proper(X))] 56.13/19.51 56.13/19.51 [proper(h(X))] = [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 >= [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 = [h(proper(X))] 56.13/19.51 56.13/19.51 [proper(c())] = [1] 56.13/19.51 [1] 56.13/19.51 >= [1] 56.13/19.51 [1] 56.13/19.51 = [ok(c())] 56.13/19.51 56.13/19.51 [proper(d())] = [0] 56.13/19.51 [1] 56.13/19.51 >= [0] 56.13/19.51 [1] 56.13/19.51 = [ok(d())] 56.13/19.51 56.13/19.51 [top^#(mark(X))] = [1 2] X + [6] 56.13/19.51 [0 0] [0] 56.13/19.51 >= [1 2] X + [6] 56.13/19.51 [0 0] [0] 56.13/19.51 = [c_10(top^#(proper(X)))] 56.13/19.51 56.13/19.51 [top^#(ok(X))] = [1 0] X + [8] 56.13/19.51 [0 0] [0] 56.13/19.51 > [1 0] X + [7] 56.13/19.51 [0 0] [0] 56.13/19.51 = [c_11(top^#(active(X)))] 56.13/19.51 56.13/19.51 56.13/19.51 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(n^1)). 56.13/19.51 56.13/19.51 Strict Trs: 56.13/19.51 { g(ok(X)) -> ok(g(X)) 56.13/19.51 , h(ok(X)) -> ok(h(X)) 56.13/19.51 , proper(g(X)) -> g(proper(X)) 56.13/19.51 , proper(h(X)) -> h(proper(X)) } 56.13/19.51 Weak DPs: 56.13/19.51 { top^#(mark(X)) -> c_10(top^#(proper(X))) 56.13/19.51 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.13/19.51 Weak Trs: 56.13/19.51 { active(g(X)) -> mark(h(X)) 56.13/19.51 , active(h(d())) -> mark(g(c())) 56.13/19.51 , active(c()) -> mark(d()) 56.13/19.51 , proper(c()) -> ok(c()) 56.13/19.51 , proper(d()) -> ok(d()) } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(n^1)) 56.13/19.51 56.13/19.51 We use the processor 'matrix interpretation of dimension 2' to 56.13/19.51 orient following rules strictly. 56.13/19.51 56.13/19.51 Trs: { proper(g(X)) -> g(proper(X)) } 56.13/19.51 56.13/19.51 The induced complexity on above rules (modulo remaining rules) is 56.13/19.51 YES(?,O(n^1)) . These rules are moved into the corresponding weak 56.13/19.51 component(s). 56.13/19.51 56.13/19.51 Sub-proof: 56.13/19.51 ---------- 56.13/19.51 TcT has computed the following constructor-based matrix 56.13/19.51 interpretation satisfying not(EDA) and not(IDA(1)). 56.13/19.51 56.13/19.51 [active](x1) = [1 4] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 [g](x1) = [1 4] x1 + [0] 56.13/19.51 [0 2] [1] 56.13/19.51 56.13/19.51 [mark](x1) = [1 6] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 [h](x1) = [1 0] x1 + [4] 56.13/19.51 [0 2] [0] 56.13/19.51 56.13/19.51 [c] = [6] 56.13/19.51 [0] 56.13/19.51 56.13/19.51 [d] = [0] 56.13/19.51 [1] 56.13/19.51 56.13/19.51 [proper](x1) = [1 1] x1 + [0] 56.13/19.51 [0 1] [0] 56.13/19.51 56.13/19.51 [ok](x1) = [1 0] x1 + [0] 56.13/19.51 [0 1] [0] 56.13/19.51 56.13/19.51 [top^#](x1) = [1 4] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 [c_10](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 [c_11](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 The order satisfies the following ordering constraints: 56.13/19.51 56.13/19.51 [active(g(X))] = [1 12] X + [4] 56.13/19.51 [0 0] [0] 56.13/19.51 >= [1 12] X + [4] 56.13/19.51 [0 0] [0] 56.13/19.51 = [mark(h(X))] 56.13/19.51 56.13/19.51 [active(h(d()))] = [12] 56.13/19.51 [0] 56.13/19.51 >= [12] 56.13/19.51 [0] 56.13/19.51 = [mark(g(c()))] 56.13/19.51 56.13/19.51 [active(c())] = [6] 56.13/19.51 [0] 56.13/19.51 >= [6] 56.13/19.51 [0] 56.13/19.51 = [mark(d())] 56.13/19.51 56.13/19.51 [g(ok(X))] = [1 4] X + [0] 56.13/19.51 [0 2] [1] 56.13/19.51 >= [1 4] X + [0] 56.13/19.51 [0 2] [1] 56.13/19.51 = [ok(g(X))] 56.13/19.51 56.13/19.51 [h(ok(X))] = [1 0] X + [4] 56.13/19.51 [0 2] [0] 56.13/19.51 >= [1 0] X + [4] 56.13/19.51 [0 2] [0] 56.13/19.51 = [ok(h(X))] 56.13/19.51 56.13/19.51 [proper(g(X))] = [1 6] X + [1] 56.13/19.51 [0 2] [1] 56.13/19.51 > [1 5] X + [0] 56.13/19.51 [0 2] [1] 56.13/19.51 = [g(proper(X))] 56.13/19.51 56.13/19.51 [proper(h(X))] = [1 2] X + [4] 56.13/19.51 [0 2] [0] 56.13/19.51 >= [1 1] X + [4] 56.13/19.51 [0 2] [0] 56.13/19.51 = [h(proper(X))] 56.13/19.51 56.13/19.51 [proper(c())] = [6] 56.13/19.51 [0] 56.13/19.51 >= [6] 56.13/19.51 [0] 56.13/19.51 = [ok(c())] 56.13/19.51 56.13/19.51 [proper(d())] = [1] 56.13/19.51 [1] 56.13/19.51 > [0] 56.13/19.51 [1] 56.13/19.51 = [ok(d())] 56.13/19.51 56.13/19.51 [top^#(mark(X))] = [1 6] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 >= [1 5] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 = [c_10(top^#(proper(X)))] 56.13/19.51 56.13/19.51 [top^#(ok(X))] = [1 4] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 >= [1 4] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 = [c_11(top^#(active(X)))] 56.13/19.51 56.13/19.51 56.13/19.51 We return to the main proof. 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(n^1)). 56.13/19.51 56.13/19.51 Strict Trs: 56.13/19.51 { g(ok(X)) -> ok(g(X)) 56.13/19.51 , h(ok(X)) -> ok(h(X)) 56.13/19.51 , proper(h(X)) -> h(proper(X)) } 56.13/19.51 Weak DPs: 56.13/19.51 { top^#(mark(X)) -> c_10(top^#(proper(X))) 56.13/19.51 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.13/19.51 Weak Trs: 56.13/19.51 { active(g(X)) -> mark(h(X)) 56.13/19.51 , active(h(d())) -> mark(g(c())) 56.13/19.51 , active(c()) -> mark(d()) 56.13/19.51 , proper(g(X)) -> g(proper(X)) 56.13/19.51 , proper(c()) -> ok(c()) 56.13/19.51 , proper(d()) -> ok(d()) } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(n^1)) 56.13/19.51 56.13/19.51 We use the processor 'matrix interpretation of dimension 2' to 56.13/19.51 orient following rules strictly. 56.13/19.51 56.13/19.51 Trs: { proper(h(X)) -> h(proper(X)) } 56.13/19.51 56.13/19.51 The induced complexity on above rules (modulo remaining rules) is 56.13/19.51 YES(?,O(n^1)) . These rules are moved into the corresponding weak 56.13/19.51 component(s). 56.13/19.51 56.13/19.51 Sub-proof: 56.13/19.51 ---------- 56.13/19.51 TcT has computed the following constructor-based matrix 56.13/19.51 interpretation satisfying not(EDA) and not(IDA(1)). 56.13/19.51 56.13/19.51 [active](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [4] 56.13/19.51 56.13/19.51 [g](x1) = [1 6] x1 + [6] 56.13/19.51 [0 1] [6] 56.13/19.51 56.13/19.51 [mark](x1) = [1 1] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 [h](x1) = [1 5] x1 + [0] 56.13/19.51 [0 1] [6] 56.13/19.51 56.13/19.51 [c] = [3] 56.13/19.51 [0] 56.13/19.51 56.13/19.51 [d] = [0] 56.13/19.51 [3] 56.13/19.51 56.13/19.51 [proper](x1) = [1 1] x1 + [0] 56.13/19.51 [0 1] [1] 56.13/19.51 56.13/19.51 [ok](x1) = [1 0] x1 + [0] 56.13/19.51 [0 1] [0] 56.13/19.51 56.13/19.51 [top^#](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 [c_10](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 [c_11](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 The order satisfies the following ordering constraints: 56.13/19.51 56.13/19.51 [active(g(X))] = [1 6] X + [6] 56.13/19.51 [0 0] [4] 56.13/19.51 >= [1 6] X + [6] 56.13/19.51 [0 0] [0] 56.13/19.51 = [mark(h(X))] 56.13/19.51 56.13/19.51 [active(h(d()))] = [15] 56.13/19.51 [4] 56.13/19.51 >= [15] 56.13/19.51 [0] 56.13/19.51 = [mark(g(c()))] 56.13/19.51 56.13/19.51 [active(c())] = [3] 56.13/19.51 [4] 56.13/19.51 >= [3] 56.13/19.51 [0] 56.13/19.51 = [mark(d())] 56.13/19.51 56.13/19.51 [g(ok(X))] = [1 6] X + [6] 56.13/19.51 [0 1] [6] 56.13/19.51 >= [1 6] X + [6] 56.13/19.51 [0 1] [6] 56.13/19.51 = [ok(g(X))] 56.13/19.51 56.13/19.51 [h(ok(X))] = [1 5] X + [0] 56.13/19.51 [0 1] [6] 56.13/19.51 >= [1 5] X + [0] 56.13/19.51 [0 1] [6] 56.13/19.51 = [ok(h(X))] 56.13/19.51 56.13/19.51 [proper(g(X))] = [1 7] X + [12] 56.13/19.51 [0 1] [7] 56.13/19.51 >= [1 7] X + [12] 56.13/19.51 [0 1] [7] 56.13/19.51 = [g(proper(X))] 56.13/19.51 56.13/19.51 [proper(h(X))] = [1 6] X + [6] 56.13/19.51 [0 1] [7] 56.13/19.51 > [1 6] X + [5] 56.13/19.51 [0 1] [7] 56.13/19.51 = [h(proper(X))] 56.13/19.51 56.13/19.51 [proper(c())] = [3] 56.13/19.51 [1] 56.13/19.51 >= [3] 56.13/19.51 [0] 56.13/19.51 = [ok(c())] 56.13/19.51 56.13/19.51 [proper(d())] = [3] 56.13/19.51 [4] 56.13/19.51 > [0] 56.13/19.51 [3] 56.13/19.51 = [ok(d())] 56.13/19.51 56.13/19.51 [top^#(mark(X))] = [1 1] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 >= [1 1] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 = [c_10(top^#(proper(X)))] 56.13/19.51 56.13/19.51 [top^#(ok(X))] = [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 >= [1 0] X + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 = [c_11(top^#(active(X)))] 56.13/19.51 56.13/19.51 56.13/19.51 We return to the main proof. 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(n^1)). 56.13/19.51 56.13/19.51 Strict Trs: 56.13/19.51 { g(ok(X)) -> ok(g(X)) 56.13/19.51 , h(ok(X)) -> ok(h(X)) } 56.13/19.51 Weak DPs: 56.13/19.51 { top^#(mark(X)) -> c_10(top^#(proper(X))) 56.13/19.51 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.13/19.51 Weak Trs: 56.13/19.51 { active(g(X)) -> mark(h(X)) 56.13/19.51 , active(h(d())) -> mark(g(c())) 56.13/19.51 , active(c()) -> mark(d()) 56.13/19.51 , proper(g(X)) -> g(proper(X)) 56.13/19.51 , proper(h(X)) -> h(proper(X)) 56.13/19.51 , proper(c()) -> ok(c()) 56.13/19.51 , proper(d()) -> ok(d()) } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(n^1)) 56.13/19.51 56.13/19.51 We use the processor 'matrix interpretation of dimension 2' to 56.13/19.51 orient following rules strictly. 56.13/19.51 56.13/19.51 Trs: 56.13/19.51 { g(ok(X)) -> ok(g(X)) 56.13/19.51 , h(ok(X)) -> ok(h(X)) } 56.13/19.51 56.13/19.51 The induced complexity on above rules (modulo remaining rules) is 56.13/19.51 YES(?,O(n^1)) . These rules are moved into the corresponding weak 56.13/19.51 component(s). 56.13/19.51 56.13/19.51 Sub-proof: 56.13/19.51 ---------- 56.13/19.51 TcT has computed the following constructor-based matrix 56.13/19.51 interpretation satisfying not(EDA) and not(IDA(1)). 56.13/19.51 56.13/19.51 [active](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [4] 56.13/19.51 56.13/19.51 [g](x1) = [1 5] x1 + [4] 56.13/19.51 [0 1] [5] 56.13/19.51 56.13/19.51 [mark](x1) = [1 1] x1 + [0] 56.13/19.51 [0 0] [0] 56.13/19.51 56.13/19.51 [h](x1) = [1 4] x1 + [0] 56.13/19.51 [0 1] [4] 56.13/19.51 56.13/19.51 [c] = [3] 56.13/19.51 [0] 56.13/19.51 56.13/19.51 [d] = [0] 56.13/19.51 [3] 56.13/19.51 56.13/19.51 [proper](x1) = [1 1] x1 + [0] 56.13/19.51 [0 1] [1] 56.13/19.51 56.13/19.51 [ok](x1) = [1 0] x1 + [0] 56.13/19.51 [0 1] [1] 56.13/19.51 56.13/19.51 [top^#](x1) = [2 0] x1 + [0] 56.13/19.51 [0 0] [4] 56.13/19.51 56.13/19.51 [c_10](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [3] 56.13/19.51 56.13/19.51 [c_11](x1) = [1 0] x1 + [0] 56.13/19.51 [0 0] [3] 56.13/19.51 56.13/19.51 The order satisfies the following ordering constraints: 56.13/19.51 56.13/19.51 [active(g(X))] = [1 5] X + [4] 56.13/19.51 [0 0] [4] 56.13/19.51 >= [1 5] X + [4] 56.13/19.51 [0 0] [0] 56.13/19.51 = [mark(h(X))] 56.13/19.51 56.13/19.51 [active(h(d()))] = [12] 56.13/19.51 [4] 56.13/19.51 >= [12] 56.13/19.51 [0] 56.13/19.51 = [mark(g(c()))] 56.13/19.51 56.13/19.51 [active(c())] = [3] 56.13/19.51 [4] 56.13/19.51 >= [3] 56.13/19.51 [0] 56.13/19.51 = [mark(d())] 56.13/19.51 56.13/19.51 [g(ok(X))] = [1 5] X + [9] 56.13/19.51 [0 1] [6] 56.13/19.51 > [1 5] X + [4] 56.13/19.51 [0 1] [6] 56.13/19.51 = [ok(g(X))] 56.13/19.51 56.13/19.51 [h(ok(X))] = [1 4] X + [4] 56.13/19.51 [0 1] [5] 56.13/19.51 > [1 4] X + [0] 56.13/19.51 [0 1] [5] 56.13/19.51 = [ok(h(X))] 56.13/19.51 56.13/19.51 [proper(g(X))] = [1 6] X + [9] 56.13/19.51 [0 1] [6] 56.13/19.51 >= [1 6] X + [9] 56.13/19.51 [0 1] [6] 56.13/19.51 = [g(proper(X))] 56.13/19.51 56.13/19.51 [proper(h(X))] = [1 5] X + [4] 56.13/19.51 [0 1] [5] 56.13/19.51 >= [1 5] X + [4] 56.13/19.51 [0 1] [5] 56.13/19.51 = [h(proper(X))] 56.13/19.51 56.13/19.51 [proper(c())] = [3] 56.13/19.51 [1] 56.13/19.51 >= [3] 56.13/19.51 [1] 56.13/19.51 = [ok(c())] 56.13/19.51 56.13/19.51 [proper(d())] = [3] 56.13/19.51 [4] 56.13/19.51 > [0] 56.13/19.51 [4] 56.13/19.51 = [ok(d())] 56.13/19.51 56.13/19.51 [top^#(mark(X))] = [2 2] X + [0] 56.13/19.51 [0 0] [4] 56.13/19.51 >= [2 2] X + [0] 56.13/19.51 [0 0] [3] 56.13/19.51 = [c_10(top^#(proper(X)))] 56.13/19.51 56.13/19.51 [top^#(ok(X))] = [2 0] X + [0] 56.13/19.51 [0 0] [4] 56.13/19.51 >= [2 0] X + [0] 56.13/19.51 [0 0] [3] 56.13/19.51 = [c_11(top^#(active(X)))] 56.13/19.51 56.13/19.51 56.13/19.51 We return to the main proof. 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(1)). 56.13/19.51 56.13/19.51 Weak DPs: 56.13/19.51 { top^#(mark(X)) -> c_10(top^#(proper(X))) 56.13/19.51 , top^#(ok(X)) -> c_11(top^#(active(X))) } 56.13/19.51 Weak Trs: 56.13/19.51 { active(g(X)) -> mark(h(X)) 56.13/19.51 , active(h(d())) -> mark(g(c())) 56.13/19.51 , active(c()) -> mark(d()) 56.13/19.51 , g(ok(X)) -> ok(g(X)) 56.13/19.51 , h(ok(X)) -> ok(h(X)) 56.13/19.51 , proper(g(X)) -> g(proper(X)) 56.13/19.51 , proper(h(X)) -> h(proper(X)) 56.13/19.51 , proper(c()) -> ok(c()) 56.13/19.51 , proper(d()) -> ok(d()) } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(1)) 56.13/19.51 56.13/19.51 Empty rules are trivially bounded 56.13/19.51 56.13/19.51 * Path {5}: YES(O(1),O(1)) 56.13/19.51 ------------------------ 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(1)). 56.13/19.51 56.13/19.51 Strict Trs: 56.13/19.51 { active(g(X)) -> mark(h(X)) 56.13/19.51 , active(h(d())) -> mark(g(c())) 56.13/19.51 , active(c()) -> mark(d()) 56.13/19.51 , g(ok(X)) -> ok(g(X)) 56.13/19.51 , h(ok(X)) -> ok(h(X)) 56.13/19.51 , proper(g(X)) -> g(proper(X)) 56.13/19.51 , proper(h(X)) -> h(proper(X)) 56.13/19.51 , proper(c()) -> ok(c()) 56.13/19.51 , proper(d()) -> ok(d()) } 56.13/19.51 Weak DPs: { active^#(c()) -> c_3() } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(1)) 56.13/19.51 56.13/19.51 No rule is usable, rules are removed from the input problem. 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(1)). 56.13/19.51 56.13/19.51 Weak DPs: { active^#(c()) -> c_3() } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(1)) 56.13/19.51 56.13/19.51 Empty rules are trivially bounded 56.13/19.51 56.13/19.51 * Path {6}: YES(O(1),O(1)) 56.13/19.51 ------------------------ 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(1)). 56.13/19.51 56.13/19.51 Strict Trs: 56.13/19.51 { active(g(X)) -> mark(h(X)) 56.13/19.51 , active(h(d())) -> mark(g(c())) 56.13/19.51 , active(c()) -> mark(d()) 56.13/19.51 , g(ok(X)) -> ok(g(X)) 56.13/19.51 , h(ok(X)) -> ok(h(X)) 56.13/19.51 , proper(g(X)) -> g(proper(X)) 56.13/19.51 , proper(h(X)) -> h(proper(X)) 56.13/19.51 , proper(c()) -> ok(c()) 56.13/19.51 , proper(d()) -> ok(d()) } 56.13/19.51 Weak DPs: { proper^#(c()) -> c_8() } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(1)) 56.13/19.51 56.13/19.51 No rule is usable, rules are removed from the input problem. 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(1)). 56.13/19.51 56.13/19.51 Weak DPs: { proper^#(c()) -> c_8() } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(1)) 56.13/19.51 56.13/19.51 Empty rules are trivially bounded 56.13/19.51 56.13/19.51 * Path {7}: YES(O(1),O(1)) 56.13/19.51 ------------------------ 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(1)). 56.13/19.51 56.13/19.51 Strict Trs: 56.13/19.51 { active(g(X)) -> mark(h(X)) 56.13/19.51 , active(h(d())) -> mark(g(c())) 56.13/19.51 , active(c()) -> mark(d()) 56.13/19.51 , g(ok(X)) -> ok(g(X)) 56.13/19.51 , h(ok(X)) -> ok(h(X)) 56.13/19.51 , proper(g(X)) -> g(proper(X)) 56.13/19.51 , proper(h(X)) -> h(proper(X)) 56.13/19.51 , proper(c()) -> ok(c()) 56.13/19.51 , proper(d()) -> ok(d()) } 56.13/19.51 Weak DPs: { proper^#(d()) -> c_9() } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(1)) 56.13/19.51 56.13/19.51 No rule is usable, rules are removed from the input problem. 56.13/19.51 56.13/19.51 We are left with following problem, upon which TcT provides the 56.13/19.51 certificate YES(O(1),O(1)). 56.13/19.51 56.13/19.51 Weak DPs: { proper^#(d()) -> c_9() } 56.13/19.51 Obligation: 56.13/19.51 runtime complexity 56.13/19.51 Answer: 56.13/19.51 YES(O(1),O(1)) 56.13/19.51 56.13/19.51 Empty rules are trivially bounded 56.13/19.51 56.13/19.51 Hurray, we answered YES(?,O(n^1)) 56.13/19.52 EOF