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