YES(O(1),O(n^1)) 0.00/0.62 YES(O(1),O(n^1)) 0.00/0.62 0.00/0.62 We are left with following problem, upon which TcT provides the 0.00/0.62 certificate YES(O(1),O(n^1)). 0.00/0.62 0.00/0.62 Strict Trs: 0.00/0.62 { f(empty(), l) -> l 0.00/0.62 , f(cons(x, k), l) -> g(k, l, cons(x, k)) 0.00/0.62 , g(a, b, c) -> f(a, cons(b, c)) } 0.00/0.62 Obligation: 0.00/0.62 innermost runtime complexity 0.00/0.62 Answer: 0.00/0.62 YES(O(1),O(n^1)) 0.00/0.62 0.00/0.62 We add the following weak dependency pairs: 0.00/0.62 0.00/0.62 Strict DPs: 0.00/0.62 { f^#(empty(), l) -> c_1() 0.00/0.62 , f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) 0.00/0.62 , g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 0.00/0.62 and mark the set of starting terms. 0.00/0.62 0.00/0.62 We are left with following problem, upon which TcT provides the 0.00/0.62 certificate YES(O(1),O(n^1)). 0.00/0.62 0.00/0.62 Strict DPs: 0.00/0.62 { f^#(empty(), l) -> c_1() 0.00/0.62 , f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) 0.00/0.62 , g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 Strict Trs: 0.00/0.62 { f(empty(), l) -> l 0.00/0.62 , f(cons(x, k), l) -> g(k, l, cons(x, k)) 0.00/0.62 , g(a, b, c) -> f(a, cons(b, c)) } 0.00/0.62 Obligation: 0.00/0.62 innermost runtime complexity 0.00/0.62 Answer: 0.00/0.62 YES(O(1),O(n^1)) 0.00/0.62 0.00/0.62 No rule is usable, rules are removed from the input problem. 0.00/0.62 0.00/0.62 We are left with following problem, upon which TcT provides the 0.00/0.62 certificate YES(O(1),O(n^1)). 0.00/0.62 0.00/0.62 Strict DPs: 0.00/0.62 { f^#(empty(), l) -> c_1() 0.00/0.62 , f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) 0.00/0.62 , g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 Obligation: 0.00/0.62 innermost runtime complexity 0.00/0.62 Answer: 0.00/0.62 YES(O(1),O(n^1)) 0.00/0.62 0.00/0.62 The weightgap principle applies (using the following constant 0.00/0.62 growth matrix-interpretation) 0.00/0.62 0.00/0.62 The following argument positions are usable: 0.00/0.62 Uargs(c_2) = {1}, Uargs(c_3) = {1} 0.00/0.62 0.00/0.62 TcT has computed the following constructor-restricted matrix 0.00/0.62 interpretation. 0.00/0.62 0.00/0.62 [empty] = [0] 0.00/0.62 [0] 0.00/0.62 0.00/0.62 [cons](x1, x2) = [1 0] x1 + [0] 0.00/0.62 [0 0] [0] 0.00/0.62 0.00/0.62 [f^#](x1, x2) = [2 0] x2 + [0] 0.00/0.62 [0 0] [0] 0.00/0.62 0.00/0.62 [c_1] = [1] 0.00/0.62 [0] 0.00/0.62 0.00/0.62 [c_2](x1) = [1 0] x1 + [0] 0.00/0.62 [0 1] [0] 0.00/0.62 0.00/0.62 [g^#](x1, x2, x3) = [2 0] x2 + [1] 0.00/0.62 [2 2] [0] 0.00/0.62 0.00/0.62 [c_3](x1) = [1 0] x1 + [0] 0.00/0.62 [0 1] [0] 0.00/0.62 0.00/0.62 The order satisfies the following ordering constraints: 0.00/0.62 0.00/0.62 [f^#(empty(), l)] = [2 0] l + [0] 0.00/0.62 [0 0] [0] 0.00/0.62 ? [1] 0.00/0.62 [0] 0.00/0.62 = [c_1()] 0.00/0.62 0.00/0.62 [f^#(cons(x, k), l)] = [2 0] l + [0] 0.00/0.62 [0 0] [0] 0.00/0.62 ? [2 0] l + [1] 0.00/0.62 [2 2] [0] 0.00/0.62 = [c_2(g^#(k, l, cons(x, k)))] 0.00/0.62 0.00/0.62 [g^#(a, b, c)] = [2 0] b + [1] 0.00/0.62 [2 2] [0] 0.00/0.62 > [2 0] b + [0] 0.00/0.62 [0 0] [0] 0.00/0.62 = [c_3(f^#(a, cons(b, c)))] 0.00/0.62 0.00/0.62 0.00/0.62 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.62 0.00/0.62 We are left with following problem, upon which TcT provides the 0.00/0.62 certificate YES(O(1),O(n^1)). 0.00/0.62 0.00/0.62 Strict DPs: 0.00/0.62 { f^#(empty(), l) -> c_1() 0.00/0.62 , f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) } 0.00/0.62 Weak DPs: { g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 Obligation: 0.00/0.62 innermost runtime complexity 0.00/0.62 Answer: 0.00/0.62 YES(O(1),O(n^1)) 0.00/0.62 0.00/0.62 We use the processor 'matrix interpretation of dimension 1' to 0.00/0.62 orient following rules strictly. 0.00/0.62 0.00/0.62 DPs: 0.00/0.62 { 1: f^#(empty(), l) -> c_1() } 0.00/0.62 0.00/0.62 Sub-proof: 0.00/0.62 ---------- 0.00/0.62 The following argument positions are usable: 0.00/0.62 Uargs(c_2) = {1}, Uargs(c_3) = {1} 0.00/0.62 0.00/0.62 TcT has computed the following constructor-based matrix 0.00/0.62 interpretation satisfying not(EDA). 0.00/0.62 0.00/0.62 [empty] = [1] 0.00/0.62 0.00/0.62 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 0.00/0.62 0.00/0.62 [f^#](x1, x2) = [1] x1 + [0] 0.00/0.62 0.00/0.62 [c_1] = [0] 0.00/0.62 0.00/0.62 [c_2](x1) = [1] x1 + [0] 0.00/0.62 0.00/0.62 [g^#](x1, x2, x3) = [1] x1 + [0] 0.00/0.62 0.00/0.62 [c_3](x1) = [1] x1 + [0] 0.00/0.62 0.00/0.62 The order satisfies the following ordering constraints: 0.00/0.62 0.00/0.62 [f^#(empty(), l)] = [1] 0.00/0.62 > [0] 0.00/0.62 = [c_1()] 0.00/0.62 0.00/0.62 [f^#(cons(x, k), l)] = [1] x + [1] k + [0] 0.00/0.62 >= [1] k + [0] 0.00/0.62 = [c_2(g^#(k, l, cons(x, k)))] 0.00/0.62 0.00/0.62 [g^#(a, b, c)] = [1] a + [0] 0.00/0.62 >= [1] a + [0] 0.00/0.62 = [c_3(f^#(a, cons(b, c)))] 0.00/0.62 0.00/0.62 0.00/0.62 The strictly oriented rules are moved into the weak component. 0.00/0.62 0.00/0.62 We are left with following problem, upon which TcT provides the 0.00/0.62 certificate YES(O(1),O(n^1)). 0.00/0.62 0.00/0.62 Strict DPs: { f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) } 0.00/0.62 Weak DPs: 0.00/0.62 { f^#(empty(), l) -> c_1() 0.00/0.62 , g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 Obligation: 0.00/0.62 innermost runtime complexity 0.00/0.62 Answer: 0.00/0.62 YES(O(1),O(n^1)) 0.00/0.62 0.00/0.62 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.62 closed under successors. The DPs are removed. 0.00/0.62 0.00/0.62 { f^#(empty(), l) -> c_1() } 0.00/0.62 0.00/0.62 We are left with following problem, upon which TcT provides the 0.00/0.62 certificate YES(O(1),O(n^1)). 0.00/0.62 0.00/0.62 Strict DPs: { f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) } 0.00/0.62 Weak DPs: { g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 Obligation: 0.00/0.62 innermost runtime complexity 0.00/0.62 Answer: 0.00/0.62 YES(O(1),O(n^1)) 0.00/0.62 0.00/0.62 We use the processor 'matrix interpretation of dimension 1' to 0.00/0.62 orient following rules strictly. 0.00/0.62 0.00/0.62 DPs: 0.00/0.62 { 1: f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) } 0.00/0.62 0.00/0.62 Sub-proof: 0.00/0.62 ---------- 0.00/0.62 The following argument positions are usable: 0.00/0.62 Uargs(c_2) = {1}, Uargs(c_3) = {1} 0.00/0.62 0.00/0.62 TcT has computed the following constructor-based matrix 0.00/0.62 interpretation satisfying not(EDA). 0.00/0.62 0.00/0.62 [empty] = [0] 0.00/0.62 0.00/0.62 [cons](x1, x2) = [1] x1 + [1] x2 + [4] 0.00/0.62 0.00/0.62 [f^#](x1, x2) = [1] x1 + [0] 0.00/0.62 0.00/0.62 [c_1] = [0] 0.00/0.62 0.00/0.62 [c_2](x1) = [1] x1 + [1] 0.00/0.62 0.00/0.62 [g^#](x1, x2, x3) = [1] x1 + [0] 0.00/0.62 0.00/0.62 [c_3](x1) = [1] x1 + [0] 0.00/0.62 0.00/0.62 The order satisfies the following ordering constraints: 0.00/0.62 0.00/0.62 [f^#(cons(x, k), l)] = [1] x + [1] k + [4] 0.00/0.62 > [1] k + [1] 0.00/0.62 = [c_2(g^#(k, l, cons(x, k)))] 0.00/0.62 0.00/0.62 [g^#(a, b, c)] = [1] a + [0] 0.00/0.62 >= [1] a + [0] 0.00/0.62 = [c_3(f^#(a, cons(b, c)))] 0.00/0.62 0.00/0.62 0.00/0.62 We return to the main proof. Consider the set of all dependency 0.00/0.62 pairs 0.00/0.62 0.00/0.62 : 0.00/0.62 { 1: f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) 0.00/0.62 , 2: g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 0.00/0.62 Processor 'matrix interpretation of dimension 1' induces the 0.00/0.62 complexity certificate YES(?,O(n^1)) on application of dependency 0.00/0.62 pairs {1}. These cover all (indirect) predecessors of dependency 0.00/0.62 pairs {1,2}, their number of application is equally bounded. The 0.00/0.62 dependency pairs are shifted into the weak component. 0.00/0.62 0.00/0.62 We are left with following problem, upon which TcT provides the 0.00/0.62 certificate YES(O(1),O(1)). 0.00/0.62 0.00/0.62 Weak DPs: 0.00/0.62 { f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) 0.00/0.62 , g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 Obligation: 0.00/0.62 innermost runtime complexity 0.00/0.62 Answer: 0.00/0.62 YES(O(1),O(1)) 0.00/0.62 0.00/0.62 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.62 closed under successors. The DPs are removed. 0.00/0.62 0.00/0.62 { f^#(cons(x, k), l) -> c_2(g^#(k, l, cons(x, k))) 0.00/0.62 , g^#(a, b, c) -> c_3(f^#(a, cons(b, c))) } 0.00/0.62 0.00/0.62 We are left with following problem, upon which TcT provides the 0.00/0.62 certificate YES(O(1),O(1)). 0.00/0.62 0.00/0.62 Rules: Empty 0.00/0.62 Obligation: 0.00/0.62 innermost runtime complexity 0.00/0.62 Answer: 0.00/0.62 YES(O(1),O(1)) 0.00/0.62 0.00/0.62 Empty rules are trivially bounded 0.00/0.62 0.00/0.62 Hurray, we answered YES(O(1),O(n^1)) 0.00/0.62 EOF