YES(O(1),O(n^1)) 52.53/26.01 YES(O(1),O(n^1)) 52.53/26.01 52.53/26.01 We are left with following problem, upon which TcT provides the 52.53/26.01 certificate YES(O(1),O(n^1)). 52.53/26.01 52.53/26.01 Strict Trs: 52.53/26.01 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.01 , from(X) -> n__from(X) 52.53/26.01 , head(cons(X, XS)) -> X 52.53/26.01 , 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.01 , activate(X) -> X 52.53/26.01 , activate(n__from(X)) -> from(activate(X)) 52.53/26.01 , activate(n__s(X)) -> s(activate(X)) 52.53/26.01 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.01 , take(X1, X2) -> n__take(X1, X2) 52.53/26.01 , take(0(), XS) -> nil() 52.53/26.01 , take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))) 52.53/26.01 , s(X) -> n__s(X) 52.53/26.01 , sel(0(), cons(X, XS)) -> X 52.53/26.01 , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) } 52.53/26.01 Obligation: 52.53/26.01 innermost runtime complexity 52.53/26.01 Answer: 52.53/26.01 YES(O(1),O(n^1)) 52.53/26.01 52.53/26.01 Arguments of following rules are not normal-forms: 52.53/26.01 52.53/26.01 { take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))) 52.53/26.01 , sel(s(N), cons(X, XS)) -> sel(N, activate(XS)) } 52.53/26.01 52.53/26.01 All above mentioned rules can be savely removed. 52.53/26.01 52.53/26.01 We are left with following problem, upon which TcT provides the 52.53/26.01 certificate YES(O(1),O(n^1)). 52.53/26.01 52.53/26.01 Strict Trs: 52.53/26.01 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.01 , from(X) -> n__from(X) 52.53/26.01 , head(cons(X, XS)) -> X 52.53/26.01 , 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.01 , activate(X) -> X 52.53/26.01 , activate(n__from(X)) -> from(activate(X)) 52.53/26.01 , activate(n__s(X)) -> s(activate(X)) 52.53/26.01 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.01 , take(X1, X2) -> n__take(X1, X2) 52.53/26.01 , take(0(), XS) -> nil() 52.53/26.01 , s(X) -> n__s(X) 52.53/26.01 , sel(0(), cons(X, XS)) -> X } 52.53/26.01 Obligation: 52.53/26.01 innermost runtime complexity 52.53/26.01 Answer: 52.53/26.01 YES(O(1),O(n^1)) 52.53/26.01 52.53/26.01 We use the processor 'matrix interpretation of dimension 3' to 52.53/26.01 orient following rules strictly. 52.53/26.01 52.53/26.01 Trs: 52.53/26.01 { 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.01 , sel(0(), cons(X, XS)) -> X } 52.53/26.01 52.53/26.01 The induced complexity on above rules (modulo remaining rules) is 52.53/26.01 YES(?,O(n^1)) . These rules are moved into the corresponding weak 52.53/26.01 component(s). 52.53/26.01 52.53/26.01 Sub-proof: 52.53/26.01 ---------- 52.53/26.01 The following argument positions are usable: 52.53/26.01 Uargs(from) = {1}, Uargs(head) = {1}, Uargs(take) = {1, 2}, 52.53/26.01 Uargs(s) = {1} 52.53/26.01 52.53/26.01 TcT has computed the following constructor-based matrix 52.53/26.01 interpretation satisfying not(EDA) and not(IDA(1)). 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [from](x1) = [0 1 4] x1 + [0] 52.53/26.01 [2 0 0] [0] 52.53/26.01 52.53/26.01 [0 0 0] [1 0 0] [0] 52.53/26.01 [cons](x1, x2) = [0 1 1] x1 + [0 1 0] x2 + [0] 52.53/26.01 [1 0 0] [0 0 1] [0] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [n__from](x1) = [0 1 4] x1 + [0] 52.53/26.01 [1 0 0] [0] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [n__s](x1) = [0 0 0] x1 + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 52.53/26.01 [1 0 1] [0] 52.53/26.01 [head](x1) = [0 1 0] x1 + [0] 52.53/26.01 [0 2 0] [0] 52.53/26.01 52.53/26.01 [1 0 2] [7] 52.53/26.01 [2nd](x1) = [4 4 0] x1 + [7] 52.53/26.01 [0 4 0] [7] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [activate](x1) = [0 2 0] x1 + [0] 52.53/26.01 [0 0 2] [0] 52.53/26.01 52.53/26.01 [1 0 0] [1 0 0] [0] 52.53/26.01 [take](x1, x2) = [0 0 2] x1 + [0 0 0] x2 + [0] 52.53/26.01 [0 0 0] [0 0 0] [0] 52.53/26.01 52.53/26.01 [0] 52.53/26.01 [0] = [0] 52.53/26.01 [0] 52.53/26.01 52.53/26.01 [0] 52.53/26.01 [nil] = [0] 52.53/26.01 [0] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [s](x1) = [0 0 0] x1 + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 52.53/26.01 [1 0 0] [1 0 0] [0] 52.53/26.01 [n__take](x1, x2) = [0 0 2] x1 + [0 0 0] x2 + [0] 52.53/26.01 [0 0 0] [0 0 0] [0] 52.53/26.01 52.53/26.01 [7 0 4] [0 0 4] [7] 52.53/26.01 [sel](x1, x2) = [7 7 7] x1 + [0 1 0] x2 + [7] 52.53/26.01 [7 7 7] [0 2 0] [7] 52.53/26.01 52.53/26.01 The order satisfies the following ordering constraints: 52.53/26.01 52.53/26.01 [from(X)] = [1 0 0] [0] 52.53/26.01 [0 1 4] X + [0] 52.53/26.01 [2 0 0] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 1] X + [0] 52.53/26.01 [2 0 0] [0] 52.53/26.01 = [cons(X, n__from(n__s(X)))] 52.53/26.01 52.53/26.01 [from(X)] = [1 0 0] [0] 52.53/26.01 [0 1 4] X + [0] 52.53/26.01 [2 0 0] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 4] X + [0] 52.53/26.01 [1 0 0] [0] 52.53/26.01 = [n__from(X)] 52.53/26.01 52.53/26.01 [head(cons(X, XS))] = [1 0 0] [1 0 1] [0] 52.53/26.01 [0 1 1] X + [0 1 0] XS + [0] 52.53/26.01 [0 2 2] [0 2 0] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 [2nd(cons(X, XS))] = [2 0 0] [1 0 2] [7] 52.53/26.01 [0 4 4] X + [4 4 0] XS + [7] 52.53/26.01 [0 4 4] [0 4 0] [7] 52.53/26.01 > [1 0 2] [0] 52.53/26.01 [0 2 0] XS + [0] 52.53/26.01 [0 4 0] [0] 52.53/26.01 = [head(activate(XS))] 52.53/26.01 52.53/26.01 [activate(X)] = [1 0 0] [0] 52.53/26.01 [0 2 0] X + [0] 52.53/26.01 [0 0 2] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 [activate(n__from(X))] = [1 0 0] [0] 52.53/26.01 [0 2 8] X + [0] 52.53/26.01 [2 0 0] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 2 8] X + [0] 52.53/26.01 [2 0 0] [0] 52.53/26.01 = [from(activate(X))] 52.53/26.01 52.53/26.01 [activate(n__s(X))] = [1 0 0] [0] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 = [s(activate(X))] 52.53/26.01 52.53/26.01 [activate(n__take(X1, X2))] = [1 0 0] [1 0 0] [0] 52.53/26.01 [0 0 4] X1 + [0 0 0] X2 + [0] 52.53/26.01 [0 0 0] [0 0 0] [0] 52.53/26.01 >= [1 0 0] [1 0 0] [0] 52.53/26.01 [0 0 4] X1 + [0 0 0] X2 + [0] 52.53/26.01 [0 0 0] [0 0 0] [0] 52.53/26.01 = [take(activate(X1), activate(X2))] 52.53/26.01 52.53/26.01 [take(X1, X2)] = [1 0 0] [1 0 0] [0] 52.53/26.01 [0 0 2] X1 + [0 0 0] X2 + [0] 52.53/26.01 [0 0 0] [0 0 0] [0] 52.53/26.01 >= [1 0 0] [1 0 0] [0] 52.53/26.01 [0 0 2] X1 + [0 0 0] X2 + [0] 52.53/26.01 [0 0 0] [0 0 0] [0] 52.53/26.01 = [n__take(X1, X2)] 52.53/26.01 52.53/26.01 [take(0(), XS)] = [1 0 0] [0] 52.53/26.01 [0 0 0] XS + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 >= [0] 52.53/26.01 [0] 52.53/26.01 [0] 52.53/26.01 = [nil()] 52.53/26.01 52.53/26.01 [s(X)] = [1 0 0] [0] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 = [n__s(X)] 52.53/26.01 52.53/26.01 [sel(0(), cons(X, XS))] = [4 0 0] [0 0 4] [7] 52.53/26.01 [0 1 1] X + [0 1 0] XS + [7] 52.53/26.01 [0 2 2] [0 2 0] [7] 52.53/26.01 > [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 52.53/26.01 We return to the main proof. 52.53/26.01 52.53/26.01 We are left with following problem, upon which TcT provides the 52.53/26.01 certificate YES(O(1),O(n^1)). 52.53/26.01 52.53/26.01 Strict Trs: 52.53/26.01 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.01 , from(X) -> n__from(X) 52.53/26.01 , head(cons(X, XS)) -> X 52.53/26.01 , activate(X) -> X 52.53/26.01 , activate(n__from(X)) -> from(activate(X)) 52.53/26.01 , activate(n__s(X)) -> s(activate(X)) 52.53/26.01 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.01 , take(X1, X2) -> n__take(X1, X2) 52.53/26.01 , take(0(), XS) -> nil() 52.53/26.01 , s(X) -> n__s(X) } 52.53/26.01 Weak Trs: 52.53/26.01 { 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.01 , sel(0(), cons(X, XS)) -> X } 52.53/26.01 Obligation: 52.53/26.01 innermost runtime complexity 52.53/26.01 Answer: 52.53/26.01 YES(O(1),O(n^1)) 52.53/26.01 52.53/26.01 We use the processor 'matrix interpretation of dimension 3' to 52.53/26.01 orient following rules strictly. 52.53/26.01 52.53/26.01 Trs: 52.53/26.01 { activate(n__s(X)) -> s(activate(X)) 52.53/26.01 , s(X) -> n__s(X) } 52.53/26.01 52.53/26.01 The induced complexity on above rules (modulo remaining rules) is 52.53/26.01 YES(?,O(n^1)) . These rules are moved into the corresponding weak 52.53/26.01 component(s). 52.53/26.01 52.53/26.01 Sub-proof: 52.53/26.01 ---------- 52.53/26.01 The following argument positions are usable: 52.53/26.01 Uargs(from) = {1}, Uargs(head) = {1}, Uargs(take) = {1, 2}, 52.53/26.01 Uargs(s) = {1} 52.53/26.01 52.53/26.01 TcT has computed the following constructor-based matrix 52.53/26.01 interpretation satisfying not(EDA) and not(IDA(1)). 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [from](x1) = [1 0 0] x1 + [2] 52.53/26.01 [1 2 1] [4] 52.53/26.01 52.53/26.01 [1 0 0] [0 0 0] [0] 52.53/26.01 [cons](x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0] 52.53/26.01 [0 1 1] [0 1 1] [0] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [n__from](x1) = [1 0 0] x1 + [2] 52.53/26.01 [0 1 1] [0] 52.53/26.01 52.53/26.01 [1 0 0] [2] 52.53/26.01 [n__s](x1) = [0 0 0] x1 + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [head](x1) = [0 0 1] x1 + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 52.53/26.01 [0 2 0] [7] 52.53/26.01 [2nd](x1) = [0 5 7] x1 + [3] 52.53/26.01 [0 5 7] [7] 52.53/26.01 52.53/26.01 [2 0 0] [0] 52.53/26.01 [activate](x1) = [0 2 0] x1 + [0] 52.53/26.01 [5 3 7] [0] 52.53/26.01 52.53/26.01 [1 0 0] [1 0 0] [0] 52.53/26.01 [take](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [3] 52.53/26.01 [0 0 0] [0 0 0] [4] 52.53/26.01 52.53/26.01 [0] 52.53/26.01 [0] = [0] 52.53/26.01 [0] 52.53/26.01 52.53/26.01 [0] 52.53/26.01 [nil] = [3] 52.53/26.01 [4] 52.53/26.01 52.53/26.01 [1 0 0] [3] 52.53/26.01 [s](x1) = [0 0 0] x1 + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 52.53/26.01 [1 0 0] [1 0 0] [0] 52.53/26.01 [n__take](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [3] 52.53/26.01 [0 0 0] [0 0 0] [0] 52.53/26.01 52.53/26.01 [7 4 0] [1 0 0] [7] 52.53/26.01 [sel](x1, x2) = [7 7 7] x1 + [0 0 1] x2 + [7] 52.53/26.01 [7 7 7] [0 0 1] [7] 52.53/26.01 52.53/26.01 The order satisfies the following ordering constraints: 52.53/26.01 52.53/26.01 [from(X)] = [1 0 0] [0] 52.53/26.01 [1 0 0] X + [2] 52.53/26.01 [1 2 1] [4] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [1 0 0] X + [2] 52.53/26.01 [1 1 1] [4] 52.53/26.01 = [cons(X, n__from(n__s(X)))] 52.53/26.01 52.53/26.01 [from(X)] = [1 0 0] [0] 52.53/26.01 [1 0 0] X + [2] 52.53/26.01 [1 2 1] [4] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [1 0 0] X + [2] 52.53/26.01 [0 1 1] [0] 52.53/26.01 = [n__from(X)] 52.53/26.01 52.53/26.01 [head(cons(X, XS))] = [1 0 0] [0 0 0] [0] 52.53/26.01 [0 1 1] X + [0 1 1] XS + [0] 52.53/26.01 [0 1 1] [0 1 1] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 [2nd(cons(X, XS))] = [0 0 0] [2 0 0] [7] 52.53/26.01 [0 7 7] X + [5 7 7] XS + [3] 52.53/26.01 [0 7 7] [5 7 7] [7] 52.53/26.01 > [2 0 0] [0] 52.53/26.01 [5 3 7] XS + [0] 52.53/26.01 [5 3 7] [0] 52.53/26.01 = [head(activate(XS))] 52.53/26.01 52.53/26.01 [activate(X)] = [2 0 0] [0] 52.53/26.01 [0 2 0] X + [0] 52.53/26.01 [5 3 7] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 [activate(n__from(X))] = [2 0 0] [0] 52.53/26.01 [2 0 0] X + [4] 52.53/26.01 [8 7 7] [6] 52.53/26.01 >= [2 0 0] [0] 52.53/26.01 [2 0 0] X + [2] 52.53/26.01 [7 7 7] [4] 52.53/26.01 = [from(activate(X))] 52.53/26.01 52.53/26.01 [activate(n__s(X))] = [2 0 0] [4] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [5 0 0] [10] 52.53/26.01 > [2 0 0] [3] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 = [s(activate(X))] 52.53/26.01 52.53/26.01 [activate(n__take(X1, X2))] = [2 0 0] [2 0 0] [0] 52.53/26.01 [0 0 0] X1 + [0 0 0] X2 + [6] 52.53/26.01 [5 0 0] [5 0 0] [9] 52.53/26.01 >= [2 0 0] [2 0 0] [0] 52.53/26.01 [0 0 0] X1 + [0 0 0] X2 + [3] 52.53/26.01 [0 0 0] [0 0 0] [4] 52.53/26.01 = [take(activate(X1), activate(X2))] 52.53/26.01 52.53/26.01 [take(X1, X2)] = [1 0 0] [1 0 0] [0] 52.53/26.01 [0 0 0] X1 + [0 0 0] X2 + [3] 52.53/26.01 [0 0 0] [0 0 0] [4] 52.53/26.01 >= [1 0 0] [1 0 0] [0] 52.53/26.01 [0 0 0] X1 + [0 0 0] X2 + [3] 52.53/26.01 [0 0 0] [0 0 0] [0] 52.53/26.01 = [n__take(X1, X2)] 52.53/26.01 52.53/26.01 [take(0(), XS)] = [1 0 0] [0] 52.53/26.01 [0 0 0] XS + [3] 52.53/26.01 [0 0 0] [4] 52.53/26.01 >= [0] 52.53/26.01 [3] 52.53/26.01 [4] 52.53/26.01 = [nil()] 52.53/26.01 52.53/26.01 [s(X)] = [1 0 0] [3] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 > [1 0 0] [2] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [0] 52.53/26.01 = [n__s(X)] 52.53/26.01 52.53/26.01 [sel(0(), cons(X, XS))] = [1 0 0] [0 0 0] [7] 52.53/26.01 [0 1 1] X + [0 1 1] XS + [7] 52.53/26.01 [0 1 1] [0 1 1] [7] 52.53/26.01 > [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 52.53/26.01 We return to the main proof. 52.53/26.01 52.53/26.01 We are left with following problem, upon which TcT provides the 52.53/26.01 certificate YES(O(1),O(n^1)). 52.53/26.01 52.53/26.01 Strict Trs: 52.53/26.01 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.01 , from(X) -> n__from(X) 52.53/26.01 , head(cons(X, XS)) -> X 52.53/26.01 , activate(X) -> X 52.53/26.01 , activate(n__from(X)) -> from(activate(X)) 52.53/26.01 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.01 , take(X1, X2) -> n__take(X1, X2) 52.53/26.01 , take(0(), XS) -> nil() } 52.53/26.01 Weak Trs: 52.53/26.01 { 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.01 , activate(n__s(X)) -> s(activate(X)) 52.53/26.01 , s(X) -> n__s(X) 52.53/26.01 , sel(0(), cons(X, XS)) -> X } 52.53/26.01 Obligation: 52.53/26.01 innermost runtime complexity 52.53/26.01 Answer: 52.53/26.01 YES(O(1),O(n^1)) 52.53/26.01 52.53/26.01 We use the processor 'matrix interpretation of dimension 3' to 52.53/26.01 orient following rules strictly. 52.53/26.01 52.53/26.01 Trs: { head(cons(X, XS)) -> X } 52.53/26.01 52.53/26.01 The induced complexity on above rules (modulo remaining rules) is 52.53/26.01 YES(?,O(n^1)) . These rules are moved into the corresponding weak 52.53/26.01 component(s). 52.53/26.01 52.53/26.01 Sub-proof: 52.53/26.01 ---------- 52.53/26.01 The following argument positions are usable: 52.53/26.01 Uargs(from) = {1}, Uargs(head) = {1}, Uargs(take) = {1, 2}, 52.53/26.01 Uargs(s) = {1} 52.53/26.01 52.53/26.01 TcT has computed the following constructor-based matrix 52.53/26.01 interpretation satisfying not(EDA) and not(IDA(1)). 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [from](x1) = [0 1 2] x1 + [6] 52.53/26.01 [4 0 0] [4] 52.53/26.01 52.53/26.01 [0 0 0] [1 0 0] [0] 52.53/26.01 [cons](x1, x2) = [0 1 1] x1 + [0 1 0] x2 + [0] 52.53/26.01 [1 0 0] [0 0 1] [0] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [n__from](x1) = [0 1 2] x1 + [2] 52.53/26.01 [1 0 0] [2] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [n__s](x1) = [0 0 0] x1 + [0] 52.53/26.01 [0 0 0] [2] 52.53/26.01 52.53/26.01 [1 0 1] [1] 52.53/26.01 [head](x1) = [0 1 0] x1 + [0] 52.53/26.01 [0 1 0] [0] 52.53/26.01 52.53/26.01 [4 0 4] [3] 52.53/26.01 [2nd](x1) = [4 4 0] x1 + [7] 52.53/26.01 [0 4 4] [7] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [activate](x1) = [0 4 0] x1 + [4] 52.53/26.01 [0 0 4] [0] 52.53/26.01 52.53/26.01 [1 0 0] [1 0 0] [0] 52.53/26.01 [take](x1, x2) = [0 1 0] x1 + [0 0 0] x2 + [2] 52.53/26.01 [0 0 1] [0 0 0] [2] 52.53/26.01 52.53/26.01 [0] 52.53/26.01 [0] = [0] 52.53/26.01 [0] 52.53/26.01 52.53/26.01 [0] 52.53/26.01 [nil] = [1] 52.53/26.01 [1] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [s](x1) = [0 0 0] x1 + [0] 52.53/26.01 [0 0 0] [4] 52.53/26.01 52.53/26.01 [1 0 0] [1 0 0] [0] 52.53/26.01 [n__take](x1, x2) = [0 1 0] x1 + [0 0 0] x2 + [1] 52.53/26.01 [0 0 1] [0 0 0] [2] 52.53/26.01 52.53/26.01 [7 0 4] [0 0 2] [7] 52.53/26.01 [sel](x1, x2) = [7 7 7] x1 + [0 1 0] x2 + [7] 52.53/26.01 [7 7 7] [0 1 0] [7] 52.53/26.01 52.53/26.01 The order satisfies the following ordering constraints: 52.53/26.01 52.53/26.01 [from(X)] = [1 0 0] [0] 52.53/26.01 [0 1 2] X + [6] 52.53/26.01 [4 0 0] [4] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 1] X + [6] 52.53/26.01 [2 0 0] [2] 52.53/26.01 = [cons(X, n__from(n__s(X)))] 52.53/26.01 52.53/26.01 [from(X)] = [1 0 0] [0] 52.53/26.01 [0 1 2] X + [6] 52.53/26.01 [4 0 0] [4] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 2] X + [2] 52.53/26.01 [1 0 0] [2] 52.53/26.01 = [n__from(X)] 52.53/26.01 52.53/26.01 [head(cons(X, XS))] = [1 0 0] [1 0 1] [1] 52.53/26.01 [0 1 1] X + [0 1 0] XS + [0] 52.53/26.01 [0 1 1] [0 1 0] [0] 52.53/26.01 > [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 [2nd(cons(X, XS))] = [4 0 0] [4 0 4] [3] 52.53/26.01 [0 4 4] X + [4 4 0] XS + [7] 52.53/26.01 [4 4 4] [0 4 4] [7] 52.53/26.01 > [1 0 4] [1] 52.53/26.01 [0 4 0] XS + [4] 52.53/26.01 [0 4 0] [4] 52.53/26.01 = [head(activate(XS))] 52.53/26.01 52.53/26.01 [activate(X)] = [1 0 0] [0] 52.53/26.01 [0 4 0] X + [4] 52.53/26.01 [0 0 4] [0] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 [activate(n__from(X))] = [1 0 0] [0] 52.53/26.01 [0 4 8] X + [12] 52.53/26.01 [4 0 0] [8] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 4 8] X + [10] 52.53/26.01 [4 0 0] [4] 52.53/26.01 = [from(activate(X))] 52.53/26.01 52.53/26.01 [activate(n__s(X))] = [1 0 0] [0] 52.53/26.01 [0 0 0] X + [4] 52.53/26.01 [0 0 0] [8] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [4] 52.53/26.01 = [s(activate(X))] 52.53/26.01 52.53/26.01 [activate(n__take(X1, X2))] = [1 0 0] [1 0 0] [0] 52.53/26.01 [0 4 0] X1 + [0 0 0] X2 + [8] 52.53/26.01 [0 0 4] [0 0 0] [8] 52.53/26.01 >= [1 0 0] [1 0 0] [0] 52.53/26.01 [0 4 0] X1 + [0 0 0] X2 + [6] 52.53/26.01 [0 0 4] [0 0 0] [2] 52.53/26.01 = [take(activate(X1), activate(X2))] 52.53/26.01 52.53/26.01 [take(X1, X2)] = [1 0 0] [1 0 0] [0] 52.53/26.01 [0 1 0] X1 + [0 0 0] X2 + [2] 52.53/26.01 [0 0 1] [0 0 0] [2] 52.53/26.01 >= [1 0 0] [1 0 0] [0] 52.53/26.01 [0 1 0] X1 + [0 0 0] X2 + [1] 52.53/26.01 [0 0 1] [0 0 0] [2] 52.53/26.01 = [n__take(X1, X2)] 52.53/26.01 52.53/26.01 [take(0(), XS)] = [1 0 0] [0] 52.53/26.01 [0 0 0] XS + [2] 52.53/26.01 [0 0 0] [2] 52.53/26.01 >= [0] 52.53/26.01 [1] 52.53/26.01 [1] 52.53/26.01 = [nil()] 52.53/26.01 52.53/26.01 [s(X)] = [1 0 0] [0] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [4] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 0 0] X + [0] 52.53/26.01 [0 0 0] [2] 52.53/26.01 = [n__s(X)] 52.53/26.01 52.53/26.01 [sel(0(), cons(X, XS))] = [2 0 0] [0 0 2] [7] 52.53/26.01 [0 1 1] X + [0 1 0] XS + [7] 52.53/26.01 [0 1 1] [0 1 0] [7] 52.53/26.01 > [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 52.53/26.01 We return to the main proof. 52.53/26.01 52.53/26.01 We are left with following problem, upon which TcT provides the 52.53/26.01 certificate YES(O(1),O(n^1)). 52.53/26.01 52.53/26.01 Strict Trs: 52.53/26.01 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.01 , from(X) -> n__from(X) 52.53/26.01 , activate(X) -> X 52.53/26.01 , activate(n__from(X)) -> from(activate(X)) 52.53/26.01 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.01 , take(X1, X2) -> n__take(X1, X2) 52.53/26.01 , take(0(), XS) -> nil() } 52.53/26.01 Weak Trs: 52.53/26.01 { head(cons(X, XS)) -> X 52.53/26.01 , 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.01 , activate(n__s(X)) -> s(activate(X)) 52.53/26.01 , s(X) -> n__s(X) 52.53/26.01 , sel(0(), cons(X, XS)) -> X } 52.53/26.01 Obligation: 52.53/26.01 innermost runtime complexity 52.53/26.01 Answer: 52.53/26.01 YES(O(1),O(n^1)) 52.53/26.01 52.53/26.01 We use the processor 'matrix interpretation of dimension 3' to 52.53/26.01 orient following rules strictly. 52.53/26.01 52.53/26.01 Trs: { take(0(), XS) -> nil() } 52.53/26.01 52.53/26.01 The induced complexity on above rules (modulo remaining rules) is 52.53/26.01 YES(?,O(n^1)) . These rules are moved into the corresponding weak 52.53/26.01 component(s). 52.53/26.01 52.53/26.01 Sub-proof: 52.53/26.01 ---------- 52.53/26.01 The following argument positions are usable: 52.53/26.01 Uargs(from) = {1}, Uargs(head) = {1}, Uargs(take) = {1, 2}, 52.53/26.01 Uargs(s) = {1} 52.53/26.01 52.53/26.01 TcT has computed the following constructor-based matrix 52.53/26.01 interpretation satisfying not(EDA) and not(IDA(1)). 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [from](x1) = [1 0 0] x1 + [4] 52.53/26.01 [0 2 1] [7] 52.53/26.01 52.53/26.01 [1 0 0] [0 0 0] [0] 52.53/26.01 [cons](x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [2] 52.53/26.01 [0 1 1] [0 0 1] [0] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [n__from](x1) = [1 0 0] x1 + [4] 52.53/26.01 [0 1 1] [4] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [n__s](x1) = [0 0 0] x1 + [0] 52.53/26.01 [0 0 0] [3] 52.53/26.01 52.53/26.01 [4 0 0] [0] 52.53/26.01 [head](x1) = [0 0 2] x1 + [0] 52.53/26.01 [0 0 1] [2] 52.53/26.01 52.53/26.01 [0 4 0] [3] 52.53/26.01 [2nd](x1) = [0 0 4] x1 + [7] 52.53/26.01 [0 0 2] [7] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [activate](x1) = [0 1 0] x1 + [0] 52.53/26.01 [0 0 2] [2] 52.53/26.01 52.53/26.01 [1 0 0] [1 0 0] [0] 52.53/26.01 [take](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] 52.53/26.01 [0 0 0] [0 1 0] [2] 52.53/26.01 52.53/26.01 [1] 52.53/26.01 [0] = [0] 52.53/26.01 [0] 52.53/26.01 52.53/26.01 [0] 52.53/26.01 [nil] = [0] 52.53/26.01 [1] 52.53/26.01 52.53/26.01 [1 0 0] [0] 52.53/26.01 [s](x1) = [0 0 0] x1 + [0] 52.53/26.01 [0 0 0] [3] 52.53/26.01 52.53/26.01 [1 0 0] [1 0 0] [0] 52.53/26.01 [n__take](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] 52.53/26.01 [0 0 0] [0 1 0] [2] 52.53/26.01 52.53/26.01 [0 4 0] [4 0 0] [7] 52.53/26.01 [sel](x1, x2) = [0 7 7] x1 + [0 0 2] x2 + [7] 52.53/26.01 [0 7 7] [0 0 1] [7] 52.53/26.01 52.53/26.01 The order satisfies the following ordering constraints: 52.53/26.01 52.53/26.01 [from(X)] = [1 0 0] [0] 52.53/26.01 [1 0 0] X + [4] 52.53/26.01 [0 2 1] [7] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [1 0 0] X + [2] 52.53/26.01 [0 1 1] [7] 52.53/26.01 = [cons(X, n__from(n__s(X)))] 52.53/26.01 52.53/26.01 [from(X)] = [1 0 0] [0] 52.53/26.01 [1 0 0] X + [4] 52.53/26.01 [0 2 1] [7] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [1 0 0] X + [4] 52.53/26.01 [0 1 1] [4] 52.53/26.01 = [n__from(X)] 52.53/26.01 52.53/26.01 [head(cons(X, XS))] = [4 0 0] [0 0 0] [0] 52.53/26.01 [0 2 2] X + [0 0 2] XS + [0] 52.53/26.01 [0 1 1] [0 0 1] [2] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 [2nd(cons(X, XS))] = [0 0 0] [4 0 0] [11] 52.53/26.01 [0 4 4] X + [0 0 4] XS + [7] 52.53/26.01 [0 2 2] [0 0 2] [7] 52.53/26.01 > [4 0 0] [0] 52.53/26.01 [0 0 4] XS + [4] 52.53/26.01 [0 0 2] [4] 52.53/26.01 = [head(activate(XS))] 52.53/26.01 52.53/26.01 [activate(X)] = [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 2] [2] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [0 1 0] X + [0] 52.53/26.01 [0 0 1] [0] 52.53/26.01 = [X] 52.53/26.01 52.53/26.01 [activate(n__from(X))] = [1 0 0] [0] 52.53/26.01 [1 0 0] X + [4] 52.53/26.01 [0 2 2] [10] 52.53/26.01 >= [1 0 0] [0] 52.53/26.01 [1 0 0] X + [4] 52.53/26.01 [0 2 2] [9] 52.53/26.01 = [from(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__s(X))] = [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [8] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [3] 52.53/26.02 = [s(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__take(X1, X2))] = [1 0 0] [1 0 0] [0] 52.53/26.02 [0 0 0] X1 + [0 0 0] X2 + [0] 52.53/26.02 [0 0 0] [0 2 0] [6] 52.53/26.02 >= [1 0 0] [1 0 0] [0] 52.53/26.02 [0 0 0] X1 + [0 0 0] X2 + [0] 52.53/26.02 [0 0 0] [0 1 0] [2] 52.53/26.02 = [take(activate(X1), activate(X2))] 52.53/26.02 52.53/26.02 [take(X1, X2)] = [1 0 0] [1 0 0] [0] 52.53/26.02 [0 0 0] X1 + [0 0 0] X2 + [0] 52.53/26.02 [0 0 0] [0 1 0] [2] 52.53/26.02 >= [1 0 0] [1 0 0] [0] 52.53/26.02 [0 0 0] X1 + [0 0 0] X2 + [0] 52.53/26.02 [0 0 0] [0 1 0] [2] 52.53/26.02 = [n__take(X1, X2)] 52.53/26.02 52.53/26.02 [take(0(), XS)] = [1 0 0] [1] 52.53/26.02 [0 0 0] XS + [0] 52.53/26.02 [0 1 0] [2] 52.53/26.02 > [0] 52.53/26.02 [0] 52.53/26.02 [1] 52.53/26.02 = [nil()] 52.53/26.02 52.53/26.02 [s(X)] = [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [3] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [3] 52.53/26.02 = [n__s(X)] 52.53/26.02 52.53/26.02 [sel(0(), cons(X, XS))] = [4 0 0] [0 0 0] [7] 52.53/26.02 [0 2 2] X + [0 0 2] XS + [7] 52.53/26.02 [0 1 1] [0 0 1] [7] 52.53/26.02 > [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 52.53/26.02 We return to the main proof. 52.53/26.02 52.53/26.02 We are left with following problem, upon which TcT provides the 52.53/26.02 certificate YES(O(1),O(n^1)). 52.53/26.02 52.53/26.02 Strict Trs: 52.53/26.02 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.02 , from(X) -> n__from(X) 52.53/26.02 , activate(X) -> X 52.53/26.02 , activate(n__from(X)) -> from(activate(X)) 52.53/26.02 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.02 , take(X1, X2) -> n__take(X1, X2) } 52.53/26.02 Weak Trs: 52.53/26.02 { head(cons(X, XS)) -> X 52.53/26.02 , 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.02 , activate(n__s(X)) -> s(activate(X)) 52.53/26.02 , take(0(), XS) -> nil() 52.53/26.02 , s(X) -> n__s(X) 52.53/26.02 , sel(0(), cons(X, XS)) -> X } 52.53/26.02 Obligation: 52.53/26.02 innermost runtime complexity 52.53/26.02 Answer: 52.53/26.02 YES(O(1),O(n^1)) 52.53/26.02 52.53/26.02 We use the processor 'matrix interpretation of dimension 3' to 52.53/26.02 orient following rules strictly. 52.53/26.02 52.53/26.02 Trs: 52.53/26.02 { activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) } 52.53/26.02 52.53/26.02 The induced complexity on above rules (modulo remaining rules) is 52.53/26.02 YES(?,O(n^1)) . These rules are moved into the corresponding weak 52.53/26.02 component(s). 52.53/26.02 52.53/26.02 Sub-proof: 52.53/26.02 ---------- 52.53/26.02 The following argument positions are usable: 52.53/26.02 Uargs(from) = {1}, Uargs(head) = {1}, Uargs(take) = {1, 2}, 52.53/26.02 Uargs(s) = {1} 52.53/26.02 52.53/26.02 TcT has computed the following constructor-based matrix 52.53/26.02 interpretation satisfying not(EDA) and not(IDA(1)). 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [from](x1) = [2 1 2] x1 + [0] 52.53/26.02 [4 0 0] [0] 52.53/26.02 52.53/26.02 [0 0 0] [0 0 0] [0] 52.53/26.02 [cons](x1, x2) = [0 1 2] x1 + [0 1 1] x2 + [0] 52.53/26.02 [1 0 0] [1 0 1] [0] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [n__from](x1) = [1 1 2] x1 + [0] 52.53/26.02 [1 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [n__s](x1) = [0 0 0] x1 + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 1] [0] 52.53/26.02 [head](x1) = [0 1 0] x1 + [0] 52.53/26.02 [0 1 0] [0] 52.53/26.02 52.53/26.02 [0 0 7] [3] 52.53/26.02 [2nd](x1) = [0 7 0] x1 + [7] 52.53/26.02 [0 7 4] [7] 52.53/26.02 52.53/26.02 [2 0 0] [0] 52.53/26.02 [activate](x1) = [0 7 7] x1 + [0] 52.53/26.02 [5 0 3] [0] 52.53/26.02 52.53/26.02 [1 0 0] [1 0 0] [1] 52.53/26.02 [take](x1, x2) = [1 1 2] x1 + [0 0 0] x2 + [4] 52.53/26.02 [4 0 0] [0 0 0] [0] 52.53/26.02 52.53/26.02 [0] 52.53/26.02 [0] = [0] 52.53/26.02 [0] 52.53/26.02 52.53/26.02 [1] 52.53/26.02 [nil] = [4] 52.53/26.02 [0] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [s](x1) = [0 0 0] x1 + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 0] [1 0 0] [1] 52.53/26.02 [n__take](x1, x2) = [1 1 2] x1 + [0 0 0] x2 + [1] 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 52.53/26.02 [7 0 4] [0 0 4] [7] 52.53/26.02 [sel](x1, x2) = [7 7 7] x1 + [0 2 0] x2 + [7] 52.53/26.02 [7 7 7] [0 1 0] [7] 52.53/26.02 52.53/26.02 The order satisfies the following ordering constraints: 52.53/26.02 52.53/26.02 [from(X)] = [1 0 0] [0] 52.53/26.02 [2 1 2] X + [0] 52.53/26.02 [4 0 0] [0] 52.53/26.02 >= [0 0 0] [0] 52.53/26.02 [2 1 2] X + [0] 52.53/26.02 [3 0 0] [0] 52.53/26.02 = [cons(X, n__from(n__s(X)))] 52.53/26.02 52.53/26.02 [from(X)] = [1 0 0] [0] 52.53/26.02 [2 1 2] X + [0] 52.53/26.02 [4 0 0] [0] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [1 1 2] X + [0] 52.53/26.02 [1 0 0] [0] 52.53/26.02 = [n__from(X)] 52.53/26.02 52.53/26.02 [head(cons(X, XS))] = [1 0 0] [1 0 1] [0] 52.53/26.02 [0 1 2] X + [0 1 1] XS + [0] 52.53/26.02 [0 1 2] [0 1 1] [0] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 [2nd(cons(X, XS))] = [7 0 0] [7 0 7] [3] 52.53/26.02 [0 7 14] X + [0 7 7] XS + [7] 52.53/26.02 [4 7 14] [4 7 11] [7] 52.53/26.02 > [7 0 3] [0] 52.53/26.02 [0 7 7] XS + [0] 52.53/26.02 [0 7 7] [0] 52.53/26.02 = [head(activate(XS))] 52.53/26.02 52.53/26.02 [activate(X)] = [2 0 0] [0] 52.53/26.02 [0 7 7] X + [0] 52.53/26.02 [5 0 3] [0] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 [activate(n__from(X))] = [ 2 0 0] [0] 52.53/26.02 [14 7 14] X + [0] 52.53/26.02 [ 8 0 0] [0] 52.53/26.02 >= [ 2 0 0] [0] 52.53/26.02 [14 7 13] X + [0] 52.53/26.02 [ 8 0 0] [0] 52.53/26.02 = [from(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__s(X))] = [2 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [5 0 0] [0] 52.53/26.02 >= [2 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 = [s(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__take(X1, X2))] = [ 2 0 0] [2 0 0] [2] 52.53/26.02 [14 7 14] X1 + [0 0 0] X2 + [7] 52.53/26.02 [ 8 0 0] [5 0 0] [5] 52.53/26.02 > [ 2 0 0] [2 0 0] [1] 52.53/26.02 [12 7 13] X1 + [0 0 0] X2 + [4] 52.53/26.02 [ 8 0 0] [0 0 0] [0] 52.53/26.02 = [take(activate(X1), activate(X2))] 52.53/26.02 52.53/26.02 [take(X1, X2)] = [1 0 0] [1 0 0] [1] 52.53/26.02 [1 1 2] X1 + [0 0 0] X2 + [4] 52.53/26.02 [4 0 0] [0 0 0] [0] 52.53/26.02 >= [1 0 0] [1 0 0] [1] 52.53/26.02 [1 1 2] X1 + [0 0 0] X2 + [1] 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 = [n__take(X1, X2)] 52.53/26.02 52.53/26.02 [take(0(), XS)] = [1 0 0] [1] 52.53/26.02 [0 0 0] XS + [4] 52.53/26.02 [0 0 0] [0] 52.53/26.02 >= [1] 52.53/26.02 [4] 52.53/26.02 [0] 52.53/26.02 = [nil()] 52.53/26.02 52.53/26.02 [s(X)] = [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 = [n__s(X)] 52.53/26.02 52.53/26.02 [sel(0(), cons(X, XS))] = [4 0 0] [4 0 4] [7] 52.53/26.02 [0 2 4] X + [0 2 2] XS + [7] 52.53/26.02 [0 1 2] [0 1 1] [7] 52.53/26.02 > [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 52.53/26.02 We return to the main proof. 52.53/26.02 52.53/26.02 We are left with following problem, upon which TcT provides the 52.53/26.02 certificate YES(O(1),O(n^1)). 52.53/26.02 52.53/26.02 Strict Trs: 52.53/26.02 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.02 , from(X) -> n__from(X) 52.53/26.02 , activate(X) -> X 52.53/26.02 , activate(n__from(X)) -> from(activate(X)) 52.53/26.02 , take(X1, X2) -> n__take(X1, X2) } 52.53/26.02 Weak Trs: 52.53/26.02 { head(cons(X, XS)) -> X 52.53/26.02 , 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.02 , activate(n__s(X)) -> s(activate(X)) 52.53/26.02 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.02 , take(0(), XS) -> nil() 52.53/26.02 , s(X) -> n__s(X) 52.53/26.02 , sel(0(), cons(X, XS)) -> X } 52.53/26.02 Obligation: 52.53/26.02 innermost runtime complexity 52.53/26.02 Answer: 52.53/26.02 YES(O(1),O(n^1)) 52.53/26.02 52.53/26.02 We use the processor 'matrix interpretation of dimension 3' to 52.53/26.02 orient following rules strictly. 52.53/26.02 52.53/26.02 Trs: { take(X1, X2) -> n__take(X1, X2) } 52.53/26.02 52.53/26.02 The induced complexity on above rules (modulo remaining rules) is 52.53/26.02 YES(?,O(n^1)) . These rules are moved into the corresponding weak 52.53/26.02 component(s). 52.53/26.02 52.53/26.02 Sub-proof: 52.53/26.02 ---------- 52.53/26.02 The following argument positions are usable: 52.53/26.02 Uargs(from) = {1}, Uargs(head) = {1}, Uargs(take) = {1, 2}, 52.53/26.02 Uargs(s) = {1} 52.53/26.02 52.53/26.02 TcT has computed the following constructor-based matrix 52.53/26.02 interpretation satisfying not(EDA) and not(IDA(1)). 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [from](x1) = [0 1 4] x1 + [0] 52.53/26.02 [1 0 0] [4] 52.53/26.02 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 [cons](x1, x2) = [0 1 2] x1 + [0 1 0] x2 + [0] 52.53/26.02 [0 0 0] [1 0 0] [1] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [n__from](x1) = [0 1 3] x1 + [0] 52.53/26.02 [1 0 0] [4] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [n__s](x1) = [0 0 0] x1 + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [head](x1) = [0 1 0] x1 + [0] 52.53/26.02 [0 1 0] [0] 52.53/26.02 52.53/26.02 [0 0 2] [7] 52.53/26.02 [2nd](x1) = [0 3 4] x1 + [3] 52.53/26.02 [0 3 1] [7] 52.53/26.02 52.53/26.02 [2 0 0] [0] 52.53/26.02 [activate](x1) = [0 3 0] x1 + [0] 52.53/26.02 [0 0 2] [0] 52.53/26.02 52.53/26.02 [1 0 0] [1 0 0] [5] 52.53/26.02 [take](x1, x2) = [0 1 1] x1 + [0 0 0] x2 + [0] 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 52.53/26.02 [0] 52.53/26.02 [0] = [0] 52.53/26.02 [0] 52.53/26.02 52.53/26.02 [3] 52.53/26.02 [nil] = [0] 52.53/26.02 [0] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [s](x1) = [0 0 0] x1 + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 0] [1 0 0] [4] 52.53/26.02 [n__take](x1, x2) = [0 1 1] x1 + [0 0 0] x2 + [0] 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 52.53/26.02 [7 0 4] [4 0 0] [7] 52.53/26.02 [sel](x1, x2) = [7 7 7] x1 + [0 1 0] x2 + [7] 52.53/26.02 [7 7 7] [0 1 0] [7] 52.53/26.02 52.53/26.02 The order satisfies the following ordering constraints: 52.53/26.02 52.53/26.02 [from(X)] = [1 0 0] [0] 52.53/26.02 [0 1 4] X + [0] 52.53/26.02 [1 0 0] [4] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 2] X + [0] 52.53/26.02 [1 0 0] [1] 52.53/26.02 = [cons(X, n__from(n__s(X)))] 52.53/26.02 52.53/26.02 [from(X)] = [1 0 0] [0] 52.53/26.02 [0 1 4] X + [0] 52.53/26.02 [1 0 0] [4] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 3] X + [0] 52.53/26.02 [1 0 0] [4] 52.53/26.02 = [n__from(X)] 52.53/26.02 52.53/26.02 [head(cons(X, XS))] = [1 0 0] [0 0 0] [0] 52.53/26.02 [0 1 2] X + [0 1 0] XS + [0] 52.53/26.02 [0 1 2] [0 1 0] [0] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 [2nd(cons(X, XS))] = [0 0 0] [2 0 0] [9] 52.53/26.02 [0 3 6] X + [4 3 0] XS + [7] 52.53/26.02 [0 3 6] [1 3 0] [8] 52.53/26.02 > [2 0 0] [0] 52.53/26.02 [0 3 0] XS + [0] 52.53/26.02 [0 3 0] [0] 52.53/26.02 = [head(activate(XS))] 52.53/26.02 52.53/26.02 [activate(X)] = [2 0 0] [0] 52.53/26.02 [0 3 0] X + [0] 52.53/26.02 [0 0 2] [0] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 [activate(n__from(X))] = [2 0 0] [0] 52.53/26.02 [0 3 9] X + [0] 52.53/26.02 [2 0 0] [8] 52.53/26.02 >= [2 0 0] [0] 52.53/26.02 [0 3 8] X + [0] 52.53/26.02 [2 0 0] [4] 52.53/26.02 = [from(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__s(X))] = [2 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 >= [2 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 = [s(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__take(X1, X2))] = [2 0 0] [2 0 0] [8] 52.53/26.02 [0 3 3] X1 + [0 0 0] X2 + [0] 52.53/26.02 [2 0 0] [0 0 0] [0] 52.53/26.02 > [2 0 0] [2 0 0] [5] 52.53/26.02 [0 3 2] X1 + [0 0 0] X2 + [0] 52.53/26.02 [2 0 0] [0 0 0] [0] 52.53/26.02 = [take(activate(X1), activate(X2))] 52.53/26.02 52.53/26.02 [take(X1, X2)] = [1 0 0] [1 0 0] [5] 52.53/26.02 [0 1 1] X1 + [0 0 0] X2 + [0] 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 > [1 0 0] [1 0 0] [4] 52.53/26.02 [0 1 1] X1 + [0 0 0] X2 + [0] 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 = [n__take(X1, X2)] 52.53/26.02 52.53/26.02 [take(0(), XS)] = [1 0 0] [5] 52.53/26.02 [0 0 0] XS + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 > [3] 52.53/26.02 [0] 52.53/26.02 [0] 52.53/26.02 = [nil()] 52.53/26.02 52.53/26.02 [s(X)] = [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 = [n__s(X)] 52.53/26.02 52.53/26.02 [sel(0(), cons(X, XS))] = [4 0 0] [0 0 0] [7] 52.53/26.02 [0 1 2] X + [0 1 0] XS + [7] 52.53/26.02 [0 1 2] [0 1 0] [7] 52.53/26.02 > [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 52.53/26.02 We return to the main proof. 52.53/26.02 52.53/26.02 We are left with following problem, upon which TcT provides the 52.53/26.02 certificate YES(O(1),O(n^1)). 52.53/26.02 52.53/26.02 Strict Trs: 52.53/26.02 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.02 , from(X) -> n__from(X) 52.53/26.02 , activate(X) -> X 52.53/26.02 , activate(n__from(X)) -> from(activate(X)) } 52.53/26.02 Weak Trs: 52.53/26.02 { head(cons(X, XS)) -> X 52.53/26.02 , 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.02 , activate(n__s(X)) -> s(activate(X)) 52.53/26.02 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.02 , take(X1, X2) -> n__take(X1, X2) 52.53/26.02 , take(0(), XS) -> nil() 52.53/26.02 , s(X) -> n__s(X) 52.53/26.02 , sel(0(), cons(X, XS)) -> X } 52.53/26.02 Obligation: 52.53/26.02 innermost runtime complexity 52.53/26.02 Answer: 52.53/26.02 YES(O(1),O(n^1)) 52.53/26.02 52.53/26.02 We use the processor 'matrix interpretation of dimension 3' to 52.53/26.02 orient following rules strictly. 52.53/26.02 52.53/26.02 Trs: 52.53/26.02 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.02 , from(X) -> n__from(X) 52.53/26.02 , activate(n__from(X)) -> from(activate(X)) } 52.53/26.02 52.53/26.02 The induced complexity on above rules (modulo remaining rules) is 52.53/26.02 YES(?,O(n^1)) . These rules are moved into the corresponding weak 52.53/26.02 component(s). 52.53/26.02 52.53/26.02 Sub-proof: 52.53/26.02 ---------- 52.53/26.02 The following argument positions are usable: 52.53/26.02 Uargs(from) = {1}, Uargs(head) = {1}, Uargs(take) = {1, 2}, 52.53/26.02 Uargs(s) = {1} 52.53/26.02 52.53/26.02 TcT has computed the following constructor-based matrix 52.53/26.02 interpretation satisfying not(EDA) and not(IDA(1)). 52.53/26.02 52.53/26.02 [1 0 0] [3] 52.53/26.02 [from](x1) = [1 1 1] x1 + [1] 52.53/26.02 [1 0 0] [4] 52.53/26.02 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 [cons](x1, x2) = [0 1 1] x1 + [0 1 1] x2 + [0] 52.53/26.02 [0 0 0] [1 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 0] [2] 52.53/26.02 [n__from](x1) = [0 1 1] x1 + [0] 52.53/26.02 [1 0 0] [1] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [n__s](x1) = [0 0 0] x1 + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [head](x1) = [0 1 0] x1 + [0] 52.53/26.02 [0 1 0] [2] 52.53/26.02 52.53/26.02 [0 0 2] [3] 52.53/26.02 [2nd](x1) = [0 7 5] x1 + [7] 52.53/26.02 [0 7 5] [7] 52.53/26.02 52.53/26.02 [2 0 0] [0] 52.53/26.02 [activate](x1) = [5 7 3] x1 + [2] 52.53/26.02 [0 0 4] [6] 52.53/26.02 52.53/26.02 [1 0 0] [1 0 0] [2] 52.53/26.02 [take](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] 52.53/26.02 [1 0 0] [0 0 0] [4] 52.53/26.02 52.53/26.02 [0] 52.53/26.02 [0] = [0] 52.53/26.02 [0] 52.53/26.02 52.53/26.02 [1] 52.53/26.02 [nil] = [0] 52.53/26.02 [4] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [s](x1) = [0 0 0] x1 + [0] 52.53/26.02 [0 0 0] [4] 52.53/26.02 52.53/26.02 [1 0 0] [1 0 0] [2] 52.53/26.02 [n__take](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 52.53/26.02 [7 0 4] [4 0 0] [7] 52.53/26.02 [sel](x1, x2) = [7 7 7] x1 + [0 4 0] x2 + [7] 52.53/26.02 [7 7 7] [0 1 0] [7] 52.53/26.02 52.53/26.02 The order satisfies the following ordering constraints: 52.53/26.02 52.53/26.02 [from(X)] = [1 0 0] [3] 52.53/26.02 [1 1 1] X + [1] 52.53/26.02 [1 0 0] [4] 52.53/26.02 > [1 0 0] [0] 52.53/26.02 [1 1 1] X + [1] 52.53/26.02 [1 0 0] [2] 52.53/26.02 = [cons(X, n__from(n__s(X)))] 52.53/26.02 52.53/26.02 [from(X)] = [1 0 0] [3] 52.53/26.02 [1 1 1] X + [1] 52.53/26.02 [1 0 0] [4] 52.53/26.02 > [1 0 0] [2] 52.53/26.02 [0 1 1] X + [0] 52.53/26.02 [1 0 0] [1] 52.53/26.02 = [n__from(X)] 52.53/26.02 52.53/26.02 [head(cons(X, XS))] = [1 0 0] [0 0 0] [0] 52.53/26.02 [0 1 1] X + [0 1 1] XS + [0] 52.53/26.02 [0 1 1] [0 1 1] [2] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 [2nd(cons(X, XS))] = [0 0 0] [2 0 0] [3] 52.53/26.02 [0 7 7] X + [5 7 7] XS + [7] 52.53/26.02 [0 7 7] [5 7 7] [7] 52.53/26.02 > [2 0 0] [0] 52.53/26.02 [5 7 3] XS + [2] 52.53/26.02 [5 7 3] [4] 52.53/26.02 = [head(activate(XS))] 52.53/26.02 52.53/26.02 [activate(X)] = [2 0 0] [0] 52.53/26.02 [5 7 3] X + [2] 52.53/26.02 [0 0 4] [6] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 [activate(n__from(X))] = [2 0 0] [4] 52.53/26.02 [8 7 7] X + [15] 52.53/26.02 [4 0 0] [10] 52.53/26.02 > [2 0 0] [3] 52.53/26.02 [7 7 7] X + [9] 52.53/26.02 [2 0 0] [4] 52.53/26.02 = [from(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__s(X))] = [2 0 0] [0] 52.53/26.02 [5 0 0] X + [2] 52.53/26.02 [0 0 0] [6] 52.53/26.02 >= [2 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [4] 52.53/26.02 = [s(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__take(X1, X2))] = [2 0 0] [2 0 0] [4] 52.53/26.02 [8 0 0] X1 + [5 0 0] X2 + [12] 52.53/26.02 [4 0 0] [0 0 0] [6] 52.53/26.02 > [2 0 0] [2 0 0] [2] 52.53/26.02 [0 0 0] X1 + [0 0 0] X2 + [0] 52.53/26.02 [2 0 0] [0 0 0] [4] 52.53/26.02 = [take(activate(X1), activate(X2))] 52.53/26.02 52.53/26.02 [take(X1, X2)] = [1 0 0] [1 0 0] [2] 52.53/26.02 [0 0 0] X1 + [0 0 0] X2 + [0] 52.53/26.02 [1 0 0] [0 0 0] [4] 52.53/26.02 >= [1 0 0] [1 0 0] [2] 52.53/26.02 [0 0 0] X1 + [0 0 0] X2 + [0] 52.53/26.02 [1 0 0] [0 0 0] [0] 52.53/26.02 = [n__take(X1, X2)] 52.53/26.02 52.53/26.02 [take(0(), XS)] = [1 0 0] [2] 52.53/26.02 [0 0 0] XS + [0] 52.53/26.02 [0 0 0] [4] 52.53/26.02 > [1] 52.53/26.02 [0] 52.53/26.02 [4] 52.53/26.02 = [nil()] 52.53/26.02 52.53/26.02 [s(X)] = [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [4] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 0 0] X + [0] 52.53/26.02 [0 0 0] [0] 52.53/26.02 = [n__s(X)] 52.53/26.02 52.53/26.02 [sel(0(), cons(X, XS))] = [4 0 0] [0 0 0] [7] 52.53/26.02 [0 4 4] X + [0 4 4] XS + [7] 52.53/26.02 [0 1 1] [0 1 1] [7] 52.53/26.02 > [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 52.53/26.02 We return to the main proof. 52.53/26.02 52.53/26.02 We are left with following problem, upon which TcT provides the 52.53/26.02 certificate YES(O(1),O(n^1)). 52.53/26.02 52.53/26.02 Strict Trs: { activate(X) -> X } 52.53/26.02 Weak Trs: 52.53/26.02 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.02 , from(X) -> n__from(X) 52.53/26.02 , head(cons(X, XS)) -> X 52.53/26.02 , 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.02 , activate(n__from(X)) -> from(activate(X)) 52.53/26.02 , activate(n__s(X)) -> s(activate(X)) 52.53/26.02 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.02 , take(X1, X2) -> n__take(X1, X2) 52.53/26.02 , take(0(), XS) -> nil() 52.53/26.02 , s(X) -> n__s(X) 52.53/26.02 , sel(0(), cons(X, XS)) -> X } 52.53/26.02 Obligation: 52.53/26.02 innermost runtime complexity 52.53/26.02 Answer: 52.53/26.02 YES(O(1),O(n^1)) 52.53/26.02 52.53/26.02 We use the processor 'matrix interpretation of dimension 3' to 52.53/26.02 orient following rules strictly. 52.53/26.02 52.53/26.02 Trs: { activate(X) -> X } 52.53/26.02 52.53/26.02 The induced complexity on above rules (modulo remaining rules) is 52.53/26.02 YES(?,O(n^1)) . These rules are moved into the corresponding weak 52.53/26.02 component(s). 52.53/26.02 52.53/26.02 Sub-proof: 52.53/26.02 ---------- 52.53/26.02 The following argument positions are usable: 52.53/26.02 Uargs(from) = {1}, Uargs(head) = {1}, Uargs(take) = {1, 2}, 52.53/26.02 Uargs(s) = {1} 52.53/26.02 52.53/26.02 TcT has computed the following constructor-based matrix 52.53/26.02 interpretation satisfying not(EDA) and not(IDA(1)). 52.53/26.02 52.53/26.02 [1 0 0] [2] 52.53/26.02 [from](x1) = [1 1 2] x1 + [4] 52.53/26.02 [1 0 0] [6] 52.53/26.02 52.53/26.02 [0 0 0] [1 0 0] [0] 52.53/26.02 [cons](x1, x2) = [0 1 1] x1 + [0 1 0] x2 + [0] 52.53/26.02 [1 0 0] [0 0 1] [0] 52.53/26.02 52.53/26.02 [1 0 0] [1] 52.53/26.02 [n__from](x1) = [1 1 2] x1 + [1] 52.53/26.02 [0 0 0] [6] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [n__s](x1) = [0 0 0] x1 + [1] 52.53/26.02 [0 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 2] [0] 52.53/26.02 [head](x1) = [0 1 0] x1 + [0] 52.53/26.02 [0 1 0] [2] 52.53/26.02 52.53/26.02 [6 0 2] [7] 52.53/26.02 [2nd](x1) = [0 6 4] x1 + [7] 52.53/26.02 [0 6 0] [7] 52.53/26.02 52.53/26.02 [2 0 0] [1] 52.53/26.02 [activate](x1) = [0 6 0] x1 + [2] 52.53/26.02 [2 0 1] [0] 52.53/26.02 52.53/26.02 [1 0 0] [1 0 0] [6] 52.53/26.02 [take](x1, x2) = [1 1 0] x1 + [0 1 0] x2 + [2] 52.53/26.02 [0 0 0] [0 0 1] [4] 52.53/26.02 52.53/26.02 [0] 52.53/26.02 [0] = [0] 52.53/26.02 [0] 52.53/26.02 52.53/26.02 [4] 52.53/26.02 [nil] = [1] 52.53/26.02 [4] 52.53/26.02 52.53/26.02 [1 0 0] [0] 52.53/26.02 [s](x1) = [0 0 0] x1 + [1] 52.53/26.02 [0 0 0] [0] 52.53/26.02 52.53/26.02 [1 0 0] [1 0 0] [4] 52.53/26.02 [n__take](x1, x2) = [1 1 0] x1 + [0 1 0] x2 + [2] 52.53/26.02 [0 0 0] [0 0 1] [0] 52.53/26.02 52.53/26.02 [7 0 4] [0 0 2] [7] 52.53/26.02 [sel](x1, x2) = [7 7 7] x1 + [0 1 0] x2 + [7] 52.53/26.02 [7 7 7] [0 1 0] [7] 52.53/26.02 52.53/26.02 The order satisfies the following ordering constraints: 52.53/26.02 52.53/26.02 [from(X)] = [1 0 0] [2] 52.53/26.02 [1 1 2] X + [4] 52.53/26.02 [1 0 0] [6] 52.53/26.02 > [1 0 0] [1] 52.53/26.02 [1 1 1] X + [2] 52.53/26.02 [1 0 0] [6] 52.53/26.02 = [cons(X, n__from(n__s(X)))] 52.53/26.02 52.53/26.02 [from(X)] = [1 0 0] [2] 52.53/26.02 [1 1 2] X + [4] 52.53/26.02 [1 0 0] [6] 52.53/26.02 > [1 0 0] [1] 52.53/26.02 [1 1 2] X + [1] 52.53/26.02 [0 0 0] [6] 52.53/26.02 = [n__from(X)] 52.53/26.02 52.53/26.02 [head(cons(X, XS))] = [2 0 0] [1 0 2] [0] 52.53/26.02 [0 1 1] X + [0 1 0] XS + [0] 52.53/26.02 [0 1 1] [0 1 0] [2] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 [2nd(cons(X, XS))] = [2 0 0] [6 0 2] [7] 52.53/26.02 [4 6 6] X + [0 6 4] XS + [7] 52.53/26.02 [0 6 6] [0 6 0] [7] 52.53/26.02 > [6 0 2] [1] 52.53/26.02 [0 6 0] XS + [2] 52.53/26.02 [0 6 0] [4] 52.53/26.02 = [head(activate(XS))] 52.53/26.02 52.53/26.02 [activate(X)] = [2 0 0] [1] 52.53/26.02 [0 6 0] X + [2] 52.53/26.02 [2 0 1] [0] 52.53/26.02 > [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 [activate(n__from(X))] = [2 0 0] [3] 52.53/26.02 [6 6 12] X + [8] 52.53/26.02 [2 0 0] [8] 52.53/26.02 >= [2 0 0] [3] 52.53/26.02 [6 6 2] X + [7] 52.53/26.02 [2 0 0] [7] 52.53/26.02 = [from(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__s(X))] = [2 0 0] [1] 52.53/26.02 [0 0 0] X + [8] 52.53/26.02 [2 0 0] [0] 52.53/26.02 >= [2 0 0] [1] 52.53/26.02 [0 0 0] X + [1] 52.53/26.02 [0 0 0] [0] 52.53/26.02 = [s(activate(X))] 52.53/26.02 52.53/26.02 [activate(n__take(X1, X2))] = [2 0 0] [2 0 0] [9] 52.53/26.02 [6 6 0] X1 + [0 6 0] X2 + [14] 52.53/26.02 [2 0 0] [2 0 1] [8] 52.53/26.02 > [2 0 0] [2 0 0] [8] 52.53/26.02 [2 6 0] X1 + [0 6 0] X2 + [7] 52.53/26.02 [0 0 0] [2 0 1] [4] 52.53/26.02 = [take(activate(X1), activate(X2))] 52.53/26.02 52.53/26.02 [take(X1, X2)] = [1 0 0] [1 0 0] [6] 52.53/26.02 [1 1 0] X1 + [0 1 0] X2 + [2] 52.53/26.02 [0 0 0] [0 0 1] [4] 52.53/26.02 > [1 0 0] [1 0 0] [4] 52.53/26.02 [1 1 0] X1 + [0 1 0] X2 + [2] 52.53/26.02 [0 0 0] [0 0 1] [0] 52.53/26.02 = [n__take(X1, X2)] 52.53/26.02 52.53/26.02 [take(0(), XS)] = [1 0 0] [6] 52.53/26.02 [0 1 0] XS + [2] 52.53/26.02 [0 0 1] [4] 52.53/26.02 > [4] 52.53/26.02 [1] 52.53/26.02 [4] 52.53/26.02 = [nil()] 52.53/26.02 52.53/26.02 [s(X)] = [1 0 0] [0] 52.53/26.02 [0 0 0] X + [1] 52.53/26.02 [0 0 0] [0] 52.53/26.02 >= [1 0 0] [0] 52.53/26.02 [0 0 0] X + [1] 52.53/26.02 [0 0 0] [0] 52.53/26.02 = [n__s(X)] 52.53/26.02 52.53/26.02 [sel(0(), cons(X, XS))] = [2 0 0] [0 0 2] [7] 52.53/26.02 [0 1 1] X + [0 1 0] XS + [7] 52.53/26.02 [0 1 1] [0 1 0] [7] 52.53/26.02 > [1 0 0] [0] 52.53/26.02 [0 1 0] X + [0] 52.53/26.02 [0 0 1] [0] 52.53/26.02 = [X] 52.53/26.02 52.53/26.02 52.53/26.02 We return to the main proof. 52.53/26.02 52.53/26.02 We are left with following problem, upon which TcT provides the 52.53/26.02 certificate YES(O(1),O(1)). 52.53/26.02 52.53/26.02 Weak Trs: 52.53/26.02 { from(X) -> cons(X, n__from(n__s(X))) 52.53/26.02 , from(X) -> n__from(X) 52.53/26.02 , head(cons(X, XS)) -> X 52.53/26.02 , 2nd(cons(X, XS)) -> head(activate(XS)) 52.53/26.02 , activate(X) -> X 52.53/26.02 , activate(n__from(X)) -> from(activate(X)) 52.53/26.02 , activate(n__s(X)) -> s(activate(X)) 52.53/26.02 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 52.53/26.02 , take(X1, X2) -> n__take(X1, X2) 52.53/26.02 , take(0(), XS) -> nil() 52.53/26.02 , s(X) -> n__s(X) 52.53/26.02 , sel(0(), cons(X, XS)) -> X } 52.53/26.02 Obligation: 52.53/26.02 innermost runtime complexity 52.53/26.02 Answer: 52.53/26.02 YES(O(1),O(1)) 52.53/26.02 52.53/26.02 Empty rules are trivially bounded 52.53/26.02 52.53/26.02 Hurray, we answered YES(O(1),O(n^1)) 52.53/26.04 EOF