YES(O(1),O(n^2)) 660.28/165.75 YES(O(1),O(n^2)) 660.28/165.75 660.28/165.75 We are left with following problem, upon which TcT provides the 660.28/165.75 certificate YES(O(1),O(n^2)). 660.28/165.75 660.28/165.75 Strict Trs: 660.28/165.75 { from(X) -> cons(X, n__from(s(X))) 660.28/165.75 , from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__from(X)) -> from(X) 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) 660.28/165.75 , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)) 660.28/165.75 , sel(0(), cons(X, Z)) -> X } 660.28/165.75 Obligation: 660.28/165.75 runtime complexity 660.28/165.75 Answer: 660.28/165.75 YES(O(1),O(n^2)) 660.28/165.75 660.28/165.75 We add the following weak dependency pairs: 660.28/165.75 660.28/165.75 Strict DPs: 660.28/165.75 { from^#(X) -> c_1(X, X) 660.28/165.75 , from^#(X) -> c_2(X) 660.28/165.75 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.75 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.75 , first^#(0(), Z) -> c_5() 660.28/165.75 , activate^#(X) -> c_6(X) 660.28/165.75 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.75 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.75 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.75 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.75 660.28/165.75 and mark the set of starting terms. 660.28/165.75 660.28/165.75 We are left with following problem, upon which TcT provides the 660.28/165.75 certificate YES(O(1),O(n^2)). 660.28/165.75 660.28/165.75 Strict DPs: 660.28/165.75 { from^#(X) -> c_1(X, X) 660.28/165.75 , from^#(X) -> c_2(X) 660.28/165.75 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.75 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.75 , first^#(0(), Z) -> c_5() 660.28/165.75 , activate^#(X) -> c_6(X) 660.28/165.75 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.75 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.75 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.75 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.75 Strict Trs: 660.28/165.75 { from(X) -> cons(X, n__from(s(X))) 660.28/165.75 , from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__from(X)) -> from(X) 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) 660.28/165.75 , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z)) 660.28/165.75 , sel(0(), cons(X, Z)) -> X } 660.28/165.75 Obligation: 660.28/165.75 runtime complexity 660.28/165.75 Answer: 660.28/165.75 YES(O(1),O(n^2)) 660.28/165.75 660.28/165.75 We replace rewrite rules by usable rules: 660.28/165.75 660.28/165.75 Strict Usable Rules: 660.28/165.75 { from(X) -> cons(X, n__from(s(X))) 660.28/165.75 , from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__from(X)) -> from(X) 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.75 660.28/165.75 We are left with following problem, upon which TcT provides the 660.28/165.75 certificate YES(O(1),O(n^2)). 660.28/165.75 660.28/165.75 Strict DPs: 660.28/165.75 { from^#(X) -> c_1(X, X) 660.28/165.75 , from^#(X) -> c_2(X) 660.28/165.75 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.75 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.75 , first^#(0(), Z) -> c_5() 660.28/165.75 , activate^#(X) -> c_6(X) 660.28/165.75 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.75 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.75 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.75 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.75 Strict Trs: 660.28/165.75 { from(X) -> cons(X, n__from(s(X))) 660.28/165.75 , from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__from(X)) -> from(X) 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.75 Obligation: 660.28/165.75 runtime complexity 660.28/165.75 Answer: 660.28/165.75 YES(O(1),O(n^2)) 660.28/165.75 660.28/165.75 The weightgap principle applies (using the following constant 660.28/165.75 growth matrix-interpretation) 660.28/165.75 660.28/165.75 The following argument positions are usable: 660.28/165.75 Uargs(cons) = {2}, Uargs(first) = {2}, Uargs(n__first) = {2}, 660.28/165.75 Uargs(activate) = {1}, Uargs(c_4) = {3}, Uargs(c_7) = {1}, 660.28/165.75 Uargs(c_8) = {1}, Uargs(sel^#) = {2}, Uargs(c_9) = {1} 660.28/165.75 660.28/165.75 TcT has computed the following constructor-restricted matrix 660.28/165.75 interpretation. 660.28/165.75 660.28/165.75 [from](x1) = [1] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [cons](x1, x2) = [1 1] x2 + [0] 660.28/165.75 [0 0] [0] 660.28/165.75 660.28/165.75 [n__from](x1) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [s](x1) = [1 2] x1 + [0] 660.28/165.75 [0 1] [2] 660.28/165.75 660.28/165.75 [first](x1, x2) = [1 2] x1 + [1 0] x2 + [2] 660.28/165.75 [0 2] [0 0] [2] 660.28/165.75 660.28/165.75 [0] = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [nil] = [1] 660.28/165.75 [1] 660.28/165.75 660.28/165.75 [n__first](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 660.28/165.75 [0 1] [0 0] [2] 660.28/165.75 660.28/165.75 [activate](x1) = [1 1] x1 + [2] 660.28/165.75 [0 2] [0] 660.28/165.75 660.28/165.75 [from^#](x1) = [0 0] x1 + [1] 660.28/165.75 [2 1] [1] 660.28/165.75 660.28/165.75 [c_1](x1, x2) = [0 0] x1 + [0 0] x2 + [1] 660.28/165.75 [2 2] [2 2] [1] 660.28/165.75 660.28/165.75 [c_2](x1) = [0 0] x1 + [0] 660.28/165.75 [1 1] [1] 660.28/165.75 660.28/165.75 [first^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2] 660.28/165.75 [1 1] [2 2] [2] 660.28/165.75 660.28/165.75 [c_3](x1, x2) = [0 0] x1 + [0 0] x2 + [1] 660.28/165.75 [2 1] [1 1] [1] 660.28/165.75 660.28/165.75 [c_4](x1, x2, x3) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1] 660.28/165.75 [1 2] [1 1] [0 1] [1] 660.28/165.75 660.28/165.75 [activate^#](x1) = [0 0] x1 + [2] 660.28/165.75 [2 1] [2] 660.28/165.75 660.28/165.75 [c_5] = [1] 660.28/165.75 [1] 660.28/165.75 660.28/165.75 [c_6](x1) = [0 0] x1 + [1] 660.28/165.75 [1 1] [1] 660.28/165.75 660.28/165.75 [c_7](x1) = [1 0] x1 + [2] 660.28/165.75 [0 1] [2] 660.28/165.75 660.28/165.75 [c_8](x1) = [1 0] x1 + [1] 660.28/165.75 [0 1] [1] 660.28/165.75 660.28/165.75 [sel^#](x1, x2) = [2 0] x2 + [0] 660.28/165.75 [0 0] [0] 660.28/165.75 660.28/165.75 [c_9](x1) = [1 0] x1 + [2] 660.28/165.75 [0 1] [2] 660.28/165.75 660.28/165.75 [c_10](x1) = [1] 660.28/165.75 [1] 660.28/165.75 660.28/165.75 The order satisfies the following ordering constraints: 660.28/165.75 660.28/165.75 [from(X)] = [1] 660.28/165.75 [0] 660.28/165.75 > [0] 660.28/165.75 [0] 660.28/165.75 = [cons(X, n__from(s(X)))] 660.28/165.75 660.28/165.75 [from(X)] = [1] 660.28/165.75 [0] 660.28/165.75 > [0] 660.28/165.75 [0] 660.28/165.75 = [n__from(X)] 660.28/165.75 660.28/165.75 [first(X1, X2)] = [1 2] X1 + [1 0] X2 + [2] 660.28/165.75 [0 2] [0 0] [2] 660.28/165.75 > [1 1] X1 + [1 0] X2 + [0] 660.28/165.75 [0 1] [0 0] [2] 660.28/165.75 = [n__first(X1, X2)] 660.28/165.75 660.28/165.75 [first(s(X), cons(Y, Z))] = [1 4] X + [1 1] Z + [6] 660.28/165.75 [0 2] [0 0] [6] 660.28/165.75 > [1 2] X + [1 1] Z + [4] 660.28/165.75 [0 0] [0 0] [0] 660.28/165.75 = [cons(Y, n__first(X, activate(Z)))] 660.28/165.75 660.28/165.75 [first(0(), Z)] = [1 0] Z + [2] 660.28/165.75 [0 0] [2] 660.28/165.75 > [1] 660.28/165.75 [1] 660.28/165.75 = [nil()] 660.28/165.75 660.28/165.75 [activate(X)] = [1 1] X + [2] 660.28/165.75 [0 2] [0] 660.28/165.75 > [1 0] X + [0] 660.28/165.75 [0 1] [0] 660.28/165.75 = [X] 660.28/165.75 660.28/165.75 [activate(n__from(X))] = [2] 660.28/165.75 [0] 660.28/165.75 > [1] 660.28/165.75 [0] 660.28/165.75 = [from(X)] 660.28/165.75 660.28/165.75 [activate(n__first(X1, X2))] = [1 2] X1 + [1 0] X2 + [4] 660.28/165.75 [0 2] [0 0] [4] 660.28/165.75 > [1 2] X1 + [1 0] X2 + [2] 660.28/165.75 [0 2] [0 0] [2] 660.28/165.75 = [first(X1, X2)] 660.28/165.75 660.28/165.75 [from^#(X)] = [0 0] X + [1] 660.28/165.75 [2 1] [1] 660.28/165.75 ? [0 0] X + [1] 660.28/165.75 [4 4] [1] 660.28/165.75 = [c_1(X, X)] 660.28/165.75 660.28/165.75 [from^#(X)] = [0 0] X + [1] 660.28/165.75 [2 1] [1] 660.28/165.75 > [0 0] X + [0] 660.28/165.75 [1 1] [1] 660.28/165.75 = [c_2(X)] 660.28/165.75 660.28/165.75 [first^#(X1, X2)] = [0 0] X1 + [0 0] X2 + [2] 660.28/165.75 [1 1] [2 2] [2] 660.28/165.75 ? [0 0] X1 + [0 0] X2 + [1] 660.28/165.75 [2 1] [1 1] [1] 660.28/165.75 = [c_3(X1, X2)] 660.28/165.75 660.28/165.75 [first^#(s(X), cons(Y, Z))] = [0 0] X + [0 0] Z + [2] 660.28/165.75 [1 3] [2 2] [4] 660.28/165.75 ? [0 0] X + [0 0] Z + [0 0] Y + [3] 660.28/165.75 [1 1] [2 1] [1 2] [3] 660.28/165.75 = [c_4(Y, X, activate^#(Z))] 660.28/165.75 660.28/165.75 [first^#(0(), Z)] = [0 0] Z + [2] 660.28/165.75 [2 2] [2] 660.28/165.75 > [1] 660.28/165.75 [1] 660.28/165.75 = [c_5()] 660.28/165.75 660.28/165.75 [activate^#(X)] = [0 0] X + [2] 660.28/165.75 [2 1] [2] 660.28/165.75 > [0 0] X + [1] 660.28/165.75 [1 1] [1] 660.28/165.75 = [c_6(X)] 660.28/165.75 660.28/165.75 [activate^#(n__from(X))] = [2] 660.28/165.75 [2] 660.28/165.75 ? [0 0] X + [3] 660.28/165.75 [2 1] [3] 660.28/165.75 = [c_7(from^#(X))] 660.28/165.75 660.28/165.75 [activate^#(n__first(X1, X2))] = [0 0] X1 + [0 0] X2 + [2] 660.28/165.75 [2 3] [2 0] [4] 660.28/165.75 ? [0 0] X1 + [0 0] X2 + [3] 660.28/165.75 [1 1] [2 2] [3] 660.28/165.75 = [c_8(first^#(X1, X2))] 660.28/165.75 660.28/165.75 [sel^#(s(X), cons(Y, Z))] = [2 2] Z + [0] 660.28/165.75 [0 0] [0] 660.28/165.75 ? [2 2] Z + [6] 660.28/165.75 [0 0] [2] 660.28/165.75 = [c_9(sel^#(X, activate(Z)))] 660.28/165.75 660.28/165.75 [sel^#(0(), cons(X, Z))] = [2 2] Z + [0] 660.28/165.75 [0 0] [0] 660.28/165.75 ? [1] 660.28/165.75 [1] 660.28/165.75 = [c_10(X)] 660.28/165.75 660.28/165.75 660.28/165.75 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 660.28/165.75 660.28/165.75 We are left with following problem, upon which TcT provides the 660.28/165.75 certificate YES(O(1),O(n^1)). 660.28/165.75 660.28/165.75 Strict DPs: 660.28/165.75 { from^#(X) -> c_1(X, X) 660.28/165.75 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.75 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.75 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.75 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.75 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.75 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.75 Weak DPs: 660.28/165.75 { from^#(X) -> c_2(X) 660.28/165.75 , first^#(0(), Z) -> c_5() 660.28/165.75 , activate^#(X) -> c_6(X) } 660.28/165.75 Weak Trs: 660.28/165.75 { from(X) -> cons(X, n__from(s(X))) 660.28/165.75 , from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__from(X)) -> from(X) 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.75 Obligation: 660.28/165.75 runtime complexity 660.28/165.75 Answer: 660.28/165.75 YES(O(1),O(n^1)) 660.28/165.75 660.28/165.75 The following weak DPs constitute a sub-graph of the DG that is 660.28/165.75 closed under successors. The DPs are removed. 660.28/165.75 660.28/165.75 { first^#(0(), Z) -> c_5() } 660.28/165.75 660.28/165.75 We are left with following problem, upon which TcT provides the 660.28/165.75 certificate YES(O(1),O(n^1)). 660.28/165.75 660.28/165.75 Strict DPs: 660.28/165.75 { from^#(X) -> c_1(X, X) 660.28/165.75 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.75 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.75 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.75 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.75 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.75 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.75 Weak DPs: 660.28/165.75 { from^#(X) -> c_2(X) 660.28/165.75 , activate^#(X) -> c_6(X) } 660.28/165.75 Weak Trs: 660.28/165.75 { from(X) -> cons(X, n__from(s(X))) 660.28/165.75 , from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__from(X)) -> from(X) 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.75 Obligation: 660.28/165.75 runtime complexity 660.28/165.75 Answer: 660.28/165.75 YES(O(1),O(n^1)) 660.28/165.75 660.28/165.75 We use the processor 'matrix interpretation of dimension 1' to 660.28/165.75 orient following rules strictly. 660.28/165.75 660.28/165.75 DPs: 660.28/165.75 { 7: sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.75 Trs: 660.28/165.75 { from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.75 660.28/165.75 Sub-proof: 660.28/165.75 ---------- 660.28/165.75 The following argument positions are usable: 660.28/165.75 Uargs(c_4) = {3}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, 660.28/165.75 Uargs(c_9) = {1} 660.28/165.75 660.28/165.75 TcT has computed the following constructor-based matrix 660.28/165.75 interpretation satisfying not(EDA). 660.28/165.75 660.28/165.75 [from](x1) = [4] 660.28/165.75 660.28/165.75 [cons](x1, x2) = [1] x2 + [4] 660.28/165.75 660.28/165.75 [n__from](x1) = [0] 660.28/165.75 660.28/165.75 [s](x1) = [1] x1 + [6] 660.28/165.75 660.28/165.75 [first](x1, x2) = [1] x1 + [6] 660.28/165.75 660.28/165.75 [0] = [0] 660.28/165.75 660.28/165.75 [nil] = [5] 660.28/165.75 660.28/165.75 [n__first](x1, x2) = [1] x1 + [4] 660.28/165.75 660.28/165.75 [activate](x1) = [1] x1 + [4] 660.28/165.75 660.28/165.75 [from^#](x1) = [0] 660.28/165.75 660.28/165.75 [c_1](x1, x2) = [0] 660.28/165.75 660.28/165.75 [c_2](x1) = [0] 660.28/165.75 660.28/165.75 [first^#](x1, x2) = [0] 660.28/165.75 660.28/165.75 [c_3](x1, x2) = [0] 660.28/165.75 660.28/165.75 [c_4](x1, x2, x3) = [2] x3 + [0] 660.28/165.75 660.28/165.75 [activate^#](x1) = [0] 660.28/165.75 660.28/165.75 [c_6](x1) = [0] 660.28/165.75 660.28/165.75 [c_7](x1) = [4] x1 + [0] 660.28/165.75 660.28/165.75 [c_8](x1) = [1] x1 + [0] 660.28/165.75 660.28/165.75 [sel^#](x1, x2) = [2] x2 + [0] 660.28/165.75 660.28/165.75 [c_9](x1) = [1] x1 + [0] 660.28/165.75 660.28/165.75 [c_10](x1) = [6] 660.28/165.75 660.28/165.75 The order satisfies the following ordering constraints: 660.28/165.75 660.28/165.75 [from(X)] = [4] 660.28/165.75 >= [4] 660.28/165.75 = [cons(X, n__from(s(X)))] 660.28/165.75 660.28/165.75 [from(X)] = [4] 660.28/165.75 > [0] 660.28/165.75 = [n__from(X)] 660.28/165.75 660.28/165.75 [first(X1, X2)] = [1] X1 + [6] 660.28/165.75 > [1] X1 + [4] 660.28/165.75 = [n__first(X1, X2)] 660.28/165.75 660.28/165.75 [first(s(X), cons(Y, Z))] = [1] X + [12] 660.28/165.75 > [1] X + [8] 660.28/165.75 = [cons(Y, n__first(X, activate(Z)))] 660.28/165.75 660.28/165.75 [first(0(), Z)] = [6] 660.28/165.75 > [5] 660.28/165.75 = [nil()] 660.28/165.75 660.28/165.75 [activate(X)] = [1] X + [4] 660.28/165.75 > [1] X + [0] 660.28/165.75 = [X] 660.28/165.75 660.28/165.75 [activate(n__from(X))] = [4] 660.28/165.75 >= [4] 660.28/165.75 = [from(X)] 660.28/165.75 660.28/165.75 [activate(n__first(X1, X2))] = [1] X1 + [8] 660.28/165.75 > [1] X1 + [6] 660.28/165.75 = [first(X1, X2)] 660.28/165.75 660.28/165.75 [from^#(X)] = [0] 660.28/165.75 >= [0] 660.28/165.75 = [c_1(X, X)] 660.28/165.75 660.28/165.75 [from^#(X)] = [0] 660.28/165.75 >= [0] 660.28/165.75 = [c_2(X)] 660.28/165.75 660.28/165.75 [first^#(X1, X2)] = [0] 660.28/165.75 >= [0] 660.28/165.75 = [c_3(X1, X2)] 660.28/165.75 660.28/165.75 [first^#(s(X), cons(Y, Z))] = [0] 660.28/165.75 >= [0] 660.28/165.75 = [c_4(Y, X, activate^#(Z))] 660.28/165.75 660.28/165.75 [activate^#(X)] = [0] 660.28/165.75 >= [0] 660.28/165.75 = [c_6(X)] 660.28/165.75 660.28/165.75 [activate^#(n__from(X))] = [0] 660.28/165.75 >= [0] 660.28/165.75 = [c_7(from^#(X))] 660.28/165.75 660.28/165.75 [activate^#(n__first(X1, X2))] = [0] 660.28/165.75 >= [0] 660.28/165.75 = [c_8(first^#(X1, X2))] 660.28/165.75 660.28/165.75 [sel^#(s(X), cons(Y, Z))] = [2] Z + [8] 660.28/165.75 >= [2] Z + [8] 660.28/165.75 = [c_9(sel^#(X, activate(Z)))] 660.28/165.75 660.28/165.75 [sel^#(0(), cons(X, Z))] = [2] Z + [8] 660.28/165.75 > [6] 660.28/165.75 = [c_10(X)] 660.28/165.75 660.28/165.75 660.28/165.75 The strictly oriented rules are moved into the weak component. 660.28/165.75 660.28/165.75 We are left with following problem, upon which TcT provides the 660.28/165.75 certificate YES(O(1),O(n^1)). 660.28/165.75 660.28/165.75 Strict DPs: 660.28/165.75 { from^#(X) -> c_1(X, X) 660.28/165.75 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.75 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.75 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.75 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.75 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) } 660.28/165.75 Weak DPs: 660.28/165.75 { from^#(X) -> c_2(X) 660.28/165.75 , activate^#(X) -> c_6(X) 660.28/165.75 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.75 Weak Trs: 660.28/165.75 { from(X) -> cons(X, n__from(s(X))) 660.28/165.75 , from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__from(X)) -> from(X) 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.75 Obligation: 660.28/165.75 runtime complexity 660.28/165.75 Answer: 660.28/165.75 YES(O(1),O(n^1)) 660.28/165.75 660.28/165.75 We use the processor 'matrix interpretation of dimension 2' to 660.28/165.75 orient following rules strictly. 660.28/165.75 660.28/165.75 DPs: 660.28/165.75 { 6: sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) } 660.28/165.75 660.28/165.75 Sub-proof: 660.28/165.75 ---------- 660.28/165.75 The following argument positions are usable: 660.28/165.75 Uargs(c_4) = {3}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, 660.28/165.75 Uargs(c_9) = {1} 660.28/165.75 660.28/165.75 TcT has computed the following constructor-based matrix 660.28/165.75 interpretation satisfying not(EDA) and not(IDA(1)). 660.28/165.75 660.28/165.75 [from](x1) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [cons](x1, x2) = [0 1] x2 + [0] 660.28/165.75 [0 0] [0] 660.28/165.75 660.28/165.75 [n__from](x1) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [s](x1) = [1 1] x1 + [2] 660.28/165.75 [0 0] [0] 660.28/165.75 660.28/165.75 [first](x1, x2) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [0] = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [nil] = [7] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [n__first](x1, x2) = [0 0] x1 + [0] 660.28/165.75 [1 0] [0] 660.28/165.75 660.28/165.75 [activate](x1) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [from^#](x1) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [c_1](x1, x2) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [c_2](x1) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [first^#](x1, x2) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [c_3](x1, x2) = [0] 660.28/165.75 [0] 660.28/165.75 660.28/165.75 [c_4](x1, x2, x3) = [4 0] x3 + [0] 660.28/165.75 [0 0] [0] 660.28/165.75 660.28/165.75 [activate^#](x1) = [0] 660.28/165.75 [4] 660.28/165.75 660.28/165.75 [c_6](x1) = [0] 660.28/165.75 [4] 660.28/165.75 660.28/165.75 [c_7](x1) = [4 0] x1 + [0] 660.28/165.75 [0 0] [3] 660.28/165.75 660.28/165.75 [c_8](x1) = [1 0] x1 + [0] 660.28/165.75 [0 0] [3] 660.28/165.75 660.28/165.75 [sel^#](x1, x2) = [4 0] x1 + [0] 660.28/165.75 [0 0] [1] 660.28/165.75 660.28/165.75 [c_9](x1) = [1 7] x1 + [0] 660.28/165.75 [0 0] [1] 660.28/165.75 660.28/165.75 [c_10](x1) = [0] 660.28/165.75 [1] 660.28/165.75 660.28/165.75 The order satisfies the following ordering constraints: 660.28/165.75 660.28/165.75 [from(X)] = [0] 660.28/165.75 [0] 660.28/165.75 >= [0] 660.28/165.75 [0] 660.28/165.75 = [cons(X, n__from(s(X)))] 660.28/165.75 660.28/165.75 [from(X)] = [0] 660.28/165.75 [0] 660.28/165.75 >= [0] 660.28/165.75 [0] 660.28/165.75 = [n__from(X)] 660.28/165.75 660.28/165.75 [first(X1, X2)] = [0] 660.28/165.75 [0] 660.28/165.75 ? [0 0] X1 + [0] 660.28/165.75 [1 0] [0] 660.28/165.75 = [n__first(X1, X2)] 660.28/165.75 660.28/165.75 [first(s(X), cons(Y, Z))] = [0] 660.28/165.75 [0] 660.28/165.75 ? [1 0] X + [0] 660.28/165.75 [0 0] [0] 660.28/165.75 = [cons(Y, n__first(X, activate(Z)))] 660.28/165.75 660.28/165.75 [first(0(), Z)] = [0] 660.28/165.75 [0] 660.28/165.75 ? [7] 660.28/165.75 [0] 660.28/165.75 = [nil()] 660.28/165.75 660.28/165.75 [activate(X)] = [0] 660.28/165.75 [0] 660.28/165.75 ? [1 0] X + [0] 660.28/165.75 [0 1] [0] 660.28/165.75 = [X] 660.28/165.75 660.28/165.75 [activate(n__from(X))] = [0] 660.28/165.75 [0] 660.28/165.75 >= [0] 660.28/165.75 [0] 660.28/165.75 = [from(X)] 660.28/165.75 660.28/165.75 [activate(n__first(X1, X2))] = [0] 660.28/165.75 [0] 660.28/165.75 >= [0] 660.28/165.75 [0] 660.28/165.75 = [first(X1, X2)] 660.28/165.75 660.28/165.75 [from^#(X)] = [0] 660.28/165.75 [0] 660.28/165.75 >= [0] 660.28/165.75 [0] 660.28/165.75 = [c_1(X, X)] 660.28/165.75 660.28/165.75 [from^#(X)] = [0] 660.28/165.75 [0] 660.28/165.75 >= [0] 660.28/165.75 [0] 660.28/165.75 = [c_2(X)] 660.28/165.75 660.28/165.75 [first^#(X1, X2)] = [0] 660.28/165.75 [0] 660.28/165.75 >= [0] 660.28/165.75 [0] 660.28/165.75 = [c_3(X1, X2)] 660.28/165.75 660.28/165.75 [first^#(s(X), cons(Y, Z))] = [0] 660.28/165.75 [0] 660.28/165.75 >= [0] 660.28/165.75 [0] 660.28/165.75 = [c_4(Y, X, activate^#(Z))] 660.28/165.75 660.28/165.75 [activate^#(X)] = [0] 660.28/165.75 [4] 660.28/165.75 >= [0] 660.28/165.75 [4] 660.28/165.75 = [c_6(X)] 660.28/165.75 660.28/165.75 [activate^#(n__from(X))] = [0] 660.28/165.75 [4] 660.28/165.75 >= [0] 660.28/165.75 [3] 660.28/165.75 = [c_7(from^#(X))] 660.28/165.75 660.28/165.75 [activate^#(n__first(X1, X2))] = [0] 660.28/165.75 [4] 660.28/165.75 >= [0] 660.28/165.75 [3] 660.28/165.75 = [c_8(first^#(X1, X2))] 660.28/165.75 660.28/165.75 [sel^#(s(X), cons(Y, Z))] = [4 4] X + [8] 660.28/165.75 [0 0] [1] 660.28/165.75 > [4 0] X + [7] 660.28/165.75 [0 0] [1] 660.28/165.75 = [c_9(sel^#(X, activate(Z)))] 660.28/165.75 660.28/165.75 [sel^#(0(), cons(X, Z))] = [0] 660.28/165.75 [1] 660.28/165.75 >= [0] 660.28/165.75 [1] 660.28/165.75 = [c_10(X)] 660.28/165.75 660.28/165.75 660.28/165.75 The strictly oriented rules are moved into the weak component. 660.28/165.75 660.28/165.75 We are left with following problem, upon which TcT provides the 660.28/165.75 certificate YES(O(1),O(n^1)). 660.28/165.75 660.28/165.75 Strict DPs: 660.28/165.75 { from^#(X) -> c_1(X, X) 660.28/165.75 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.75 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.75 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.75 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) } 660.28/165.75 Weak DPs: 660.28/165.75 { from^#(X) -> c_2(X) 660.28/165.75 , activate^#(X) -> c_6(X) 660.28/165.75 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.75 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.75 Weak Trs: 660.28/165.75 { from(X) -> cons(X, n__from(s(X))) 660.28/165.75 , from(X) -> n__from(X) 660.28/165.75 , first(X1, X2) -> n__first(X1, X2) 660.28/165.75 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.75 , first(0(), Z) -> nil() 660.28/165.75 , activate(X) -> X 660.28/165.75 , activate(n__from(X)) -> from(X) 660.28/165.75 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.75 Obligation: 660.28/165.75 runtime complexity 660.28/165.75 Answer: 660.28/165.75 YES(O(1),O(n^1)) 660.28/165.75 660.28/165.75 We use the processor 'matrix interpretation of dimension 1' to 660.28/165.75 orient following rules strictly. 660.28/165.75 660.28/165.75 DPs: 660.28/165.75 { 3: first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.75 , 4: activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.75 , 5: activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) } 660.28/165.75 660.28/165.75 Sub-proof: 660.28/165.75 ---------- 660.28/165.75 The following argument positions are usable: 660.28/165.75 Uargs(c_4) = {3}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, 660.28/165.75 Uargs(c_9) = {1} 660.28/165.75 660.28/165.75 TcT has computed the following constructor-based matrix 660.28/165.75 interpretation satisfying not(EDA). 660.28/165.75 660.28/165.75 [from](x1) = [4] x1 + [0] 660.28/165.75 660.28/165.75 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 660.28/165.75 660.28/165.75 [n__from](x1) = [2] 660.28/165.75 660.28/165.75 [s](x1) = [1] x1 + [4] 660.28/165.75 660.28/165.75 [first](x1, x2) = [0] 660.28/165.75 660.28/165.75 [0] = [0] 660.28/165.75 660.28/165.75 [nil] = [7] 660.28/165.75 660.28/165.75 [n__first](x1, x2) = [1] x1 + [1] x2 + [4] 660.28/165.75 660.28/165.75 [activate](x1) = [0] 660.28/165.75 660.28/165.75 [from^#](x1) = [0] 660.28/165.75 660.28/165.75 [c_1](x1, x2) = [0] 660.28/165.75 660.28/165.75 [c_2](x1) = [0] 660.28/165.75 660.28/165.75 [first^#](x1, x2) = [2] x1 + [2] x2 + [0] 660.28/165.75 660.28/165.75 [c_3](x1, x2) = [2] x1 + [1] x2 + [0] 660.28/165.75 660.28/165.75 [c_4](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [5] 660.28/165.75 660.28/165.75 [activate^#](x1) = [2] x1 + [0] 660.28/165.75 660.28/165.75 [c_6](x1) = [2] x1 + [0] 660.28/165.75 660.28/165.75 [c_7](x1) = [4] x1 + [3] 660.28/165.75 660.28/165.75 [c_8](x1) = [1] x1 + [7] 660.28/165.75 660.28/165.75 [sel^#](x1, x2) = [0] 660.28/165.75 660.28/165.75 [c_9](x1) = [2] x1 + [0] 660.28/165.75 660.28/165.75 [c_10](x1) = [0] 660.28/165.75 660.28/165.75 The order satisfies the following ordering constraints: 660.28/165.75 660.28/165.75 [from(X)] = [4] X + [0] 660.28/165.75 ? [1] X + [2] 660.28/165.76 = [cons(X, n__from(s(X)))] 660.28/165.76 660.28/165.76 [from(X)] = [4] X + [0] 660.28/165.76 ? [2] 660.28/165.76 = [n__from(X)] 660.28/165.76 660.28/165.76 [first(X1, X2)] = [0] 660.28/165.76 ? [1] X1 + [1] X2 + [4] 660.28/165.76 = [n__first(X1, X2)] 660.28/165.76 660.28/165.76 [first(s(X), cons(Y, Z))] = [0] 660.28/165.76 ? [1] X + [1] Y + [4] 660.28/165.76 = [cons(Y, n__first(X, activate(Z)))] 660.28/165.76 660.28/165.76 [first(0(), Z)] = [0] 660.28/165.76 ? [7] 660.28/165.76 = [nil()] 660.28/165.76 660.28/165.76 [activate(X)] = [0] 660.28/165.76 ? [1] X + [0] 660.28/165.76 = [X] 660.28/165.76 660.28/165.76 [activate(n__from(X))] = [0] 660.28/165.76 ? [4] X + [0] 660.28/165.76 = [from(X)] 660.28/165.76 660.28/165.76 [activate(n__first(X1, X2))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [first(X1, X2)] 660.28/165.76 660.28/165.76 [from^#(X)] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [c_1(X, X)] 660.28/165.76 660.28/165.76 [from^#(X)] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [c_2(X)] 660.28/165.76 660.28/165.76 [first^#(X1, X2)] = [2] X1 + [2] X2 + [0] 660.28/165.76 >= [2] X1 + [1] X2 + [0] 660.28/165.76 = [c_3(X1, X2)] 660.28/165.76 660.28/165.76 [first^#(s(X), cons(Y, Z))] = [2] X + [2] Z + [2] Y + [8] 660.28/165.76 > [2] X + [2] Z + [1] Y + [5] 660.28/165.76 = [c_4(Y, X, activate^#(Z))] 660.28/165.76 660.28/165.76 [activate^#(X)] = [2] X + [0] 660.28/165.76 >= [2] X + [0] 660.28/165.76 = [c_6(X)] 660.28/165.76 660.28/165.76 [activate^#(n__from(X))] = [4] 660.28/165.76 > [3] 660.28/165.76 = [c_7(from^#(X))] 660.28/165.76 660.28/165.76 [activate^#(n__first(X1, X2))] = [2] X1 + [2] X2 + [8] 660.28/165.76 > [2] X1 + [2] X2 + [7] 660.28/165.76 = [c_8(first^#(X1, X2))] 660.28/165.76 660.28/165.76 [sel^#(s(X), cons(Y, Z))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [c_9(sel^#(X, activate(Z)))] 660.28/165.76 660.28/165.76 [sel^#(0(), cons(X, Z))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [c_10(X)] 660.28/165.76 660.28/165.76 660.28/165.76 The strictly oriented rules are moved into the weak component. 660.28/165.76 660.28/165.76 We are left with following problem, upon which TcT provides the 660.28/165.76 certificate YES(O(1),O(n^1)). 660.28/165.76 660.28/165.76 Strict DPs: 660.28/165.76 { from^#(X) -> c_1(X, X) 660.28/165.76 , first^#(X1, X2) -> c_3(X1, X2) } 660.28/165.76 Weak DPs: 660.28/165.76 { from^#(X) -> c_2(X) 660.28/165.76 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.76 , activate^#(X) -> c_6(X) 660.28/165.76 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.76 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.76 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.76 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.76 Weak Trs: 660.28/165.76 { from(X) -> cons(X, n__from(s(X))) 660.28/165.76 , from(X) -> n__from(X) 660.28/165.76 , first(X1, X2) -> n__first(X1, X2) 660.28/165.76 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.76 , first(0(), Z) -> nil() 660.28/165.76 , activate(X) -> X 660.28/165.76 , activate(n__from(X)) -> from(X) 660.28/165.76 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.76 Obligation: 660.28/165.76 runtime complexity 660.28/165.76 Answer: 660.28/165.76 YES(O(1),O(n^1)) 660.28/165.76 660.28/165.76 We use the processor 'matrix interpretation of dimension 1' to 660.28/165.76 orient following rules strictly. 660.28/165.76 660.28/165.76 DPs: 660.28/165.76 { 2: first^#(X1, X2) -> c_3(X1, X2) 660.28/165.76 , 4: first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.76 , 5: activate^#(X) -> c_6(X) 660.28/165.76 , 6: activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.76 , 7: activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) } 660.28/165.76 660.28/165.76 Sub-proof: 660.28/165.76 ---------- 660.28/165.76 The following argument positions are usable: 660.28/165.76 Uargs(c_4) = {3}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, 660.28/165.76 Uargs(c_9) = {1} 660.28/165.76 660.28/165.76 TcT has computed the following constructor-based matrix 660.28/165.76 interpretation satisfying not(EDA). 660.28/165.76 660.28/165.76 [from](x1) = [4] x1 + [0] 660.28/165.76 660.28/165.76 [cons](x1, x2) = [1] x1 + [1] x2 + [4] 660.28/165.76 660.28/165.76 [n__from](x1) = [1] x1 + [0] 660.28/165.76 660.28/165.76 [s](x1) = [1] x1 + [0] 660.28/165.76 660.28/165.76 [first](x1, x2) = [0] 660.28/165.76 660.28/165.76 [0] = [0] 660.28/165.76 660.28/165.76 [nil] = [7] 660.28/165.76 660.28/165.76 [n__first](x1, x2) = [1] x1 + [1] x2 + [0] 660.28/165.76 660.28/165.76 [activate](x1) = [0] 660.28/165.76 660.28/165.76 [from^#](x1) = [1] x1 + [0] 660.28/165.76 660.28/165.76 [c_1](x1, x2) = [1] x1 + [0] 660.28/165.76 660.28/165.76 [c_2](x1) = [1] x1 + [0] 660.28/165.76 660.28/165.76 [first^#](x1, x2) = [2] x2 + [1] 660.28/165.76 660.28/165.76 [c_3](x1, x2) = [2] x2 + [0] 660.28/165.76 660.28/165.76 [c_4](x1, x2, x3) = [2] x1 + [1] x3 + [1] 660.28/165.76 660.28/165.76 [activate^#](x1) = [2] x1 + [4] 660.28/165.76 660.28/165.76 [c_6](x1) = [2] x1 + [3] 660.28/165.76 660.28/165.76 [c_7](x1) = [2] x1 + [1] 660.28/165.76 660.28/165.76 [c_8](x1) = [1] x1 + [1] 660.28/165.76 660.28/165.76 [sel^#](x1, x2) = [0] 660.28/165.76 660.28/165.76 [c_9](x1) = [1] x1 + [0] 660.28/165.76 660.28/165.76 [c_10](x1) = [0] 660.28/165.76 660.28/165.76 The order satisfies the following ordering constraints: 660.28/165.76 660.28/165.76 [from(X)] = [4] X + [0] 660.28/165.76 ? [2] X + [4] 660.28/165.76 = [cons(X, n__from(s(X)))] 660.28/165.76 660.28/165.76 [from(X)] = [4] X + [0] 660.28/165.76 >= [1] X + [0] 660.28/165.76 = [n__from(X)] 660.28/165.76 660.28/165.76 [first(X1, X2)] = [0] 660.28/165.76 ? [1] X1 + [1] X2 + [0] 660.28/165.76 = [n__first(X1, X2)] 660.28/165.76 660.28/165.76 [first(s(X), cons(Y, Z))] = [0] 660.28/165.76 ? [1] X + [1] Y + [4] 660.28/165.76 = [cons(Y, n__first(X, activate(Z)))] 660.28/165.76 660.28/165.76 [first(0(), Z)] = [0] 660.28/165.76 ? [7] 660.28/165.76 = [nil()] 660.28/165.76 660.28/165.76 [activate(X)] = [0] 660.28/165.76 ? [1] X + [0] 660.28/165.76 = [X] 660.28/165.76 660.28/165.76 [activate(n__from(X))] = [0] 660.28/165.76 ? [4] X + [0] 660.28/165.76 = [from(X)] 660.28/165.76 660.28/165.76 [activate(n__first(X1, X2))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [first(X1, X2)] 660.28/165.76 660.28/165.76 [from^#(X)] = [1] X + [0] 660.28/165.76 >= [1] X + [0] 660.28/165.76 = [c_1(X, X)] 660.28/165.76 660.28/165.76 [from^#(X)] = [1] X + [0] 660.28/165.76 >= [1] X + [0] 660.28/165.76 = [c_2(X)] 660.28/165.76 660.28/165.76 [first^#(X1, X2)] = [2] X2 + [1] 660.28/165.76 > [2] X2 + [0] 660.28/165.76 = [c_3(X1, X2)] 660.28/165.76 660.28/165.76 [first^#(s(X), cons(Y, Z))] = [2] Z + [2] Y + [9] 660.28/165.76 > [2] Z + [2] Y + [5] 660.28/165.76 = [c_4(Y, X, activate^#(Z))] 660.28/165.76 660.28/165.76 [activate^#(X)] = [2] X + [4] 660.28/165.76 > [2] X + [3] 660.28/165.76 = [c_6(X)] 660.28/165.76 660.28/165.76 [activate^#(n__from(X))] = [2] X + [4] 660.28/165.76 > [2] X + [1] 660.28/165.76 = [c_7(from^#(X))] 660.28/165.76 660.28/165.76 [activate^#(n__first(X1, X2))] = [2] X1 + [2] X2 + [4] 660.28/165.76 > [2] X2 + [2] 660.28/165.76 = [c_8(first^#(X1, X2))] 660.28/165.76 660.28/165.76 [sel^#(s(X), cons(Y, Z))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [c_9(sel^#(X, activate(Z)))] 660.28/165.76 660.28/165.76 [sel^#(0(), cons(X, Z))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [c_10(X)] 660.28/165.76 660.28/165.76 660.28/165.76 The strictly oriented rules are moved into the weak component. 660.28/165.76 660.28/165.76 We are left with following problem, upon which TcT provides the 660.28/165.76 certificate YES(O(1),O(1)). 660.28/165.76 660.28/165.76 Strict DPs: { from^#(X) -> c_1(X, X) } 660.28/165.76 Weak DPs: 660.28/165.76 { from^#(X) -> c_2(X) 660.28/165.76 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.76 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.76 , activate^#(X) -> c_6(X) 660.28/165.76 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.76 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.76 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.76 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.76 Weak Trs: 660.28/165.76 { from(X) -> cons(X, n__from(s(X))) 660.28/165.76 , from(X) -> n__from(X) 660.28/165.76 , first(X1, X2) -> n__first(X1, X2) 660.28/165.76 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.76 , first(0(), Z) -> nil() 660.28/165.76 , activate(X) -> X 660.28/165.76 , activate(n__from(X)) -> from(X) 660.28/165.76 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.76 Obligation: 660.28/165.76 runtime complexity 660.28/165.76 Answer: 660.28/165.76 YES(O(1),O(1)) 660.28/165.76 660.28/165.76 We use the processor 'matrix interpretation of dimension 1' to 660.28/165.76 orient following rules strictly. 660.28/165.76 660.28/165.76 DPs: 660.28/165.76 { 1: from^#(X) -> c_1(X, X) 660.28/165.76 , 2: from^#(X) -> c_2(X) 660.28/165.76 , 3: first^#(X1, X2) -> c_3(X1, X2) 660.28/165.76 , 5: activate^#(X) -> c_6(X) } 660.28/165.76 660.28/165.76 Sub-proof: 660.28/165.76 ---------- 660.28/165.76 The following argument positions are usable: 660.28/165.76 Uargs(c_4) = {3}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, 660.28/165.76 Uargs(c_9) = {1} 660.28/165.76 660.28/165.76 TcT has computed the following constructor-restricted matrix 660.28/165.76 interpretation. Note that the diagonal of the component-wise maxima 660.28/165.76 of interpretation-entries (of constructors) contains no more than 0 660.28/165.76 non-zero entries. 660.28/165.76 660.28/165.76 [from](x1) = [0] 660.28/165.76 660.28/165.76 [cons](x1, x2) = [0] 660.28/165.76 660.28/165.76 [n__from](x1) = [0] 660.28/165.76 660.28/165.76 [s](x1) = [0] 660.28/165.76 660.28/165.76 [first](x1, x2) = [4] x2 + [0] 660.28/165.76 660.28/165.76 [0] = [0] 660.28/165.76 660.28/165.76 [nil] = [6] 660.28/165.76 660.28/165.76 [n__first](x1, x2) = [0] 660.28/165.76 660.28/165.76 [activate](x1) = [0] 660.28/165.76 660.28/165.76 [from^#](x1) = [2] 660.28/165.76 660.28/165.76 [c_1](x1, x2) = [1] 660.28/165.76 660.28/165.76 [c_2](x1) = [0] 660.28/165.76 660.28/165.76 [first^#](x1, x2) = [2] 660.28/165.76 660.28/165.76 [c_3](x1, x2) = [1] 660.28/165.76 660.28/165.76 [c_4](x1, x2, x3) = [1] x3 + [0] 660.28/165.76 660.28/165.76 [activate^#](x1) = [2] 660.28/165.76 660.28/165.76 [c_6](x1) = [1] 660.28/165.76 660.28/165.76 [c_7](x1) = [1] x1 + [0] 660.28/165.76 660.28/165.76 [c_8](x1) = [1] x1 + [0] 660.28/165.76 660.28/165.76 [sel^#](x1, x2) = [0] 660.28/165.76 660.28/165.76 [c_9](x1) = [4] x1 + [0] 660.28/165.76 660.28/165.76 [c_10](x1) = [0] 660.28/165.76 660.28/165.76 The order satisfies the following ordering constraints: 660.28/165.76 660.28/165.76 [from(X)] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [cons(X, n__from(s(X)))] 660.28/165.76 660.28/165.76 [from(X)] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [n__from(X)] 660.28/165.76 660.28/165.76 [first(X1, X2)] = [4] X2 + [0] 660.28/165.76 >= [0] 660.28/165.76 = [n__first(X1, X2)] 660.28/165.76 660.28/165.76 [first(s(X), cons(Y, Z))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [cons(Y, n__first(X, activate(Z)))] 660.28/165.76 660.28/165.76 [first(0(), Z)] = [4] Z + [0] 660.28/165.76 ? [6] 660.28/165.76 = [nil()] 660.28/165.76 660.28/165.76 [activate(X)] = [0] 660.28/165.76 ? [1] X + [0] 660.28/165.76 = [X] 660.28/165.76 660.28/165.76 [activate(n__from(X))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [from(X)] 660.28/165.76 660.28/165.76 [activate(n__first(X1, X2))] = [0] 660.28/165.76 ? [4] X2 + [0] 660.28/165.76 = [first(X1, X2)] 660.28/165.76 660.28/165.76 [from^#(X)] = [2] 660.28/165.76 > [1] 660.28/165.76 = [c_1(X, X)] 660.28/165.76 660.28/165.76 [from^#(X)] = [2] 660.28/165.76 > [0] 660.28/165.76 = [c_2(X)] 660.28/165.76 660.28/165.76 [first^#(X1, X2)] = [2] 660.28/165.76 > [1] 660.28/165.76 = [c_3(X1, X2)] 660.28/165.76 660.28/165.76 [first^#(s(X), cons(Y, Z))] = [2] 660.28/165.76 >= [2] 660.28/165.76 = [c_4(Y, X, activate^#(Z))] 660.28/165.76 660.28/165.76 [activate^#(X)] = [2] 660.28/165.76 > [1] 660.28/165.76 = [c_6(X)] 660.28/165.76 660.28/165.76 [activate^#(n__from(X))] = [2] 660.28/165.76 >= [2] 660.28/165.76 = [c_7(from^#(X))] 660.28/165.76 660.28/165.76 [activate^#(n__first(X1, X2))] = [2] 660.28/165.76 >= [2] 660.28/165.76 = [c_8(first^#(X1, X2))] 660.28/165.76 660.28/165.76 [sel^#(s(X), cons(Y, Z))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [c_9(sel^#(X, activate(Z)))] 660.28/165.76 660.28/165.76 [sel^#(0(), cons(X, Z))] = [0] 660.28/165.76 >= [0] 660.28/165.76 = [c_10(X)] 660.28/165.76 660.28/165.76 660.28/165.76 The strictly oriented rules are moved into the weak component. 660.28/165.76 660.28/165.76 We are left with following problem, upon which TcT provides the 660.28/165.76 certificate YES(O(1),O(1)). 660.28/165.76 660.28/165.76 Weak DPs: 660.28/165.76 { from^#(X) -> c_1(X, X) 660.28/165.76 , from^#(X) -> c_2(X) 660.28/165.76 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.76 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.76 , activate^#(X) -> c_6(X) 660.28/165.76 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.76 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.76 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.76 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.76 Weak Trs: 660.28/165.76 { from(X) -> cons(X, n__from(s(X))) 660.28/165.76 , from(X) -> n__from(X) 660.28/165.76 , first(X1, X2) -> n__first(X1, X2) 660.28/165.76 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.76 , first(0(), Z) -> nil() 660.28/165.76 , activate(X) -> X 660.28/165.76 , activate(n__from(X)) -> from(X) 660.28/165.76 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.76 Obligation: 660.28/165.76 runtime complexity 660.28/165.76 Answer: 660.28/165.76 YES(O(1),O(1)) 660.28/165.76 660.28/165.76 The following weak DPs constitute a sub-graph of the DG that is 660.28/165.76 closed under successors. The DPs are removed. 660.28/165.76 660.28/165.76 { from^#(X) -> c_1(X, X) 660.28/165.76 , from^#(X) -> c_2(X) 660.28/165.76 , first^#(X1, X2) -> c_3(X1, X2) 660.28/165.76 , first^#(s(X), cons(Y, Z)) -> c_4(Y, X, activate^#(Z)) 660.28/165.76 , activate^#(X) -> c_6(X) 660.28/165.76 , activate^#(n__from(X)) -> c_7(from^#(X)) 660.28/165.76 , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2)) 660.28/165.76 , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) 660.28/165.76 , sel^#(0(), cons(X, Z)) -> c_10(X) } 660.28/165.76 660.28/165.76 We are left with following problem, upon which TcT provides the 660.28/165.76 certificate YES(O(1),O(1)). 660.28/165.76 660.28/165.76 Weak Trs: 660.28/165.76 { from(X) -> cons(X, n__from(s(X))) 660.28/165.76 , from(X) -> n__from(X) 660.28/165.76 , first(X1, X2) -> n__first(X1, X2) 660.28/165.76 , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))) 660.28/165.76 , first(0(), Z) -> nil() 660.28/165.76 , activate(X) -> X 660.28/165.76 , activate(n__from(X)) -> from(X) 660.28/165.76 , activate(n__first(X1, X2)) -> first(X1, X2) } 660.28/165.76 Obligation: 660.28/165.76 runtime complexity 660.28/165.76 Answer: 660.28/165.76 YES(O(1),O(1)) 660.28/165.76 660.28/165.76 No rule is usable, rules are removed from the input problem. 660.28/165.76 660.28/165.76 We are left with following problem, upon which TcT provides the 660.28/165.76 certificate YES(O(1),O(1)). 660.28/165.76 660.28/165.76 Rules: Empty 660.28/165.76 Obligation: 660.28/165.76 runtime complexity 660.28/165.76 Answer: 660.28/165.76 YES(O(1),O(1)) 660.28/165.76 660.28/165.76 Empty rules are trivially bounded 660.28/165.76 660.28/165.76 Hurray, we answered YES(O(1),O(n^2)) 660.28/165.77 EOF