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