YES(O(1),O(n^1)) 207.88/68.75 YES(O(1),O(n^1)) 207.88/68.75 207.88/68.75 We are left with following problem, upon which TcT provides the 207.88/68.75 certificate YES(O(1),O(n^1)). 207.88/68.75 207.88/68.75 Strict Trs: 207.88/68.75 { U11(tt(), N, X, XS) -> 207.88/68.75 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.75 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.75 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.75 , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) 207.88/68.75 , activate(X) -> X 207.88/68.75 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.75 , activate(n__s(X)) -> s(activate(X)) 207.88/68.75 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.75 , snd(pair(X, Y)) -> Y 207.88/68.75 , and(tt(), X) -> activate(X) 207.88/68.75 , fst(pair(X, Y)) -> X 207.88/68.75 , head(cons(N, XS)) -> N 207.88/68.75 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.75 , natsFrom(X) -> n__natsFrom(X) 207.88/68.75 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.75 , s(X) -> n__s(X) 207.88/68.75 , tail(cons(N, XS)) -> activate(XS) 207.88/68.75 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.75 Obligation: 207.88/68.75 innermost runtime complexity 207.88/68.75 Answer: 207.88/68.75 YES(O(1),O(n^1)) 207.88/68.75 207.88/68.75 Arguments of following rules are not normal-forms: 207.88/68.75 207.88/68.75 { splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) } 207.88/68.75 207.88/68.75 All above mentioned rules can be savely removed. 207.88/68.75 207.88/68.75 We are left with following problem, upon which TcT provides the 207.88/68.75 certificate YES(O(1),O(n^1)). 207.88/68.75 207.88/68.75 Strict Trs: 207.88/68.75 { U11(tt(), N, X, XS) -> 207.88/68.75 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.75 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.75 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.75 , activate(X) -> X 207.88/68.75 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.75 , activate(n__s(X)) -> s(activate(X)) 207.88/68.75 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.75 , snd(pair(X, Y)) -> Y 207.88/68.75 , and(tt(), X) -> activate(X) 207.88/68.75 , fst(pair(X, Y)) -> X 207.88/68.75 , head(cons(N, XS)) -> N 207.88/68.75 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.75 , natsFrom(X) -> n__natsFrom(X) 207.88/68.75 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.75 , s(X) -> n__s(X) 207.88/68.75 , tail(cons(N, XS)) -> activate(XS) 207.88/68.75 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.75 Obligation: 207.88/68.75 innermost runtime complexity 207.88/68.75 Answer: 207.88/68.75 YES(O(1),O(n^1)) 207.88/68.75 207.88/68.75 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.75 orient following rules strictly. 207.88/68.75 207.88/68.75 Trs: 207.88/68.75 { U11(tt(), N, X, XS) -> 207.88/68.75 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.75 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.75 , snd(pair(X, Y)) -> Y 207.88/68.75 , and(tt(), X) -> activate(X) 207.88/68.75 , fst(pair(X, Y)) -> X 207.88/68.75 , head(cons(N, XS)) -> N 207.88/68.75 , tail(cons(N, XS)) -> activate(XS) } 207.88/68.75 207.88/68.75 The induced complexity on above rules (modulo remaining rules) is 207.88/68.75 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.75 component(s). 207.88/68.75 207.88/68.75 Sub-proof: 207.88/68.75 ---------- 207.88/68.75 The following argument positions are usable: 207.88/68.75 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.75 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.75 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.75 207.88/68.75 TcT has computed the following constructor-based matrix 207.88/68.75 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.75 207.88/68.75 [7 0 4] [7 0 7] [7 0 7] [7 0 207.88/68.75 7] [7] 207.88/68.75 [U11](x1, x2, x3, x4) = [7 7 7] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.75 7] x4 + [7] 207.88/68.75 [7 7 7] [7 7 7] [7 7 7] [7 7 207.88/68.75 7] [7] 207.88/68.75 207.88/68.75 [0] 207.88/68.75 [tt] = [0] 207.88/68.75 [0] 207.88/68.75 207.88/68.75 [2 0 0] [1 0 0] [0] 207.88/68.75 [U12](x1, x2) = [2 1 0] x1 + [1 2 2] x2 + [0] 207.88/68.75 [0 0 1] [4 0 0] [4] 207.88/68.75 207.88/68.75 [1 0 0] [2 0 0] [0] 207.88/68.75 [splitAt](x1, x2) = [0 0 0] x1 + [0 1 1] x2 + [0] 207.88/68.75 [0 0 0] [1 0 0] [0] 207.88/68.75 207.88/68.75 [1 0 0] [0] 207.88/68.75 [activate](x1) = [0 2 0] x1 + [0] 207.88/68.75 [1 0 2] [0] 207.88/68.75 207.88/68.75 [1 0 1] [0 0 0] [4] 207.88/68.75 [pair](x1, x2) = [0 1 0] x1 + [0 1 1] x2 + [0] 207.88/68.75 [0 0 0] [1 0 0] [0] 207.88/68.75 207.88/68.75 [1 0 0] [0 0 0] [0] 207.88/68.75 [cons](x1, x2) = [0 1 1] x1 + [0 1 2] x2 + [0] 207.88/68.75 [0 0 0] [1 0 0] [0] 207.88/68.75 207.88/68.75 [2 0 0] [5 0 0] [0] 207.88/68.75 [afterNth](x1, x2) = [0 0 0] x1 + [0 4 4] x2 + [0] 207.88/68.75 [4 0 4] [4 4 1] [0] 207.88/68.75 207.88/68.75 [2 0 1] [0] 207.88/68.75 [snd](x1) = [0 4 0] x1 + [0] 207.88/68.75 [0 1 0] [0] 207.88/68.75 207.88/68.75 [7 0 4] [7 0 7] [7] 207.88/68.75 [and](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.75 [7 7 7] [7 7 7] [7] 207.88/68.75 207.88/68.75 [2 0 0] [7] 207.88/68.75 [fst](x1) = [0 1 0] x1 + [7] 207.88/68.75 [1 0 0] [7] 207.88/68.75 207.88/68.75 [1 0 0] [7] 207.88/68.75 [head](x1) = [0 1 0] x1 + [7] 207.88/68.75 [0 1 0] [7] 207.88/68.75 207.88/68.75 [1 0 0] [0] 207.88/68.75 [natsFrom](x1) = [1 1 1] x1 + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 207.88/68.75 [1 0 0] [0] 207.88/68.75 [n__natsFrom](x1) = [1 1 1] x1 + [0] 207.88/68.75 [0 0 0] [0] 207.88/68.75 207.88/68.75 [1 0 0] [0] 207.88/68.75 [n__s](x1) = [0 0 0] x1 + [0] 207.88/68.75 [0 0 0] [0] 207.88/68.75 207.88/68.75 [7 0 7] [7 0 7] [7] 207.88/68.75 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.75 [7 7 7] [7 7 7] [7] 207.88/68.75 207.88/68.75 [4] 207.88/68.75 [0] = [0] 207.88/68.75 [0] 207.88/68.75 207.88/68.75 [0] 207.88/68.75 [nil] = [0] 207.88/68.75 [0] 207.88/68.75 207.88/68.75 [1 0 0] [0] 207.88/68.75 [s](x1) = [0 0 0] x1 + [0] 207.88/68.75 [0 0 0] [0] 207.88/68.75 207.88/68.75 [0 0 1] [7] 207.88/68.75 [tail](x1) = [0 4 0] x1 + [7] 207.88/68.75 [0 4 1] [7] 207.88/68.75 207.88/68.75 [7 0 7] [7 0 7] [7] 207.88/68.75 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.75 [7 7 7] [7 7 7] [7] 207.88/68.75 207.88/68.75 The order satisfies the following ordering constraints: 207.88/68.75 207.88/68.75 [U11(tt(), N, X, XS)] = [7 0 7] [7 0 7] [7 0 7] [7] 207.88/68.75 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [7] 207.88/68.75 [7 7 7] [7 7 7] [7 7 7] [7] 207.88/68.75 > [2 0 0] [1 0 0] [4 0 0] [0] 207.88/68.75 [2 0 0] N + [3 4 4] X + [5 2 2] XS + [0] 207.88/68.75 [0 0 0] [4 0 0] [1 0 0] [4] 207.88/68.75 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.75 207.88/68.75 [U12(pair(YS, ZS), X)] = [1 0 0] [2 0 2] [0 0 0] [8] 207.88/68.75 [1 2 2] X + [2 1 2] YS + [0 1 1] ZS + [8] 207.88/68.75 [4 0 0] [0 0 0] [1 0 0] [4] 207.88/68.75 > [1 0 0] [1 0 0] [0 0 0] [4] 207.88/68.75 [1 2 2] X + [0 1 2] YS + [0 1 1] ZS + [0] 207.88/68.75 [0 0 0] [0 0 0] [1 0 0] [0] 207.88/68.75 = [pair(cons(activate(X), YS), ZS)] 207.88/68.75 207.88/68.75 [splitAt(0(), XS)] = [2 0 0] [4] 207.88/68.75 [0 1 1] XS + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 >= [0 0 0] [4] 207.88/68.75 [0 1 1] XS + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 = [pair(nil(), XS)] 207.88/68.75 207.88/68.75 [activate(X)] = [1 0 0] [0] 207.88/68.75 [0 2 0] X + [0] 207.88/68.75 [1 0 2] [0] 207.88/68.75 >= [1 0 0] [0] 207.88/68.75 [0 1 0] X + [0] 207.88/68.75 [0 0 1] [0] 207.88/68.75 = [X] 207.88/68.75 207.88/68.75 [activate(n__natsFrom(X))] = [1 0 0] [0] 207.88/68.75 [2 2 2] X + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 >= [1 0 0] [0] 207.88/68.75 [2 2 2] X + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 = [natsFrom(activate(X))] 207.88/68.75 207.88/68.75 [activate(n__s(X))] = [1 0 0] [0] 207.88/68.75 [0 0 0] X + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 >= [1 0 0] [0] 207.88/68.75 [0 0 0] X + [0] 207.88/68.75 [0 0 0] [0] 207.88/68.75 = [s(activate(X))] 207.88/68.75 207.88/68.75 [afterNth(N, XS)] = [2 0 0] [5 0 0] [0] 207.88/68.75 [0 0 0] N + [0 4 4] XS + [0] 207.88/68.75 [4 0 4] [4 4 1] [0] 207.88/68.75 >= [2 0 0] [5 0 0] [0] 207.88/68.75 [0 0 0] N + [0 4 4] XS + [0] 207.88/68.75 [0 0 0] [0 1 1] [0] 207.88/68.75 = [snd(splitAt(N, XS))] 207.88/68.75 207.88/68.75 [snd(pair(X, Y))] = [2 0 2] [1 0 0] [8] 207.88/68.75 [0 4 0] X + [0 4 4] Y + [0] 207.88/68.75 [0 1 0] [0 1 1] [0] 207.88/68.75 > [1 0 0] [0] 207.88/68.75 [0 1 0] Y + [0] 207.88/68.75 [0 0 1] [0] 207.88/68.75 = [Y] 207.88/68.75 207.88/68.75 [and(tt(), X)] = [7 0 7] [7] 207.88/68.75 [7 7 7] X + [7] 207.88/68.75 [7 7 7] [7] 207.88/68.75 > [1 0 0] [0] 207.88/68.75 [0 2 0] X + [0] 207.88/68.75 [1 0 2] [0] 207.88/68.75 = [activate(X)] 207.88/68.75 207.88/68.75 [fst(pair(X, Y))] = [2 0 2] [0 0 0] [15] 207.88/68.75 [0 1 0] X + [0 1 1] Y + [7] 207.88/68.75 [1 0 1] [0 0 0] [11] 207.88/68.75 > [1 0 0] [0] 207.88/68.75 [0 1 0] X + [0] 207.88/68.75 [0 0 1] [0] 207.88/68.75 = [X] 207.88/68.75 207.88/68.75 [head(cons(N, XS))] = [1 0 0] [0 0 0] [7] 207.88/68.75 [0 1 1] N + [0 1 2] XS + [7] 207.88/68.75 [0 1 1] [0 1 2] [7] 207.88/68.75 > [1 0 0] [0] 207.88/68.75 [0 1 0] N + [0] 207.88/68.75 [0 0 1] [0] 207.88/68.75 = [N] 207.88/68.75 207.88/68.75 [natsFrom(N)] = [1 0 0] [0] 207.88/68.75 [1 1 1] N + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 >= [1 0 0] [0] 207.88/68.75 [1 1 1] N + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.75 207.88/68.75 [natsFrom(X)] = [1 0 0] [0] 207.88/68.75 [1 1 1] X + [0] 207.88/68.75 [1 0 0] [0] 207.88/68.75 >= [1 0 0] [0] 207.88/68.75 [1 1 1] X + [0] 207.88/68.75 [0 0 0] [0] 207.88/68.75 = [n__natsFrom(X)] 207.88/68.75 207.88/68.75 [sel(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.75 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.75 [7 7 7] [7 7 7] [7] 207.88/68.75 >= [2 0 0] [5 0 0] [7] 207.88/68.75 [0 0 0] N + [0 4 4] XS + [7] 207.88/68.75 [0 0 0] [0 4 4] [7] 207.88/68.75 = [head(afterNth(N, XS))] 207.88/68.75 207.88/68.75 [s(X)] = [1 0 0] [0] 207.88/68.75 [0 0 0] X + [0] 207.88/68.75 [0 0 0] [0] 207.88/68.75 >= [1 0 0] [0] 207.88/68.75 [0 0 0] X + [0] 207.88/68.75 [0 0 0] [0] 207.88/68.75 = [n__s(X)] 207.88/68.75 207.88/68.75 [tail(cons(N, XS))] = [0 0 0] [1 0 0] [7] 207.88/68.75 [0 4 4] N + [0 4 8] XS + [7] 207.88/68.75 [0 4 4] [1 4 8] [7] 207.88/68.75 > [1 0 0] [0] 207.88/68.75 [0 2 0] XS + [0] 207.88/68.75 [1 0 2] [0] 207.88/68.75 = [activate(XS)] 207.88/68.75 207.88/68.75 [take(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.75 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.75 [7 7 7] [7 7 7] [7] 207.88/68.75 >= [2 0 0] [4 0 0] [7] 207.88/68.75 [0 0 0] N + [0 1 1] XS + [7] 207.88/68.75 [1 0 0] [2 0 0] [7] 207.88/68.75 = [fst(splitAt(N, XS))] 207.88/68.75 207.88/68.75 207.88/68.75 We return to the main proof. 207.88/68.75 207.88/68.75 We are left with following problem, upon which TcT provides the 207.88/68.75 certificate YES(O(1),O(n^1)). 207.88/68.75 207.88/68.75 Strict Trs: 207.88/68.75 { splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.75 , activate(X) -> X 207.88/68.75 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.75 , activate(n__s(X)) -> s(activate(X)) 207.88/68.75 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.75 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.75 , natsFrom(X) -> n__natsFrom(X) 207.88/68.75 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.75 , s(X) -> n__s(X) 207.88/68.75 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.75 Weak Trs: 207.88/68.75 { U11(tt(), N, X, XS) -> 207.88/68.75 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.75 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.75 , snd(pair(X, Y)) -> Y 207.88/68.75 , and(tt(), X) -> activate(X) 207.88/68.75 , fst(pair(X, Y)) -> X 207.88/68.75 , head(cons(N, XS)) -> N 207.88/68.75 , tail(cons(N, XS)) -> activate(XS) } 207.88/68.75 Obligation: 207.88/68.75 innermost runtime complexity 207.88/68.75 Answer: 207.88/68.75 YES(O(1),O(n^1)) 207.88/68.75 207.88/68.75 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.75 orient following rules strictly. 207.88/68.75 207.88/68.75 Trs: 207.88/68.75 { afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.75 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) } 207.88/68.75 207.88/68.75 The induced complexity on above rules (modulo remaining rules) is 207.88/68.75 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.75 component(s). 207.88/68.75 207.88/68.75 Sub-proof: 207.88/68.75 ---------- 207.88/68.75 The following argument positions are usable: 207.88/68.75 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.75 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.75 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.75 207.88/68.75 TcT has computed the following constructor-based matrix 207.88/68.75 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.75 207.88/68.75 [7 4 0] [7 7 0] [7 7 0] [7 7 207.88/68.75 0] [7] 207.88/68.75 [U11](x1, x2, x3, x4) = [7 7 7] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.75 7] x4 + [7] 207.88/68.75 [7 7 7] [7 7 7] [7 7 7] [7 7 207.88/68.75 7] [7] 207.88/68.75 207.88/68.75 [0] 207.88/68.75 [tt] = [0] 207.88/68.75 [0] 207.88/68.76 207.88/68.76 [2 0 0] [4 0 0] [0] 207.88/68.76 [U12](x1, x2) = [2 1 0] x1 + [0 2 2] x2 + [0] 207.88/68.76 [0 0 2] [0 0 1] [0] 207.88/68.76 207.88/68.76 [2 0 0] [2 0 0] [0] 207.88/68.76 [splitAt](x1, x2) = [0 0 0] x1 + [0 1 0] x2 + [0] 207.88/68.76 [0 0 2] [1 0 2] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [activate](x1) = [0 2 2] x1 + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 207.88/68.76 [1 0 0] [1 0 0] [0] 207.88/68.76 [pair](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 207.88/68.76 [0 0 1] [1 0 1] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0 0 0] [0] 207.88/68.76 [cons](x1, x2) = [0 1 0] x1 + [1 1 0] x2 + [0] 207.88/68.76 [0 0 1] [0 0 1] [0] 207.88/68.76 207.88/68.76 [2 0 0] [4 0 0] [4] 207.88/68.76 [afterNth](x1, x2) = [0 0 0] x1 + [0 2 0] x2 + [0] 207.88/68.76 [0 4 4] [2 0 4] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [snd](x1) = [0 1 0] x1 + [0] 207.88/68.76 [0 0 2] [0] 207.88/68.76 207.88/68.76 [7 4 0] [7 7 0] [7] 207.88/68.76 [and](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 [2 0 0] [7] 207.88/68.76 [fst](x1) = [0 4 0] x1 + [7] 207.88/68.76 [0 0 1] [7] 207.88/68.76 207.88/68.76 [1 0 0] [3] 207.88/68.76 [head](x1) = [0 2 0] x1 + [7] 207.88/68.76 [0 0 1] [7] 207.88/68.76 207.88/68.76 [1 0 0] [4] 207.88/68.76 [natsFrom](x1) = [2 1 0] x1 + [4] 207.88/68.76 [1 0 1] [2] 207.88/68.76 207.88/68.76 [1 0 0] [4] 207.88/68.76 [n__natsFrom](x1) = [0 1 0] x1 + [0] 207.88/68.76 [1 0 1] [2] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [n__s](x1) = [1 0 0] x1 + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 207.88/68.76 [7 7 0] [7 7 0] [7] 207.88/68.76 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 [0] 207.88/68.76 [0] = [0] 207.88/68.76 [4] 207.88/68.76 207.88/68.76 [0] 207.88/68.76 [nil] = [0] 207.88/68.76 [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [s](x1) = [1 0 0] x1 + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 207.88/68.76 [0 4 0] [7] 207.88/68.76 [tail](x1) = [0 4 2] x1 + [7] 207.88/68.76 [0 0 1] [7] 207.88/68.76 207.88/68.76 [7 7 0] [7 7 0] [7] 207.88/68.76 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 The order satisfies the following ordering constraints: 207.88/68.76 207.88/68.76 [U11(tt(), N, X, XS)] = [7 7 0] [7 7 0] [7 7 0] [7] 207.88/68.76 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [7] 207.88/68.76 [7 7 7] [7 7 7] [7 7 7] [7] 207.88/68.76 > [4 0 0] [4 0 0] [4 0 0] [0] 207.88/68.76 [4 0 0] N + [0 4 6] X + [4 2 2] XS + [0] 207.88/68.76 [0 0 4] [0 0 1] [2 0 4] [0] 207.88/68.76 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.76 207.88/68.76 [U12(pair(YS, ZS), X)] = [4 0 0] [2 0 0] [2 0 0] [0] 207.88/68.76 [0 2 2] X + [2 1 0] YS + [2 1 0] ZS + [0] 207.88/68.76 [0 0 1] [0 0 2] [2 0 2] [0] 207.88/68.76 >= [1 0 0] [0 0 0] [1 0 0] [0] 207.88/68.76 [0 2 2] X + [1 1 0] YS + [0 1 0] ZS + [0] 207.88/68.76 [0 0 1] [0 0 1] [1 0 1] [0] 207.88/68.76 = [pair(cons(activate(X), YS), ZS)] 207.88/68.76 207.88/68.76 [splitAt(0(), XS)] = [2 0 0] [0] 207.88/68.76 [0 1 0] XS + [0] 207.88/68.76 [1 0 2] [8] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 1 0] XS + [0] 207.88/68.76 [1 0 1] [0] 207.88/68.76 = [pair(nil(), XS)] 207.88/68.76 207.88/68.76 [activate(X)] = [1 0 0] [0] 207.88/68.76 [0 2 2] X + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 1 0] X + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [X] 207.88/68.76 207.88/68.76 [activate(n__natsFrom(X))] = [1 0 0] [4] 207.88/68.76 [2 2 2] X + [4] 207.88/68.76 [1 0 1] [2] 207.88/68.76 >= [1 0 0] [4] 207.88/68.76 [2 2 2] X + [4] 207.88/68.76 [1 0 1] [2] 207.88/68.76 = [natsFrom(activate(X))] 207.88/68.76 207.88/68.76 [activate(n__s(X))] = [1 0 0] [0] 207.88/68.76 [2 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [1 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 = [s(activate(X))] 207.88/68.76 207.88/68.76 [afterNth(N, XS)] = [2 0 0] [4 0 0] [4] 207.88/68.76 [0 0 0] N + [0 2 0] XS + [0] 207.88/68.76 [0 4 4] [2 0 4] [0] 207.88/68.76 > [2 0 0] [2 0 0] [0] 207.88/68.76 [0 0 0] N + [0 1 0] XS + [0] 207.88/68.76 [0 0 4] [2 0 4] [0] 207.88/68.76 = [snd(splitAt(N, XS))] 207.88/68.76 207.88/68.76 [snd(pair(X, Y))] = [1 0 0] [1 0 0] [0] 207.88/68.76 [0 1 0] X + [0 1 0] Y + [0] 207.88/68.76 [0 0 2] [2 0 2] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 1 0] Y + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [Y] 207.88/68.76 207.88/68.76 [and(tt(), X)] = [7 7 0] [7] 207.88/68.76 [7 7 7] X + [7] 207.88/68.76 [7 7 7] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 2 2] X + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [activate(X)] 207.88/68.76 207.88/68.76 [fst(pair(X, Y))] = [2 0 0] [2 0 0] [7] 207.88/68.76 [0 4 0] X + [0 4 0] Y + [7] 207.88/68.76 [0 0 1] [1 0 1] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 1 0] X + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [X] 207.88/68.76 207.88/68.76 [head(cons(N, XS))] = [1 0 0] [0 0 0] [3] 207.88/68.76 [0 2 0] N + [2 2 0] XS + [7] 207.88/68.76 [0 0 1] [0 0 1] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 1 0] N + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [N] 207.88/68.76 207.88/68.76 [natsFrom(N)] = [1 0 0] [4] 207.88/68.76 [2 1 0] N + [4] 207.88/68.76 [1 0 1] [2] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [2 1 0] N + [4] 207.88/68.76 [1 0 1] [2] 207.88/68.76 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.76 207.88/68.76 [natsFrom(X)] = [1 0 0] [4] 207.88/68.76 [2 1 0] X + [4] 207.88/68.76 [1 0 1] [2] 207.88/68.76 >= [1 0 0] [4] 207.88/68.76 [0 1 0] X + [0] 207.88/68.76 [1 0 1] [2] 207.88/68.76 = [n__natsFrom(X)] 207.88/68.76 207.88/68.76 [sel(N, XS)] = [7 7 0] [7 7 0] [7] 207.88/68.76 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 >= [2 0 0] [4 0 0] [7] 207.88/68.76 [0 0 0] N + [0 4 0] XS + [7] 207.88/68.76 [0 4 4] [2 0 4] [7] 207.88/68.76 = [head(afterNth(N, XS))] 207.88/68.76 207.88/68.76 [s(X)] = [1 0 0] [0] 207.88/68.76 [1 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [1 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 = [n__s(X)] 207.88/68.76 207.88/68.76 [tail(cons(N, XS))] = [0 4 0] [4 4 0] [7] 207.88/68.76 [0 4 2] N + [4 4 2] XS + [7] 207.88/68.76 [0 0 1] [0 0 1] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 2 2] XS + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [activate(XS)] 207.88/68.76 207.88/68.76 [take(N, XS)] = [7 7 0] [7 7 0] [7] 207.88/68.76 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 >= [4 0 0] [4 0 0] [7] 207.88/68.76 [0 0 0] N + [0 4 0] XS + [7] 207.88/68.76 [0 0 2] [1 0 2] [7] 207.88/68.76 = [fst(splitAt(N, XS))] 207.88/68.76 207.88/68.76 207.88/68.76 We return to the main proof. 207.88/68.76 207.88/68.76 We are left with following problem, upon which TcT provides the 207.88/68.76 certificate YES(O(1),O(n^1)). 207.88/68.76 207.88/68.76 Strict Trs: 207.88/68.76 { splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.76 , activate(X) -> X 207.88/68.76 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.76 , activate(n__s(X)) -> s(activate(X)) 207.88/68.76 , natsFrom(X) -> n__natsFrom(X) 207.88/68.76 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.76 , s(X) -> n__s(X) 207.88/68.76 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.76 Weak Trs: 207.88/68.76 { U11(tt(), N, X, XS) -> 207.88/68.76 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.76 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.76 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.76 , snd(pair(X, Y)) -> Y 207.88/68.76 , and(tt(), X) -> activate(X) 207.88/68.76 , fst(pair(X, Y)) -> X 207.88/68.76 , head(cons(N, XS)) -> N 207.88/68.76 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.76 , tail(cons(N, XS)) -> activate(XS) } 207.88/68.76 Obligation: 207.88/68.76 innermost runtime complexity 207.88/68.76 Answer: 207.88/68.76 YES(O(1),O(n^1)) 207.88/68.76 207.88/68.76 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.76 orient following rules strictly. 207.88/68.76 207.88/68.76 Trs: { splitAt(0(), XS) -> pair(nil(), XS) } 207.88/68.76 207.88/68.76 The induced complexity on above rules (modulo remaining rules) is 207.88/68.76 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.76 component(s). 207.88/68.76 207.88/68.76 Sub-proof: 207.88/68.76 ---------- 207.88/68.76 The following argument positions are usable: 207.88/68.76 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.76 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.76 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.76 207.88/68.76 TcT has computed the following constructor-based matrix 207.88/68.76 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.76 207.88/68.76 [4 4 0] [7 7 0] [7 7 0] [7 7 207.88/68.76 0] [3] 207.88/68.76 [U11](x1, x2, x3, x4) = [4 7 7] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.76 7] x4 + [3] 207.88/68.76 [0 7 7] [7 7 7] [7 7 7] [7 7 207.88/68.76 7] [7] 207.88/68.76 207.88/68.76 [2] 207.88/68.76 [tt] = [0] 207.88/68.76 [0] 207.88/68.76 207.88/68.76 [2 0 0] [1 0 0] [0] 207.88/68.76 [U12](x1, x2) = [0 2 0] x1 + [4 0 0] x2 + [4] 207.88/68.76 [2 0 1] [1 2 2] [4] 207.88/68.76 207.88/68.76 [1 0 0] [2 0 0] [0] 207.88/68.76 [splitAt](x1, x2) = [0 0 0] x1 + [1 1 0] x2 + [0] 207.88/68.76 [0 0 0] [1 1 1] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [activate](x1) = [1 2 0] x1 + [0] 207.88/68.76 [0 0 2] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0 0 0] [0] 207.88/68.76 [pair](x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0] 207.88/68.76 [0 1 1] [0 1 1] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0 0 0] [0] 207.88/68.76 [cons](x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0] 207.88/68.76 [0 1 1] [0 1 1] [0] 207.88/68.76 207.88/68.76 [4 0 0] [6 4 0] [0] 207.88/68.76 [afterNth](x1, x2) = [4 4 0] x1 + [1 2 2] x2 + [0] 207.88/68.76 [0 0 0] [2 2 2] [0] 207.88/68.76 207.88/68.76 [1 4 0] [0] 207.88/68.76 [snd](x1) = [0 0 1] x1 + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 207.88/68.76 [0 4 0] [7 7 0] [7] 207.88/68.76 [and](x1, x2) = [0 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [0 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 [2 0 0] [7] 207.88/68.76 [fst](x1) = [0 0 4] x1 + [7] 207.88/68.76 [0 2 2] [7] 207.88/68.76 207.88/68.76 [1 0 0] [7] 207.88/68.76 [head](x1) = [0 0 2] x1 + [7] 207.88/68.76 [0 0 2] [7] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [natsFrom](x1) = [1 0 0] x1 + [0] 207.88/68.76 [1 1 1] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [n__natsFrom](x1) = [0 0 0] x1 + [0] 207.88/68.76 [1 1 1] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [n__s](x1) = [0 0 0] x1 + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 207.88/68.76 [7 7 0] [7 7 0] [7] 207.88/68.76 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 [1] 207.88/68.76 [0] = [0] 207.88/68.76 [0] 207.88/68.76 207.88/68.76 [0] 207.88/68.76 [nil] = [0] 207.88/68.76 [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [s](x1) = [0 0 0] x1 + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 207.88/68.76 [0 1 0] [7] 207.88/68.76 [tail](x1) = [0 1 4] x1 + [7] 207.88/68.76 [0 0 2] [7] 207.88/68.76 207.88/68.76 [7 7 0] [7 7 0] [7] 207.88/68.76 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 The order satisfies the following ordering constraints: 207.88/68.76 207.88/68.76 [U11(tt(), N, X, XS)] = [7 7 0] [7 7 0] [7 7 0] [11] 207.88/68.76 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [11] 207.88/68.76 [7 7 7] [7 7 7] [7 7 7] [7] 207.88/68.76 > [2 0 0] [1 0 0] [4 0 0] [0] 207.88/68.76 [0 0 0] N + [4 0 0] X + [4 4 0] XS + [4] 207.88/68.76 [2 0 0] [3 4 4] [6 2 2] [4] 207.88/68.76 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.76 207.88/68.76 [U12(pair(YS, ZS), X)] = [1 0 0] [2 0 0] [0 0 0] [0] 207.88/68.76 [4 0 0] X + [0 0 0] YS + [2 0 0] ZS + [4] 207.88/68.76 [1 2 2] [2 1 1] [0 1 1] [4] 207.88/68.76 >= [1 0 0] [0 0 0] [0 0 0] [0] 207.88/68.76 [0 0 0] X + [0 0 0] YS + [1 0 0] ZS + [0] 207.88/68.76 [1 2 2] [1 1 1] [0 1 1] [0] 207.88/68.76 = [pair(cons(activate(X), YS), ZS)] 207.88/68.76 207.88/68.76 [splitAt(0(), XS)] = [2 0 0] [1] 207.88/68.76 [1 1 0] XS + [0] 207.88/68.76 [1 1 1] [0] 207.88/68.76 > [0 0 0] [0] 207.88/68.76 [1 0 0] XS + [0] 207.88/68.76 [0 1 1] [0] 207.88/68.76 = [pair(nil(), XS)] 207.88/68.76 207.88/68.76 [activate(X)] = [1 0 0] [0] 207.88/68.76 [1 2 0] X + [0] 207.88/68.76 [0 0 2] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 1 0] X + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [X] 207.88/68.76 207.88/68.76 [activate(n__natsFrom(X))] = [1 0 0] [0] 207.88/68.76 [1 0 0] X + [0] 207.88/68.76 [2 2 2] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [1 0 0] X + [0] 207.88/68.76 [2 2 2] [0] 207.88/68.76 = [natsFrom(activate(X))] 207.88/68.76 207.88/68.76 [activate(n__s(X))] = [1 0 0] [0] 207.88/68.76 [1 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 = [s(activate(X))] 207.88/68.76 207.88/68.76 [afterNth(N, XS)] = [4 0 0] [6 4 0] [0] 207.88/68.76 [4 4 0] N + [1 2 2] XS + [0] 207.88/68.76 [0 0 0] [2 2 2] [0] 207.88/68.76 >= [1 0 0] [6 4 0] [0] 207.88/68.76 [0 0 0] N + [1 1 1] XS + [0] 207.88/68.76 [0 0 0] [1 1 1] [0] 207.88/68.76 = [snd(splitAt(N, XS))] 207.88/68.76 207.88/68.76 [snd(pair(X, Y))] = [1 0 0] [4 0 0] [0] 207.88/68.76 [0 1 1] X + [0 1 1] Y + [0] 207.88/68.76 [0 1 1] [0 1 1] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 1 0] Y + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [Y] 207.88/68.76 207.88/68.76 [and(tt(), X)] = [7 7 0] [7] 207.88/68.76 [7 7 7] X + [7] 207.88/68.76 [7 7 7] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [1 2 0] X + [0] 207.88/68.76 [0 0 2] [0] 207.88/68.76 = [activate(X)] 207.88/68.76 207.88/68.76 [fst(pair(X, Y))] = [2 0 0] [0 0 0] [7] 207.88/68.76 [0 4 4] X + [0 4 4] Y + [7] 207.88/68.76 [0 2 2] [2 2 2] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 1 0] X + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [X] 207.88/68.76 207.88/68.76 [head(cons(N, XS))] = [1 0 0] [0 0 0] [7] 207.88/68.76 [0 2 2] N + [0 2 2] XS + [7] 207.88/68.76 [0 2 2] [0 2 2] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 1 0] N + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [N] 207.88/68.76 207.88/68.76 [natsFrom(N)] = [1 0 0] [0] 207.88/68.76 [1 0 0] N + [0] 207.88/68.76 [1 1 1] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [1 0 0] N + [0] 207.88/68.76 [1 1 1] [0] 207.88/68.76 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.76 207.88/68.76 [natsFrom(X)] = [1 0 0] [0] 207.88/68.76 [1 0 0] X + [0] 207.88/68.76 [1 1 1] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 0 0] X + [0] 207.88/68.76 [1 1 1] [0] 207.88/68.76 = [n__natsFrom(X)] 207.88/68.76 207.88/68.76 [sel(N, XS)] = [7 7 0] [7 7 0] [7] 207.88/68.76 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 >= [4 0 0] [6 4 0] [7] 207.88/68.76 [0 0 0] N + [4 4 4] XS + [7] 207.88/68.76 [0 0 0] [4 4 4] [7] 207.88/68.76 = [head(afterNth(N, XS))] 207.88/68.76 207.88/68.76 [s(X)] = [1 0 0] [0] 207.88/68.76 [0 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 = [n__s(X)] 207.88/68.76 207.88/68.76 [tail(cons(N, XS))] = [0 0 0] [1 0 0] [7] 207.88/68.76 [0 4 4] N + [1 4 4] XS + [7] 207.88/68.76 [0 2 2] [0 2 2] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [1 2 0] XS + [0] 207.88/68.76 [0 0 2] [0] 207.88/68.76 = [activate(XS)] 207.88/68.76 207.88/68.76 [take(N, XS)] = [7 7 0] [7 7 0] [7] 207.88/68.76 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 >= [2 0 0] [4 0 0] [7] 207.88/68.76 [0 0 0] N + [4 4 4] XS + [7] 207.88/68.76 [0 0 0] [4 4 2] [7] 207.88/68.76 = [fst(splitAt(N, XS))] 207.88/68.76 207.88/68.76 207.88/68.76 We return to the main proof. 207.88/68.76 207.88/68.76 We are left with following problem, upon which TcT provides the 207.88/68.76 certificate YES(O(1),O(n^1)). 207.88/68.76 207.88/68.76 Strict Trs: 207.88/68.76 { activate(X) -> X 207.88/68.76 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.76 , activate(n__s(X)) -> s(activate(X)) 207.88/68.76 , natsFrom(X) -> n__natsFrom(X) 207.88/68.76 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.76 , s(X) -> n__s(X) 207.88/68.76 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.76 Weak Trs: 207.88/68.76 { U11(tt(), N, X, XS) -> 207.88/68.76 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.76 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.76 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.76 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.76 , snd(pair(X, Y)) -> Y 207.88/68.76 , and(tt(), X) -> activate(X) 207.88/68.76 , fst(pair(X, Y)) -> X 207.88/68.76 , head(cons(N, XS)) -> N 207.88/68.76 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.76 , tail(cons(N, XS)) -> activate(XS) } 207.88/68.76 Obligation: 207.88/68.76 innermost runtime complexity 207.88/68.76 Answer: 207.88/68.76 YES(O(1),O(n^1)) 207.88/68.76 207.88/68.76 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.76 orient following rules strictly. 207.88/68.76 207.88/68.76 Trs: { take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.76 207.88/68.76 The induced complexity on above rules (modulo remaining rules) is 207.88/68.76 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.76 component(s). 207.88/68.76 207.88/68.76 Sub-proof: 207.88/68.76 ---------- 207.88/68.76 The following argument positions are usable: 207.88/68.76 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.76 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.76 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.76 207.88/68.76 TcT has computed the following constructor-based matrix 207.88/68.76 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.76 207.88/68.76 [2 0 4] [7 0 7] [7 0 7] [7 0 207.88/68.76 7] [3] 207.88/68.76 [U11](x1, x2, x3, x4) = [0 7 7] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.76 7] x4 + [7] 207.88/68.76 [2 7 7] [7 7 7] [7 7 7] [7 7 207.88/68.76 7] [7] 207.88/68.76 207.88/68.76 [4] 207.88/68.76 [tt] = [0] 207.88/68.76 [0] 207.88/68.76 207.88/68.76 [1 0 0] [1 0 0] [4] 207.88/68.76 [U12](x1, x2) = [0 2 4] x1 + [1 2 2] x2 + [4] 207.88/68.76 [1 0 4] [0 0 0] [0] 207.88/68.76 207.88/68.76 [4 0 0] [2 0 1] [0] 207.88/68.76 [splitAt](x1, x2) = [0 0 0] x1 + [0 1 0] x2 + [0] 207.88/68.76 [0 0 0] [0 0 0] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [activate](x1) = [0 2 0] x1 + [0] 207.88/68.76 [1 0 2] [0] 207.88/68.76 207.88/68.76 [1 0 0] [1 0 1] [0] 207.88/68.76 [pair](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 207.88/68.76 [0 0 1] [0 0 0] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0 0 0] [0] 207.88/68.76 [cons](x1, x2) = [0 1 1] x1 + [0 1 4] x2 + [0] 207.88/68.76 [0 0 0] [1 0 0] [0] 207.88/68.76 207.88/68.76 [4 0 0] [2 0 2] [0] 207.88/68.76 [afterNth](x1, x2) = [0 0 0] x1 + [0 4 0] x2 + [0] 207.88/68.76 [4 0 0] [4 4 4] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [snd](x1) = [0 4 0] x1 + [0] 207.88/68.76 [1 0 0] [0] 207.88/68.76 207.88/68.76 [0 0 4] [7 0 7] [7] 207.88/68.76 [and](x1, x2) = [0 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [0 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 [1 0 0] [6] 207.88/68.76 [fst](x1) = [0 4 0] x1 + [7] 207.88/68.76 [0 0 4] [7] 207.88/68.76 207.88/68.76 [1 0 0] [7] 207.88/68.76 [head](x1) = [0 1 0] x1 + [7] 207.88/68.76 [0 1 0] [7] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [natsFrom](x1) = [1 1 1] x1 + [0] 207.88/68.76 [1 0 0] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [n__natsFrom](x1) = [1 1 1] x1 + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [n__s](x1) = [0 0 0] x1 + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 207.88/68.76 [7 0 7] [7 0 7] [7] 207.88/68.76 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 [2] 207.88/68.76 [0] = [0] 207.88/68.76 [0] 207.88/68.76 207.88/68.76 [0] 207.88/68.76 [nil] = [0] 207.88/68.76 [0] 207.88/68.76 207.88/68.76 [1 0 0] [0] 207.88/68.76 [s](x1) = [0 0 0] x1 + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 207.88/68.76 [0 0 4] [7] 207.88/68.76 [tail](x1) = [0 2 4] x1 + [7] 207.88/68.76 [0 2 4] [7] 207.88/68.76 207.88/68.76 [7 0 7] [7 0 7] [7] 207.88/68.76 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 207.88/68.76 The order satisfies the following ordering constraints: 207.88/68.76 207.88/68.76 [U11(tt(), N, X, XS)] = [7 0 7] [7 0 7] [7 0 7] [11] 207.88/68.76 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [7] 207.88/68.76 [7 7 7] [7 7 7] [7 7 7] [15] 207.88/68.76 > [4 0 0] [1 0 0] [3 0 2] [4] 207.88/68.76 [0 0 0] N + [3 4 4] X + [0 4 0] XS + [4] 207.88/68.76 [4 0 0] [0 0 0] [3 0 2] [0] 207.88/68.76 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.76 207.88/68.76 [U12(pair(YS, ZS), X)] = [1 0 0] [1 0 0] [1 0 1] [4] 207.88/68.76 [1 2 2] X + [0 2 4] YS + [0 2 0] ZS + [4] 207.88/68.76 [0 0 0] [1 0 4] [1 0 1] [0] 207.88/68.76 > [1 0 0] [0 0 0] [1 0 1] [0] 207.88/68.76 [1 2 2] X + [0 1 4] YS + [0 1 0] ZS + [0] 207.88/68.76 [0 0 0] [1 0 0] [0 0 0] [0] 207.88/68.76 = [pair(cons(activate(X), YS), ZS)] 207.88/68.76 207.88/68.76 [splitAt(0(), XS)] = [2 0 1] [8] 207.88/68.76 [0 1 0] XS + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 > [1 0 1] [0] 207.88/68.76 [0 1 0] XS + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 = [pair(nil(), XS)] 207.88/68.76 207.88/68.76 [activate(X)] = [1 0 0] [0] 207.88/68.76 [0 2 0] X + [0] 207.88/68.76 [1 0 2] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 1 0] X + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [X] 207.88/68.76 207.88/68.76 [activate(n__natsFrom(X))] = [1 0 0] [0] 207.88/68.76 [2 2 2] X + [0] 207.88/68.76 [1 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [2 2 2] X + [0] 207.88/68.76 [1 0 0] [0] 207.88/68.76 = [natsFrom(activate(X))] 207.88/68.76 207.88/68.76 [activate(n__s(X))] = [1 0 0] [0] 207.88/68.76 [0 0 0] X + [0] 207.88/68.76 [1 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 = [s(activate(X))] 207.88/68.76 207.88/68.76 [afterNth(N, XS)] = [4 0 0] [2 0 2] [0] 207.88/68.76 [0 0 0] N + [0 4 0] XS + [0] 207.88/68.76 [4 0 0] [4 4 4] [0] 207.88/68.76 >= [4 0 0] [2 0 1] [0] 207.88/68.76 [0 0 0] N + [0 4 0] XS + [0] 207.88/68.76 [4 0 0] [2 0 1] [0] 207.88/68.76 = [snd(splitAt(N, XS))] 207.88/68.76 207.88/68.76 [snd(pair(X, Y))] = [1 0 0] [1 0 1] [0] 207.88/68.76 [0 4 0] X + [0 4 0] Y + [0] 207.88/68.76 [1 0 0] [1 0 1] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [0 1 0] Y + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [Y] 207.88/68.76 207.88/68.76 [and(tt(), X)] = [7 0 7] [7] 207.88/68.76 [7 7 7] X + [7] 207.88/68.76 [7 7 7] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 2 0] X + [0] 207.88/68.76 [1 0 2] [0] 207.88/68.76 = [activate(X)] 207.88/68.76 207.88/68.76 [fst(pair(X, Y))] = [1 0 0] [1 0 1] [6] 207.88/68.76 [0 4 0] X + [0 4 0] Y + [7] 207.88/68.76 [0 0 4] [0 0 0] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 1 0] X + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [X] 207.88/68.76 207.88/68.76 [head(cons(N, XS))] = [1 0 0] [0 0 0] [7] 207.88/68.76 [0 1 1] N + [0 1 4] XS + [7] 207.88/68.76 [0 1 1] [0 1 4] [7] 207.88/68.76 > [1 0 0] [0] 207.88/68.76 [0 1 0] N + [0] 207.88/68.76 [0 0 1] [0] 207.88/68.76 = [N] 207.88/68.76 207.88/68.76 [natsFrom(N)] = [1 0 0] [0] 207.88/68.76 [1 1 1] N + [0] 207.88/68.76 [1 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [1 1 1] N + [0] 207.88/68.76 [1 0 0] [0] 207.88/68.76 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.76 207.88/68.76 [natsFrom(X)] = [1 0 0] [0] 207.88/68.76 [1 1 1] X + [0] 207.88/68.76 [1 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.76 [1 1 1] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 = [n__natsFrom(X)] 207.88/68.76 207.88/68.76 [sel(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.76 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.76 [7 7 7] [7 7 7] [7] 207.88/68.76 >= [4 0 0] [2 0 2] [7] 207.88/68.76 [0 0 0] N + [0 4 0] XS + [7] 207.88/68.76 [0 0 0] [0 4 0] [7] 207.88/68.76 = [head(afterNth(N, XS))] 207.88/68.76 207.88/68.76 [s(X)] = [1 0 0] [0] 207.88/68.76 [0 0 0] X + [0] 207.88/68.76 [0 0 0] [0] 207.88/68.76 >= [1 0 0] [0] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 = [n__s(X)] 207.88/68.77 207.88/68.77 [tail(cons(N, XS))] = [0 0 0] [4 0 0] [7] 207.88/68.77 [0 2 2] N + [4 2 8] XS + [7] 207.88/68.77 [0 2 2] [4 2 8] [7] 207.88/68.77 > [1 0 0] [0] 207.88/68.77 [0 2 0] XS + [0] 207.88/68.77 [1 0 2] [0] 207.88/68.77 = [activate(XS)] 207.88/68.77 207.88/68.77 [take(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.77 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 > [4 0 0] [2 0 1] [6] 207.88/68.77 [0 0 0] N + [0 4 0] XS + [7] 207.88/68.77 [0 0 0] [0 0 0] [7] 207.88/68.77 = [fst(splitAt(N, XS))] 207.88/68.77 207.88/68.77 207.88/68.77 We return to the main proof. 207.88/68.77 207.88/68.77 We are left with following problem, upon which TcT provides the 207.88/68.77 certificate YES(O(1),O(n^1)). 207.88/68.77 207.88/68.77 Strict Trs: 207.88/68.77 { activate(X) -> X 207.88/68.77 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.77 , activate(n__s(X)) -> s(activate(X)) 207.88/68.77 , natsFrom(X) -> n__natsFrom(X) 207.88/68.77 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.77 , s(X) -> n__s(X) } 207.88/68.77 Weak Trs: 207.88/68.77 { U11(tt(), N, X, XS) -> 207.88/68.77 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.77 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.77 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.77 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.77 , snd(pair(X, Y)) -> Y 207.88/68.77 , and(tt(), X) -> activate(X) 207.88/68.77 , fst(pair(X, Y)) -> X 207.88/68.77 , head(cons(N, XS)) -> N 207.88/68.77 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.77 , tail(cons(N, XS)) -> activate(XS) 207.88/68.77 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.77 Obligation: 207.88/68.77 innermost runtime complexity 207.88/68.77 Answer: 207.88/68.77 YES(O(1),O(n^1)) 207.88/68.77 207.88/68.77 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.77 orient following rules strictly. 207.88/68.77 207.88/68.77 Trs: { activate(n__natsFrom(X)) -> natsFrom(activate(X)) } 207.88/68.77 207.88/68.77 The induced complexity on above rules (modulo remaining rules) is 207.88/68.77 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.77 component(s). 207.88/68.77 207.88/68.77 Sub-proof: 207.88/68.77 ---------- 207.88/68.77 The following argument positions are usable: 207.88/68.77 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.77 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.77 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.77 207.88/68.77 TcT has computed the following constructor-based matrix 207.88/68.77 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.77 207.88/68.77 [7 0 4] [7 0 7] [7 0 7] [7 0 207.88/68.77 7] [3] 207.88/68.77 [U11](x1, x2, x3, x4) = [7 7 7] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.77 7] x4 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7 7 7] [7 7 207.88/68.77 7] [7] 207.88/68.77 207.88/68.77 [0] 207.88/68.77 [tt] = [0] 207.88/68.77 [0] 207.88/68.77 207.88/68.77 [2 0 0] [2 0 0] [0] 207.88/68.77 [U12](x1, x2) = [0 1 1] x1 + [0 2 0] x2 + [0] 207.88/68.77 [1 0 1] [0 2 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [1 0 0] [0] 207.88/68.77 [splitAt](x1, x2) = [1 0 0] x1 + [0 1 0] x2 + [0] 207.88/68.77 [0 0 0] [0 0 2] [0] 207.88/68.77 207.88/68.77 [2 0 0] [0] 207.88/68.77 [activate](x1) = [0 2 0] x1 + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [1 0 0] [0] 207.88/68.77 [pair](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 207.88/68.77 [0 0 1] [0 0 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [0 0 0] [0] 207.88/68.77 [cons](x1, x2) = [0 1 0] x1 + [0 1 1] x2 + [0] 207.88/68.77 [0 0 1] [1 0 0] [0] 207.88/68.77 207.88/68.77 [4 0 0] [4 0 0] [0] 207.88/68.77 [afterNth](x1, x2) = [1 0 0] x1 + [0 1 0] x2 + [0] 207.88/68.77 [0 0 0] [0 0 4] [0] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [snd](x1) = [0 1 0] x1 + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 207.88/68.77 [7 0 4] [7 0 7] [7] 207.88/68.77 [and](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 207.88/68.77 [4 0 0] [7] 207.88/68.77 [fst](x1) = [0 4 0] x1 + [7] 207.88/68.77 [0 0 1] [7] 207.88/68.77 207.88/68.77 [1 0 0] [7] 207.88/68.77 [head](x1) = [0 1 0] x1 + [7] 207.88/68.77 [0 0 1] [7] 207.88/68.77 207.88/68.77 [1 0 0] [1] 207.88/68.77 [natsFrom](x1) = [1 1 0] x1 + [4] 207.88/68.77 [1 0 1] [4] 207.88/68.77 207.88/68.77 [1 0 0] [1] 207.88/68.77 [n__natsFrom](x1) = [1 1 0] x1 + [4] 207.88/68.77 [0 0 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [n__s](x1) = [0 0 0] x1 + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 207.88/68.77 [7 0 7] [7 0 7] [7] 207.88/68.77 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 207.88/68.77 [4] 207.88/68.77 [0] = [0] 207.88/68.77 [0] 207.88/68.77 207.88/68.77 [0] 207.88/68.77 [nil] = [0] 207.88/68.77 [0] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [s](x1) = [0 0 0] x1 + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 207.88/68.77 [0 0 2] [7] 207.88/68.77 [tail](x1) = [0 4 0] x1 + [7] 207.88/68.77 [0 4 0] [7] 207.88/68.77 207.88/68.77 [7 0 7] [7 0 7] [7] 207.88/68.77 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 207.88/68.77 The order satisfies the following ordering constraints: 207.88/68.77 207.88/68.77 [U11(tt(), N, X, XS)] = [7 0 7] [7 0 7] [7 0 7] [3] 207.88/68.77 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [7] 207.88/68.77 [7 7 7] [7 7 7] [7 7 7] [7] 207.88/68.77 > [4 0 0] [4 0 0] [4 0 0] [0] 207.88/68.77 [2 0 0] N + [0 4 0] X + [0 6 2] XS + [0] 207.88/68.77 [2 0 0] [0 6 1] [2 4 2] [0] 207.88/68.77 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.77 207.88/68.77 [U12(pair(YS, ZS), X)] = [2 0 0] [2 0 0] [2 0 0] [0] 207.88/68.77 [0 2 0] X + [0 1 1] YS + [0 1 1] ZS + [0] 207.88/68.77 [0 2 1] [1 0 1] [1 0 1] [0] 207.88/68.77 >= [2 0 0] [0 0 0] [1 0 0] [0] 207.88/68.77 [0 2 0] X + [0 1 1] YS + [0 1 0] ZS + [0] 207.88/68.77 [0 2 1] [1 0 0] [0 0 1] [0] 207.88/68.77 = [pair(cons(activate(X), YS), ZS)] 207.88/68.77 207.88/68.77 [splitAt(0(), XS)] = [1 0 0] [4] 207.88/68.77 [0 1 0] XS + [4] 207.88/68.77 [0 0 2] [0] 207.88/68.77 > [1 0 0] [0] 207.88/68.77 [0 1 0] XS + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [pair(nil(), XS)] 207.88/68.77 207.88/68.77 [activate(X)] = [2 0 0] [0] 207.88/68.77 [0 2 0] X + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [0 1 0] X + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [X] 207.88/68.77 207.88/68.77 [activate(n__natsFrom(X))] = [2 0 0] [2] 207.88/68.77 [2 2 0] X + [8] 207.88/68.77 [2 2 1] [8] 207.88/68.77 > [2 0 0] [1] 207.88/68.77 [2 2 0] X + [4] 207.88/68.77 [2 2 1] [4] 207.88/68.77 = [natsFrom(activate(X))] 207.88/68.77 207.88/68.77 [activate(n__s(X))] = [2 0 0] [0] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 >= [2 0 0] [0] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 = [s(activate(X))] 207.88/68.77 207.88/68.77 [afterNth(N, XS)] = [4 0 0] [4 0 0] [0] 207.88/68.77 [1 0 0] N + [0 1 0] XS + [0] 207.88/68.77 [0 0 0] [0 0 4] [0] 207.88/68.77 >= [1 0 0] [1 0 0] [0] 207.88/68.77 [1 0 0] N + [0 1 0] XS + [0] 207.88/68.77 [0 0 0] [0 0 2] [0] 207.88/68.77 = [snd(splitAt(N, XS))] 207.88/68.77 207.88/68.77 [snd(pair(X, Y))] = [1 0 0] [1 0 0] [0] 207.88/68.77 [0 1 0] X + [0 1 0] Y + [0] 207.88/68.77 [0 0 1] [0 0 1] [0] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [0 1 0] Y + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [Y] 207.88/68.77 207.88/68.77 [and(tt(), X)] = [7 0 7] [7] 207.88/68.77 [7 7 7] X + [7] 207.88/68.77 [7 7 7] [7] 207.88/68.77 > [2 0 0] [0] 207.88/68.77 [0 2 0] X + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 = [activate(X)] 207.88/68.77 207.88/68.77 [fst(pair(X, Y))] = [4 0 0] [4 0 0] [7] 207.88/68.77 [0 4 0] X + [0 4 0] Y + [7] 207.88/68.77 [0 0 1] [0 0 1] [7] 207.88/68.77 > [1 0 0] [0] 207.88/68.77 [0 1 0] X + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [X] 207.88/68.77 207.88/68.77 [head(cons(N, XS))] = [1 0 0] [0 0 0] [7] 207.88/68.77 [0 1 0] N + [0 1 1] XS + [7] 207.88/68.77 [0 0 1] [1 0 0] [7] 207.88/68.77 > [1 0 0] [0] 207.88/68.77 [0 1 0] N + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [N] 207.88/68.77 207.88/68.77 [natsFrom(N)] = [1 0 0] [1] 207.88/68.77 [1 1 0] N + [4] 207.88/68.77 [1 0 1] [4] 207.88/68.77 > [1 0 0] [0] 207.88/68.77 [1 1 0] N + [4] 207.88/68.77 [1 0 1] [1] 207.88/68.77 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.77 207.88/68.77 [natsFrom(X)] = [1 0 0] [1] 207.88/68.77 [1 1 0] X + [4] 207.88/68.77 [1 0 1] [4] 207.88/68.77 >= [1 0 0] [1] 207.88/68.77 [1 1 0] X + [4] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [n__natsFrom(X)] 207.88/68.77 207.88/68.77 [sel(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.77 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 >= [4 0 0] [4 0 0] [7] 207.88/68.77 [1 0 0] N + [0 1 0] XS + [7] 207.88/68.77 [0 0 0] [0 0 4] [7] 207.88/68.77 = [head(afterNth(N, XS))] 207.88/68.77 207.88/68.77 [s(X)] = [1 0 0] [0] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 = [n__s(X)] 207.88/68.77 207.88/68.77 [tail(cons(N, XS))] = [0 0 2] [2 0 0] [7] 207.88/68.77 [0 4 0] N + [0 4 4] XS + [7] 207.88/68.77 [0 4 0] [0 4 4] [7] 207.88/68.77 > [2 0 0] [0] 207.88/68.77 [0 2 0] XS + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 = [activate(XS)] 207.88/68.77 207.88/68.77 [take(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.77 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 >= [4 0 0] [4 0 0] [7] 207.88/68.77 [4 0 0] N + [0 4 0] XS + [7] 207.88/68.77 [0 0 0] [0 0 2] [7] 207.88/68.77 = [fst(splitAt(N, XS))] 207.88/68.77 207.88/68.77 207.88/68.77 We return to the main proof. 207.88/68.77 207.88/68.77 We are left with following problem, upon which TcT provides the 207.88/68.77 certificate YES(O(1),O(n^1)). 207.88/68.77 207.88/68.77 Strict Trs: 207.88/68.77 { activate(X) -> X 207.88/68.77 , activate(n__s(X)) -> s(activate(X)) 207.88/68.77 , natsFrom(X) -> n__natsFrom(X) 207.88/68.77 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.77 , s(X) -> n__s(X) } 207.88/68.77 Weak Trs: 207.88/68.77 { U11(tt(), N, X, XS) -> 207.88/68.77 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.77 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.77 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.77 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.77 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.77 , snd(pair(X, Y)) -> Y 207.88/68.77 , and(tt(), X) -> activate(X) 207.88/68.77 , fst(pair(X, Y)) -> X 207.88/68.77 , head(cons(N, XS)) -> N 207.88/68.77 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.77 , tail(cons(N, XS)) -> activate(XS) 207.88/68.77 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.77 Obligation: 207.88/68.77 innermost runtime complexity 207.88/68.77 Answer: 207.88/68.77 YES(O(1),O(n^1)) 207.88/68.77 207.88/68.77 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.77 orient following rules strictly. 207.88/68.77 207.88/68.77 Trs: 207.88/68.77 { activate(n__s(X)) -> s(activate(X)) 207.88/68.77 , s(X) -> n__s(X) } 207.88/68.77 207.88/68.77 The induced complexity on above rules (modulo remaining rules) is 207.88/68.77 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.77 component(s). 207.88/68.77 207.88/68.77 Sub-proof: 207.88/68.77 ---------- 207.88/68.77 The following argument positions are usable: 207.88/68.77 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.77 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.77 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.77 207.88/68.77 TcT has computed the following constructor-based matrix 207.88/68.77 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.77 207.88/68.77 [7 0 4] [7 0 7] [7 0 7] [7 0 207.88/68.77 7] [7] 207.88/68.77 [U11](x1, x2, x3, x4) = [7 7 7] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.77 7] x4 + [3] 207.88/68.77 [7 7 7] [7 7 7] [7 7 7] [7 7 207.88/68.77 7] [3] 207.88/68.77 207.88/68.77 [0] 207.88/68.77 [tt] = [0] 207.88/68.77 [0] 207.88/68.77 207.88/68.77 [2 0 0] [2 0 0] [0] 207.88/68.77 [U12](x1, x2) = [0 1 0] x1 + [0 2 0] x2 + [0] 207.88/68.77 [1 0 2] [0 2 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [1 0 0] [0] 207.88/68.77 [splitAt](x1, x2) = [0 0 0] x1 + [1 1 0] x2 + [0] 207.88/68.77 [0 0 0] [0 0 1] [0] 207.88/68.77 207.88/68.77 [2 0 0] [0] 207.88/68.77 [activate](x1) = [0 2 0] x1 + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [1 0 0] [0] 207.88/68.77 [pair](x1, x2) = [0 1 0] x1 + [1 1 0] x2 + [0] 207.88/68.77 [0 0 1] [0 0 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [0 0 0] [0] 207.88/68.77 [cons](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 207.88/68.77 [0 0 1] [1 0 1] [0] 207.88/68.77 207.88/68.77 [4 0 0] [4 0 0] [0] 207.88/68.77 [afterNth](x1, x2) = [0 4 0] x1 + [4 4 2] x2 + [0] 207.88/68.77 [0 0 0] [0 0 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [snd](x1) = [0 4 0] x1 + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 207.88/68.77 [7 0 4] [7 0 7] [7] 207.88/68.77 [and](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 207.88/68.77 [4 0 0] [7] 207.88/68.77 [fst](x1) = [0 1 0] x1 + [7] 207.88/68.77 [0 0 4] [7] 207.88/68.77 207.88/68.77 [1 0 0] [7] 207.88/68.77 [head](x1) = [0 1 2] x1 + [7] 207.88/68.77 [0 1 2] [7] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [natsFrom](x1) = [1 1 0] x1 + [6] 207.88/68.77 [1 0 1] [2] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [n__natsFrom](x1) = [1 1 0] x1 + [4] 207.88/68.77 [0 0 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [2] 207.88/68.77 [n__s](x1) = [0 0 0] x1 + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 207.88/68.77 [7 0 7] [7 0 7] [7] 207.88/68.77 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 207.88/68.77 [0] 207.88/68.77 [0] = [0] 207.88/68.77 [0] 207.88/68.77 207.88/68.77 [0] 207.88/68.77 [nil] = [0] 207.88/68.77 [0] 207.88/68.77 207.88/68.77 [1 0 0] [3] 207.88/68.77 [s](x1) = [0 0 0] x1 + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 207.88/68.77 [0 0 4] [7] 207.88/68.77 [tail](x1) = [0 2 4] x1 + [7] 207.88/68.77 [0 2 1] [7] 207.88/68.77 207.88/68.77 [7 0 7] [7 0 7] [7] 207.88/68.77 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 207.88/68.77 The order satisfies the following ordering constraints: 207.88/68.77 207.88/68.77 [U11(tt(), N, X, XS)] = [7 0 7] [7 0 7] [7 0 7] [7] 207.88/68.77 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [3] 207.88/68.77 [7 7 7] [7 7 7] [7 7 7] [3] 207.88/68.77 > [4 0 0] [4 0 0] [4 0 0] [0] 207.88/68.77 [0 0 0] N + [0 4 0] X + [2 2 0] XS + [0] 207.88/68.77 [2 0 0] [0 6 1] [2 4 2] [0] 207.88/68.77 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.77 207.88/68.77 [U12(pair(YS, ZS), X)] = [2 0 0] [2 0 0] [2 0 0] [0] 207.88/68.77 [0 2 0] X + [0 1 0] YS + [1 1 0] ZS + [0] 207.88/68.77 [0 2 1] [1 0 2] [1 0 2] [0] 207.88/68.77 >= [2 0 0] [0 0 0] [1 0 0] [0] 207.88/68.77 [0 2 0] X + [0 1 0] YS + [1 1 0] ZS + [0] 207.88/68.77 [0 2 1] [1 0 1] [0 0 1] [0] 207.88/68.77 = [pair(cons(activate(X), YS), ZS)] 207.88/68.77 207.88/68.77 [splitAt(0(), XS)] = [1 0 0] [0] 207.88/68.77 [1 1 0] XS + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [1 1 0] XS + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [pair(nil(), XS)] 207.88/68.77 207.88/68.77 [activate(X)] = [2 0 0] [0] 207.88/68.77 [0 2 0] X + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [0 1 0] X + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [X] 207.88/68.77 207.88/68.77 [activate(n__natsFrom(X))] = [2 0 0] [0] 207.88/68.77 [2 2 0] X + [8] 207.88/68.77 [2 2 1] [8] 207.88/68.77 >= [2 0 0] [0] 207.88/68.77 [2 2 0] X + [6] 207.88/68.77 [2 2 1] [2] 207.88/68.77 = [natsFrom(activate(X))] 207.88/68.77 207.88/68.77 [activate(n__s(X))] = [2 0 0] [4] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 > [2 0 0] [3] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 = [s(activate(X))] 207.88/68.77 207.88/68.77 [afterNth(N, XS)] = [4 0 0] [4 0 0] [0] 207.88/68.77 [0 4 0] N + [4 4 2] XS + [0] 207.88/68.77 [0 0 0] [0 0 1] [0] 207.88/68.77 >= [1 0 0] [1 0 0] [0] 207.88/68.77 [0 0 0] N + [4 4 0] XS + [0] 207.88/68.77 [0 0 0] [0 0 1] [0] 207.88/68.77 = [snd(splitAt(N, XS))] 207.88/68.77 207.88/68.77 [snd(pair(X, Y))] = [1 0 0] [1 0 0] [0] 207.88/68.77 [0 4 0] X + [4 4 0] Y + [0] 207.88/68.77 [0 0 1] [0 0 1] [0] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [0 1 0] Y + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [Y] 207.88/68.77 207.88/68.77 [and(tt(), X)] = [7 0 7] [7] 207.88/68.77 [7 7 7] X + [7] 207.88/68.77 [7 7 7] [7] 207.88/68.77 > [2 0 0] [0] 207.88/68.77 [0 2 0] X + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 = [activate(X)] 207.88/68.77 207.88/68.77 [fst(pair(X, Y))] = [4 0 0] [4 0 0] [7] 207.88/68.77 [0 1 0] X + [1 1 0] Y + [7] 207.88/68.77 [0 0 4] [0 0 4] [7] 207.88/68.77 > [1 0 0] [0] 207.88/68.77 [0 1 0] X + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [X] 207.88/68.77 207.88/68.77 [head(cons(N, XS))] = [1 0 0] [0 0 0] [7] 207.88/68.77 [0 1 2] N + [2 1 2] XS + [7] 207.88/68.77 [0 1 2] [2 1 2] [7] 207.88/68.77 > [1 0 0] [0] 207.88/68.77 [0 1 0] N + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [N] 207.88/68.77 207.88/68.77 [natsFrom(N)] = [1 0 0] [0] 207.88/68.77 [1 1 0] N + [6] 207.88/68.77 [1 0 1] [2] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [1 1 0] N + [6] 207.88/68.77 [1 0 1] [2] 207.88/68.77 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.77 207.88/68.77 [natsFrom(X)] = [1 0 0] [0] 207.88/68.77 [1 1 0] X + [6] 207.88/68.77 [1 0 1] [2] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [1 1 0] X + [4] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [n__natsFrom(X)] 207.88/68.77 207.88/68.77 [sel(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.77 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 >= [4 0 0] [4 0 0] [7] 207.88/68.77 [0 4 0] N + [4 4 4] XS + [7] 207.88/68.77 [0 4 0] [4 4 4] [7] 207.88/68.77 = [head(afterNth(N, XS))] 207.88/68.77 207.88/68.77 [s(X)] = [1 0 0] [3] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 > [1 0 0] [2] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 = [n__s(X)] 207.88/68.77 207.88/68.77 [tail(cons(N, XS))] = [0 0 4] [4 0 4] [7] 207.88/68.77 [0 2 4] N + [4 2 4] XS + [7] 207.88/68.77 [0 2 1] [1 2 1] [7] 207.88/68.77 > [2 0 0] [0] 207.88/68.77 [0 2 0] XS + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 = [activate(XS)] 207.88/68.77 207.88/68.77 [take(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.77 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 >= [4 0 0] [4 0 0] [7] 207.88/68.77 [0 0 0] N + [1 1 0] XS + [7] 207.88/68.77 [0 0 0] [0 0 4] [7] 207.88/68.77 = [fst(splitAt(N, XS))] 207.88/68.77 207.88/68.77 207.88/68.77 We return to the main proof. 207.88/68.77 207.88/68.77 We are left with following problem, upon which TcT provides the 207.88/68.77 certificate YES(O(1),O(n^1)). 207.88/68.77 207.88/68.77 Strict Trs: 207.88/68.77 { activate(X) -> X 207.88/68.77 , natsFrom(X) -> n__natsFrom(X) 207.88/68.77 , sel(N, XS) -> head(afterNth(N, XS)) } 207.88/68.77 Weak Trs: 207.88/68.77 { U11(tt(), N, X, XS) -> 207.88/68.77 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.77 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.77 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.77 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.77 , activate(n__s(X)) -> s(activate(X)) 207.88/68.77 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.77 , snd(pair(X, Y)) -> Y 207.88/68.77 , and(tt(), X) -> activate(X) 207.88/68.77 , fst(pair(X, Y)) -> X 207.88/68.77 , head(cons(N, XS)) -> N 207.88/68.77 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.77 , s(X) -> n__s(X) 207.88/68.77 , tail(cons(N, XS)) -> activate(XS) 207.88/68.77 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.77 Obligation: 207.88/68.77 innermost runtime complexity 207.88/68.77 Answer: 207.88/68.77 YES(O(1),O(n^1)) 207.88/68.77 207.88/68.77 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.77 orient following rules strictly. 207.88/68.77 207.88/68.77 Trs: { natsFrom(X) -> n__natsFrom(X) } 207.88/68.77 207.88/68.77 The induced complexity on above rules (modulo remaining rules) is 207.88/68.77 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.77 component(s). 207.88/68.77 207.88/68.77 Sub-proof: 207.88/68.77 ---------- 207.88/68.77 The following argument positions are usable: 207.88/68.77 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.77 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.77 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.77 207.88/68.77 TcT has computed the following constructor-based matrix 207.88/68.77 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.77 207.88/68.77 [4 0 0] [7 0 7] [7 0 7] [7 0 207.88/68.77 7] [3] 207.88/68.77 [U11](x1, x2, x3, x4) = [0 7 2] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.77 7] x4 + [7] 207.88/68.77 [0 7 2] [7 7 7] [7 7 7] [7 7 207.88/68.77 7] [7] 207.88/68.77 207.88/68.77 [2] 207.88/68.77 [tt] = [0] 207.88/68.77 [4] 207.88/68.77 207.88/68.77 [1 0 0] [2 0 0] [6] 207.88/68.77 [U12](x1, x2) = [0 1 0] x1 + [0 2 0] x2 + [0] 207.88/68.77 [1 0 2] [0 2 1] [6] 207.88/68.77 207.88/68.77 [2 0 0] [2 0 0] [0] 207.88/68.77 [splitAt](x1, x2) = [0 1 0] x1 + [0 2 0] x2 + [0] 207.88/68.77 [0 0 0] [0 0 1] [1] 207.88/68.77 207.88/68.77 [2 0 0] [0] 207.88/68.77 [activate](x1) = [0 2 0] x1 + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [1 0 0] [2] 207.88/68.77 [pair](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 207.88/68.77 [0 0 1] [0 0 1] [1] 207.88/68.77 207.88/68.77 [1 0 0] [0 0 0] [0] 207.88/68.77 [cons](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 207.88/68.77 [0 0 1] [1 0 1] [0] 207.88/68.77 207.88/68.77 [4 0 4] [4 0 0] [0] 207.88/68.77 [afterNth](x1, x2) = [0 4 0] x1 + [0 4 0] x2 + [0] 207.88/68.77 [0 0 0] [4 0 1] [1] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [snd](x1) = [0 2 0] x1 + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 207.88/68.77 [0 0 0] [7 0 7] [7] 207.88/68.77 [and](x1, x2) = [0 7 0] x1 + [7 7 7] x2 + [7] 207.88/68.77 [0 7 0] [7 7 7] [7] 207.88/68.77 207.88/68.77 [2 0 0] [7] 207.88/68.77 [fst](x1) = [0 2 0] x1 + [7] 207.88/68.77 [0 0 1] [6] 207.88/68.77 207.88/68.77 [1 0 0] [7] 207.88/68.77 [head](x1) = [0 1 0] x1 + [7] 207.88/68.77 [0 0 1] [6] 207.88/68.77 207.88/68.77 [1 0 0] [2] 207.88/68.77 [natsFrom](x1) = [1 1 0] x1 + [1] 207.88/68.77 [1 0 1] [1] 207.88/68.77 207.88/68.77 [1 0 0] [1] 207.88/68.77 [n__natsFrom](x1) = [1 1 0] x1 + [1] 207.88/68.77 [0 0 1] [0] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [n__s](x1) = [0 0 0] x1 + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 207.88/68.77 [7 0 7] [7 0 7] [7] 207.88/68.77 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 207.88/68.77 [4] 207.88/68.77 [0] = [4] 207.88/68.77 [0] 207.88/68.77 207.88/68.77 [0] 207.88/68.77 [nil] = [0] 207.88/68.77 [0] 207.88/68.77 207.88/68.77 [1 0 0] [0] 207.88/68.77 [s](x1) = [0 0 0] x1 + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 207.88/68.77 [0 0 2] [7] 207.88/68.77 [tail](x1) = [0 4 0] x1 + [7] 207.88/68.77 [0 2 1] [7] 207.88/68.77 207.88/68.77 [7 0 7] [7 0 7] [7] 207.88/68.77 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.77 [7 7 7] [7 7 7] [7] 207.88/68.77 207.88/68.77 The order satisfies the following ordering constraints: 207.88/68.77 207.88/68.77 [U11(tt(), N, X, XS)] = [7 0 7] [7 0 7] [7 0 7] [11] 207.88/68.77 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [15] 207.88/68.77 [7 7 7] [7 7 7] [7 7 7] [15] 207.88/68.77 > [4 0 0] [4 0 0] [4 0 0] [6] 207.88/68.77 [0 2 0] N + [0 4 0] X + [0 4 0] XS + [0] 207.88/68.77 [4 0 0] [0 6 1] [4 4 2] [8] 207.88/68.77 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.77 207.88/68.77 [U12(pair(YS, ZS), X)] = [2 0 0] [1 0 0] [1 0 0] [8] 207.88/68.77 [0 2 0] X + [0 1 0] YS + [0 1 0] ZS + [0] 207.88/68.77 [0 2 1] [1 0 2] [1 0 2] [10] 207.88/68.77 > [2 0 0] [0 0 0] [1 0 0] [2] 207.88/68.77 [0 2 0] X + [0 1 0] YS + [0 1 0] ZS + [0] 207.88/68.77 [0 2 1] [1 0 1] [0 0 1] [1] 207.88/68.77 = [pair(cons(activate(X), YS), ZS)] 207.88/68.77 207.88/68.77 [splitAt(0(), XS)] = [2 0 0] [8] 207.88/68.77 [0 2 0] XS + [4] 207.88/68.77 [0 0 1] [1] 207.88/68.77 > [1 0 0] [2] 207.88/68.77 [0 1 0] XS + [0] 207.88/68.77 [0 0 1] [1] 207.88/68.77 = [pair(nil(), XS)] 207.88/68.77 207.88/68.77 [activate(X)] = [2 0 0] [0] 207.88/68.77 [0 2 0] X + [0] 207.88/68.77 [0 2 1] [0] 207.88/68.77 >= [1 0 0] [0] 207.88/68.77 [0 1 0] X + [0] 207.88/68.77 [0 0 1] [0] 207.88/68.77 = [X] 207.88/68.77 207.88/68.77 [activate(n__natsFrom(X))] = [2 0 0] [2] 207.88/68.77 [2 2 0] X + [2] 207.88/68.77 [2 2 1] [2] 207.88/68.77 >= [2 0 0] [2] 207.88/68.77 [2 2 0] X + [1] 207.88/68.77 [2 2 1] [1] 207.88/68.77 = [natsFrom(activate(X))] 207.88/68.77 207.88/68.77 [activate(n__s(X))] = [2 0 0] [0] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.77 >= [2 0 0] [0] 207.88/68.77 [0 0 0] X + [0] 207.88/68.77 [0 0 0] [0] 207.88/68.78 = [s(activate(X))] 207.88/68.78 207.88/68.78 [afterNth(N, XS)] = [4 0 4] [4 0 0] [0] 207.88/68.78 [0 4 0] N + [0 4 0] XS + [0] 207.88/68.78 [0 0 0] [4 0 1] [1] 207.88/68.78 >= [2 0 0] [2 0 0] [0] 207.88/68.78 [0 2 0] N + [0 4 0] XS + [0] 207.88/68.78 [0 0 0] [0 0 1] [1] 207.88/68.78 = [snd(splitAt(N, XS))] 207.88/68.78 207.88/68.78 [snd(pair(X, Y))] = [1 0 0] [1 0 0] [2] 207.88/68.78 [0 2 0] X + [0 2 0] Y + [0] 207.88/68.78 [0 0 1] [0 0 1] [1] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] Y + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [Y] 207.88/68.78 207.88/68.78 [and(tt(), X)] = [7 0 7] [7] 207.88/68.78 [7 7 7] X + [7] 207.88/68.78 [7 7 7] [7] 207.88/68.78 > [2 0 0] [0] 207.88/68.78 [0 2 0] X + [0] 207.88/68.78 [0 2 1] [0] 207.88/68.78 = [activate(X)] 207.88/68.78 207.88/68.78 [fst(pair(X, Y))] = [2 0 0] [2 0 0] [11] 207.88/68.78 [0 2 0] X + [0 2 0] Y + [7] 207.88/68.78 [0 0 1] [0 0 1] [7] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] X + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [X] 207.88/68.78 207.88/68.78 [head(cons(N, XS))] = [1 0 0] [0 0 0] [7] 207.88/68.78 [0 1 0] N + [0 1 0] XS + [7] 207.88/68.78 [0 0 1] [1 0 1] [6] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] N + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [N] 207.88/68.78 207.88/68.78 [natsFrom(N)] = [1 0 0] [2] 207.88/68.78 [1 1 0] N + [1] 207.88/68.78 [1 0 1] [1] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [1 1 0] N + [1] 207.88/68.78 [1 0 1] [1] 207.88/68.78 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.78 207.88/68.78 [natsFrom(X)] = [1 0 0] [2] 207.88/68.78 [1 1 0] X + [1] 207.88/68.78 [1 0 1] [1] 207.88/68.78 > [1 0 0] [1] 207.88/68.78 [1 1 0] X + [1] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [n__natsFrom(X)] 207.88/68.78 207.88/68.78 [sel(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.78 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 >= [4 0 4] [4 0 0] [7] 207.88/68.78 [0 4 0] N + [0 4 0] XS + [7] 207.88/68.78 [0 0 0] [4 0 1] [7] 207.88/68.78 = [head(afterNth(N, XS))] 207.88/68.78 207.88/68.78 [s(X)] = [1 0 0] [0] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 = [n__s(X)] 207.88/68.78 207.88/68.78 [tail(cons(N, XS))] = [0 0 2] [2 0 2] [7] 207.88/68.78 [0 4 0] N + [0 4 0] XS + [7] 207.88/68.78 [0 2 1] [1 2 1] [7] 207.88/68.78 > [2 0 0] [0] 207.88/68.78 [0 2 0] XS + [0] 207.88/68.78 [0 2 1] [0] 207.88/68.78 = [activate(XS)] 207.88/68.78 207.88/68.78 [take(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.78 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 >= [4 0 0] [4 0 0] [7] 207.88/68.78 [0 2 0] N + [0 4 0] XS + [7] 207.88/68.78 [0 0 0] [0 0 1] [7] 207.88/68.78 = [fst(splitAt(N, XS))] 207.88/68.78 207.88/68.78 207.88/68.78 We return to the main proof. 207.88/68.78 207.88/68.78 We are left with following problem, upon which TcT provides the 207.88/68.78 certificate YES(O(1),O(n^1)). 207.88/68.78 207.88/68.78 Strict Trs: 207.88/68.78 { activate(X) -> X 207.88/68.78 , sel(N, XS) -> head(afterNth(N, XS)) } 207.88/68.78 Weak Trs: 207.88/68.78 { U11(tt(), N, X, XS) -> 207.88/68.78 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.78 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.78 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.78 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.78 , activate(n__s(X)) -> s(activate(X)) 207.88/68.78 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.78 , snd(pair(X, Y)) -> Y 207.88/68.78 , and(tt(), X) -> activate(X) 207.88/68.78 , fst(pair(X, Y)) -> X 207.88/68.78 , head(cons(N, XS)) -> N 207.88/68.78 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.78 , natsFrom(X) -> n__natsFrom(X) 207.88/68.78 , s(X) -> n__s(X) 207.88/68.78 , tail(cons(N, XS)) -> activate(XS) 207.88/68.78 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.78 Obligation: 207.88/68.78 innermost runtime complexity 207.88/68.78 Answer: 207.88/68.78 YES(O(1),O(n^1)) 207.88/68.78 207.88/68.78 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.78 orient following rules strictly. 207.88/68.78 207.88/68.78 Trs: { sel(N, XS) -> head(afterNth(N, XS)) } 207.88/68.78 207.88/68.78 The induced complexity on above rules (modulo remaining rules) is 207.88/68.78 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.78 component(s). 207.88/68.78 207.88/68.78 Sub-proof: 207.88/68.78 ---------- 207.88/68.78 The following argument positions are usable: 207.88/68.78 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.78 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.78 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.78 207.88/68.78 TcT has computed the following constructor-based matrix 207.88/68.78 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.78 207.88/68.78 [0 4 0] [7 7 0] [7 7 0] [7 7 207.88/68.78 0] [7] 207.88/68.78 [U11](x1, x2, x3, x4) = [0 1 7] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.78 7] x4 + [7] 207.88/68.78 [4 0 7] [7 7 7] [7 7 7] [7 7 207.88/68.78 7] [3] 207.88/68.78 207.88/68.78 [2] 207.88/68.78 [tt] = [1] 207.88/68.78 [0] 207.88/68.78 207.88/68.78 [1 0 0] [1 0 0] [7] 207.88/68.78 [U12](x1, x2) = [0 1 0] x1 + [0 0 0] x2 + [0] 207.88/68.78 [0 0 1] [2 1 2] [0] 207.88/68.78 207.88/68.78 [4 0 0] [2 4 0] [1] 207.88/68.78 [splitAt](x1, x2) = [0 0 0] x1 + [0 4 0] x2 + [4] 207.88/68.78 [0 0 0] [1 0 1] [0] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [activate](x1) = [1 1 0] x1 + [0] 207.88/68.78 [0 0 2] [0] 207.88/68.78 207.88/68.78 [1 1 0] [1 0 0] [1] 207.88/68.78 [pair](x1, x2) = [0 0 0] x1 + [0 1 0] x2 + [0] 207.88/68.78 [0 0 1] [1 0 1] [0] 207.88/68.78 207.88/68.78 [1 0 0] [0 0 0] [0] 207.88/68.78 [cons](x1, x2) = [0 0 0] x1 + [1 1 0] x2 + [0] 207.88/68.78 [0 1 1] [0 0 1] [0] 207.88/68.78 207.88/68.78 [4 0 0] [2 4 0] [4] 207.88/68.78 [afterNth](x1, x2) = [0 4 0] x1 + [0 4 4] x2 + [4] 207.88/68.78 [0 0 0] [2 0 2] [0] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [snd](x1) = [0 1 0] x1 + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 207.88/68.78 [0 0 0] [7 7 0] [7] 207.88/68.78 [and](x1, x2) = [0 0 7] x1 + [7 7 7] x2 + [7] 207.88/68.78 [0 0 7] [7 7 7] [7] 207.88/68.78 207.88/68.78 [1 0 0] [6] 207.88/68.78 [fst](x1) = [1 0 0] x1 + [6] 207.88/68.78 [0 0 4] [7] 207.88/68.78 207.88/68.78 [1 0 0] [2] 207.88/68.78 [head](x1) = [0 0 1] x1 + [7] 207.88/68.78 [0 0 2] [7] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [natsFrom](x1) = [1 0 0] x1 + [0] 207.88/68.78 [1 1 1] [0] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [n__natsFrom](x1) = [0 0 0] x1 + [0] 207.88/68.78 [1 1 1] [0] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [n__s](x1) = [0 0 0] x1 + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 207.88/68.78 [7 7 0] [7 7 0] [7] 207.88/68.78 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 207.88/68.78 [0] 207.88/68.78 [0] = [0] 207.88/68.78 [0] 207.88/68.78 207.88/68.78 [0] 207.88/68.78 [nil] = [0] 207.88/68.78 [0] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [s](x1) = [0 0 0] x1 + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 207.88/68.78 [0 4 0] [7] 207.88/68.78 [tail](x1) = [0 2 0] x1 + [7] 207.88/68.78 [0 0 2] [7] 207.88/68.78 207.88/68.78 [7 7 0] [7 7 0] [7] 207.88/68.78 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 207.88/68.78 The order satisfies the following ordering constraints: 207.88/68.78 207.88/68.78 [U11(tt(), N, X, XS)] = [7 7 0] [7 7 0] [7 7 0] [11] 207.88/68.78 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [8] 207.88/68.78 [7 7 7] [7 7 7] [7 7 7] [11] 207.88/68.78 > [4 0 0] [1 0 0] [6 4 0] [8] 207.88/68.78 [0 0 0] N + [0 0 0] X + [4 4 0] XS + [4] 207.88/68.78 [0 0 0] [3 1 4] [1 0 2] [0] 207.88/68.78 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.78 207.88/68.78 [U12(pair(YS, ZS), X)] = [1 0 0] [1 1 0] [1 0 0] [8] 207.88/68.78 [0 0 0] X + [0 0 0] YS + [0 1 0] ZS + [0] 207.88/68.78 [2 1 2] [0 0 1] [1 0 1] [0] 207.88/68.78 > [1 0 0] [1 1 0] [1 0 0] [1] 207.88/68.78 [0 0 0] X + [0 0 0] YS + [0 1 0] ZS + [0] 207.88/68.78 [1 1 2] [0 0 1] [1 0 1] [0] 207.88/68.78 = [pair(cons(activate(X), YS), ZS)] 207.88/68.78 207.88/68.78 [splitAt(0(), XS)] = [2 4 0] [1] 207.88/68.78 [0 4 0] XS + [4] 207.88/68.78 [1 0 1] [0] 207.88/68.78 >= [1 0 0] [1] 207.88/68.78 [0 1 0] XS + [0] 207.88/68.78 [1 0 1] [0] 207.88/68.78 = [pair(nil(), XS)] 207.88/68.78 207.88/68.78 [activate(X)] = [1 0 0] [0] 207.88/68.78 [1 1 0] X + [0] 207.88/68.78 [0 0 2] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [0 1 0] X + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [X] 207.88/68.78 207.88/68.78 [activate(n__natsFrom(X))] = [1 0 0] [0] 207.88/68.78 [1 0 0] X + [0] 207.88/68.78 [2 2 2] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [1 0 0] X + [0] 207.88/68.78 [2 1 2] [0] 207.88/68.78 = [natsFrom(activate(X))] 207.88/68.78 207.88/68.78 [activate(n__s(X))] = [1 0 0] [0] 207.88/68.78 [1 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 = [s(activate(X))] 207.88/68.78 207.88/68.78 [afterNth(N, XS)] = [4 0 0] [2 4 0] [4] 207.88/68.78 [0 4 0] N + [0 4 4] XS + [4] 207.88/68.78 [0 0 0] [2 0 2] [0] 207.88/68.78 > [4 0 0] [2 4 0] [1] 207.88/68.78 [0 0 0] N + [0 4 0] XS + [4] 207.88/68.78 [0 0 0] [1 0 1] [0] 207.88/68.78 = [snd(splitAt(N, XS))] 207.88/68.78 207.88/68.78 [snd(pair(X, Y))] = [1 1 0] [1 0 0] [1] 207.88/68.78 [0 0 0] X + [0 1 0] Y + [0] 207.88/68.78 [0 0 1] [1 0 1] [0] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] Y + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [Y] 207.88/68.78 207.88/68.78 [and(tt(), X)] = [7 7 0] [7] 207.88/68.78 [7 7 7] X + [7] 207.88/68.78 [7 7 7] [7] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [1 1 0] X + [0] 207.88/68.78 [0 0 2] [0] 207.88/68.78 = [activate(X)] 207.88/68.78 207.88/68.78 [fst(pair(X, Y))] = [1 1 0] [1 0 0] [7] 207.88/68.78 [1 1 0] X + [1 0 0] Y + [7] 207.88/68.78 [0 0 4] [4 0 4] [7] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] X + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [X] 207.88/68.78 207.88/68.78 [head(cons(N, XS))] = [1 0 0] [0 0 0] [2] 207.88/68.78 [0 1 1] N + [0 0 1] XS + [7] 207.88/68.78 [0 2 2] [0 0 2] [7] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] N + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [N] 207.88/68.78 207.88/68.78 [natsFrom(N)] = [1 0 0] [0] 207.88/68.78 [1 0 0] N + [0] 207.88/68.78 [1 1 1] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [1 0 0] N + [0] 207.88/68.78 [1 1 1] [0] 207.88/68.78 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.78 207.88/68.78 [natsFrom(X)] = [1 0 0] [0] 207.88/68.78 [1 0 0] X + [0] 207.88/68.78 [1 1 1] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [1 1 1] [0] 207.88/68.78 = [n__natsFrom(X)] 207.88/68.78 207.88/68.78 [sel(N, XS)] = [7 7 0] [7 7 0] [7] 207.88/68.78 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 > [4 0 0] [2 4 0] [6] 207.88/68.78 [0 0 0] N + [2 0 2] XS + [7] 207.88/68.78 [0 0 0] [4 0 4] [7] 207.88/68.78 = [head(afterNth(N, XS))] 207.88/68.78 207.88/68.78 [s(X)] = [1 0 0] [0] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 = [n__s(X)] 207.88/68.78 207.88/68.78 [tail(cons(N, XS))] = [0 0 0] [4 4 0] [7] 207.88/68.78 [0 0 0] N + [2 2 0] XS + [7] 207.88/68.78 [0 2 2] [0 0 2] [7] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [1 1 0] XS + [0] 207.88/68.78 [0 0 2] [0] 207.88/68.78 = [activate(XS)] 207.88/68.78 207.88/68.78 [take(N, XS)] = [7 7 0] [7 7 0] [7] 207.88/68.78 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 >= [4 0 0] [2 4 0] [7] 207.88/68.78 [4 0 0] N + [2 4 0] XS + [7] 207.88/68.78 [0 0 0] [4 0 4] [7] 207.88/68.78 = [fst(splitAt(N, XS))] 207.88/68.78 207.88/68.78 207.88/68.78 We return to the main proof. 207.88/68.78 207.88/68.78 We are left with following problem, upon which TcT provides the 207.88/68.78 certificate YES(O(1),O(n^1)). 207.88/68.78 207.88/68.78 Strict Trs: { activate(X) -> X } 207.88/68.78 Weak Trs: 207.88/68.78 { U11(tt(), N, X, XS) -> 207.88/68.78 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.78 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.78 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.78 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.78 , activate(n__s(X)) -> s(activate(X)) 207.88/68.78 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.78 , snd(pair(X, Y)) -> Y 207.88/68.78 , and(tt(), X) -> activate(X) 207.88/68.78 , fst(pair(X, Y)) -> X 207.88/68.78 , head(cons(N, XS)) -> N 207.88/68.78 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.78 , natsFrom(X) -> n__natsFrom(X) 207.88/68.78 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.78 , s(X) -> n__s(X) 207.88/68.78 , tail(cons(N, XS)) -> activate(XS) 207.88/68.78 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.78 Obligation: 207.88/68.78 innermost runtime complexity 207.88/68.78 Answer: 207.88/68.78 YES(O(1),O(n^1)) 207.88/68.78 207.88/68.78 We use the processor 'matrix interpretation of dimension 3' to 207.88/68.78 orient following rules strictly. 207.88/68.78 207.88/68.78 Trs: { activate(X) -> X } 207.88/68.78 207.88/68.78 The induced complexity on above rules (modulo remaining rules) is 207.88/68.78 YES(?,O(n^1)) . These rules are moved into the corresponding weak 207.88/68.78 component(s). 207.88/68.78 207.88/68.78 Sub-proof: 207.88/68.78 ---------- 207.88/68.78 The following argument positions are usable: 207.88/68.78 Uargs(U12) = {1, 2}, Uargs(splitAt) = {1, 2}, Uargs(pair) = {1}, 207.88/68.78 Uargs(cons) = {1}, Uargs(snd) = {1}, Uargs(fst) = {1}, 207.88/68.78 Uargs(head) = {1}, Uargs(natsFrom) = {1}, Uargs(s) = {1} 207.88/68.78 207.88/68.78 TcT has computed the following constructor-based matrix 207.88/68.78 interpretation satisfying not(EDA) and not(IDA(1)). 207.88/68.78 207.88/68.78 [2 0 6] [7 0 7] [7 0 7] [7 0 207.88/68.78 7] [7] 207.88/68.78 [U11](x1, x2, x3, x4) = [0 4 0] x1 + [7 7 7] x2 + [7 7 7] x3 + [7 7 207.88/68.78 7] x4 + [7] 207.88/68.78 [1 0 0] [7 7 7] [7 7 7] [7 7 207.88/68.78 7] [7] 207.88/68.78 207.88/68.78 [1] 207.88/68.78 [tt] = [2] 207.88/68.78 [1] 207.88/68.78 207.88/68.78 [2 0 0] [1 0 0] [4] 207.88/68.78 [U12](x1, x2) = [1 1 0] x1 + [2 2 2] x2 + [2] 207.88/68.78 [0 2 1] [0 0 0] [4] 207.88/68.78 207.88/68.78 [1 0 0] [2 0 0] [2] 207.88/68.78 [splitAt](x1, x2) = [1 0 0] x1 + [0 1 0] x2 + [1] 207.88/68.78 [0 0 0] [0 0 2] [0] 207.88/68.78 207.88/68.78 [1 0 0] [1] 207.88/68.78 [activate](x1) = [1 2 0] x1 + [0] 207.88/68.78 [1 0 2] [0] 207.88/68.78 207.88/68.78 [1 0 0] [1 0 0] [0] 207.88/68.78 [pair](x1, x2) = [0 1 1] x1 + [0 1 0] x2 + [2] 207.88/68.78 [0 0 0] [0 0 1] [0] 207.88/68.78 207.88/68.78 [1 0 0] [0 0 0] [0] 207.88/68.78 [cons](x1, x2) = [0 1 1] x1 + [0 1 1] x2 + [0] 207.88/68.78 [0 0 0] [1 0 0] [0] 207.88/68.78 207.88/68.78 [4 0 0] [4 0 0] [4] 207.88/68.78 [afterNth](x1, x2) = [1 0 0] x1 + [0 1 0] x2 + [2] 207.88/68.78 [0 0 0] [4 0 4] [0] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [snd](x1) = [0 1 0] x1 + [0] 207.88/68.78 [0 0 2] [0] 207.88/68.78 207.88/68.78 [7 0 7] [7] 207.88/68.78 [and](x1, x2) = [7 7 7] x2 + [7] 207.88/68.78 [7 7 7] [7] 207.88/68.78 207.88/68.78 [2 0 0] [3] 207.88/68.78 [fst](x1) = [0 1 0] x1 + [4] 207.88/68.78 [0 4 0] [3] 207.88/68.78 207.88/68.78 [1 0 0] [3] 207.88/68.78 [head](x1) = [0 2 0] x1 + [3] 207.88/68.78 [0 1 0] [5] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [natsFrom](x1) = [1 1 1] x1 + [3] 207.88/68.78 [1 0 0] [1] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [n__natsFrom](x1) = [1 1 1] x1 + [2] 207.88/68.78 [0 0 0] [1] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [n__s](x1) = [0 0 0] x1 + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 207.88/68.78 [7 0 7] [7 0 7] [7] 207.88/68.78 [sel](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 207.88/68.78 [7] 207.88/68.78 [0] = [0] 207.88/68.78 [0] 207.88/68.78 207.88/68.78 [0] 207.88/68.78 [nil] = [2] 207.88/68.78 [4] 207.88/68.78 207.88/68.78 [1 0 0] [0] 207.88/68.78 [s](x1) = [0 0 0] x1 + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 207.88/68.78 [0 0 1] [7] 207.88/68.78 [tail](x1) = [0 4 1] x1 + [7] 207.88/68.78 [0 2 1] [7] 207.88/68.78 207.88/68.78 [7 0 7] [7 0 7] [7] 207.88/68.78 [take](x1, x2) = [7 7 7] x1 + [7 7 7] x2 + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 207.88/68.78 The order satisfies the following ordering constraints: 207.88/68.78 207.88/68.78 [U11(tt(), N, X, XS)] = [7 0 7] [7 0 7] [7 0 7] [15] 207.88/68.78 [7 7 7] N + [7 7 7] X + [7 7 7] XS + [15] 207.88/68.78 [7 7 7] [7 7 7] [7 7 7] [8] 207.88/68.78 >= [2 0 0] [1 0 0] [4 0 0] [15] 207.88/68.78 [2 0 0] N + [6 4 4] X + [3 2 0] XS + [11] 207.88/68.78 [2 0 0] [0 0 0] [4 4 4] [8] 207.88/68.78 = [U12(splitAt(activate(N), activate(XS)), activate(X))] 207.88/68.78 207.88/68.78 [U12(pair(YS, ZS), X)] = [1 0 0] [2 0 0] [2 0 0] [4] 207.88/68.78 [2 2 2] X + [1 1 1] YS + [1 1 0] ZS + [4] 207.88/68.78 [0 0 0] [0 2 2] [0 2 1] [8] 207.88/68.78 > [1 0 0] [0 0 0] [1 0 0] [1] 207.88/68.78 [2 2 2] X + [1 1 1] YS + [0 1 0] ZS + [2] 207.88/68.78 [0 0 0] [0 0 0] [0 0 1] [0] 207.88/68.78 = [pair(cons(activate(X), YS), ZS)] 207.88/68.78 207.88/68.78 [splitAt(0(), XS)] = [2 0 0] [9] 207.88/68.78 [0 1 0] XS + [8] 207.88/68.78 [0 0 2] [0] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] XS + [8] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [pair(nil(), XS)] 207.88/68.78 207.88/68.78 [activate(X)] = [1 0 0] [1] 207.88/68.78 [1 2 0] X + [0] 207.88/68.78 [1 0 2] [0] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] X + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [X] 207.88/68.78 207.88/68.78 [activate(n__natsFrom(X))] = [1 0 0] [1] 207.88/68.78 [3 2 2] X + [4] 207.88/68.78 [1 0 0] [2] 207.88/68.78 >= [1 0 0] [1] 207.88/68.78 [3 2 2] X + [4] 207.88/68.78 [1 0 0] [2] 207.88/68.78 = [natsFrom(activate(X))] 207.88/68.78 207.88/68.78 [activate(n__s(X))] = [1 0 0] [1] 207.88/68.78 [1 0 0] X + [0] 207.88/68.78 [1 0 0] [0] 207.88/68.78 >= [1 0 0] [1] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 = [s(activate(X))] 207.88/68.78 207.88/68.78 [afterNth(N, XS)] = [4 0 0] [4 0 0] [4] 207.88/68.78 [1 0 0] N + [0 1 0] XS + [2] 207.88/68.78 [0 0 0] [4 0 4] [0] 207.88/68.78 > [1 0 0] [2 0 0] [2] 207.88/68.78 [1 0 0] N + [0 1 0] XS + [1] 207.88/68.78 [0 0 0] [0 0 4] [0] 207.88/68.78 = [snd(splitAt(N, XS))] 207.88/68.78 207.88/68.78 [snd(pair(X, Y))] = [1 0 0] [1 0 0] [0] 207.88/68.78 [0 1 1] X + [0 1 0] Y + [2] 207.88/68.78 [0 0 0] [0 0 2] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [0 1 0] Y + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [Y] 207.88/68.78 207.88/68.78 [and(tt(), X)] = [7 0 7] [7] 207.88/68.78 [7 7 7] X + [7] 207.88/68.78 [7 7 7] [7] 207.88/68.78 > [1 0 0] [1] 207.88/68.78 [1 2 0] X + [0] 207.88/68.78 [1 0 2] [0] 207.88/68.78 = [activate(X)] 207.88/68.78 207.88/68.78 [fst(pair(X, Y))] = [2 0 0] [2 0 0] [3] 207.88/68.78 [0 1 1] X + [0 1 0] Y + [6] 207.88/68.78 [0 4 4] [0 4 0] [11] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] X + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [X] 207.88/68.78 207.88/68.78 [head(cons(N, XS))] = [1 0 0] [0 0 0] [3] 207.88/68.78 [0 2 2] N + [0 2 2] XS + [3] 207.88/68.78 [0 1 1] [0 1 1] [5] 207.88/68.78 > [1 0 0] [0] 207.88/68.78 [0 1 0] N + [0] 207.88/68.78 [0 0 1] [0] 207.88/68.78 = [N] 207.88/68.78 207.88/68.78 [natsFrom(N)] = [1 0 0] [0] 207.88/68.78 [1 1 1] N + [3] 207.88/68.78 [1 0 0] [1] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [1 1 1] N + [3] 207.88/68.78 [1 0 0] [0] 207.88/68.78 = [cons(N, n__natsFrom(n__s(N)))] 207.88/68.78 207.88/68.78 [natsFrom(X)] = [1 0 0] [0] 207.88/68.78 [1 1 1] X + [3] 207.88/68.78 [1 0 0] [1] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [1 1 1] X + [2] 207.88/68.78 [0 0 0] [1] 207.88/68.78 = [n__natsFrom(X)] 207.88/68.78 207.88/68.78 [sel(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.78 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 >= [4 0 0] [4 0 0] [7] 207.88/68.78 [2 0 0] N + [0 2 0] XS + [7] 207.88/68.78 [1 0 0] [0 1 0] [7] 207.88/68.78 = [head(afterNth(N, XS))] 207.88/68.78 207.88/68.78 [s(X)] = [1 0 0] [0] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 >= [1 0 0] [0] 207.88/68.78 [0 0 0] X + [0] 207.88/68.78 [0 0 0] [0] 207.88/68.78 = [n__s(X)] 207.88/68.78 207.88/68.78 [tail(cons(N, XS))] = [0 0 0] [1 0 0] [7] 207.88/68.78 [0 4 4] N + [1 4 4] XS + [7] 207.88/68.78 [0 2 2] [1 2 2] [7] 207.88/68.78 > [1 0 0] [1] 207.88/68.78 [1 2 0] XS + [0] 207.88/68.78 [1 0 2] [0] 207.88/68.78 = [activate(XS)] 207.88/68.78 207.88/68.78 [take(N, XS)] = [7 0 7] [7 0 7] [7] 207.88/68.78 [7 7 7] N + [7 7 7] XS + [7] 207.88/68.78 [7 7 7] [7 7 7] [7] 207.88/68.78 >= [2 0 0] [4 0 0] [7] 207.88/68.78 [1 0 0] N + [0 1 0] XS + [5] 207.88/68.78 [4 0 0] [0 4 0] [7] 207.88/68.78 = [fst(splitAt(N, XS))] 207.88/68.78 207.88/68.78 207.88/68.78 We return to the main proof. 207.88/68.78 207.88/68.78 We are left with following problem, upon which TcT provides the 207.88/68.78 certificate YES(O(1),O(1)). 207.88/68.78 207.88/68.78 Weak Trs: 207.88/68.78 { U11(tt(), N, X, XS) -> 207.88/68.78 U12(splitAt(activate(N), activate(XS)), activate(X)) 207.88/68.78 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 207.88/68.78 , splitAt(0(), XS) -> pair(nil(), XS) 207.88/68.78 , activate(X) -> X 207.88/68.78 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 207.88/68.78 , activate(n__s(X)) -> s(activate(X)) 207.88/68.78 , afterNth(N, XS) -> snd(splitAt(N, XS)) 207.88/68.78 , snd(pair(X, Y)) -> Y 207.88/68.78 , and(tt(), X) -> activate(X) 207.88/68.78 , fst(pair(X, Y)) -> X 207.88/68.78 , head(cons(N, XS)) -> N 207.88/68.78 , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) 207.88/68.78 , natsFrom(X) -> n__natsFrom(X) 207.88/68.78 , sel(N, XS) -> head(afterNth(N, XS)) 207.88/68.78 , s(X) -> n__s(X) 207.88/68.78 , tail(cons(N, XS)) -> activate(XS) 207.88/68.78 , take(N, XS) -> fst(splitAt(N, XS)) } 207.88/68.78 Obligation: 207.88/68.78 innermost runtime complexity 207.88/68.78 Answer: 207.88/68.78 YES(O(1),O(1)) 207.88/68.78 207.88/68.78 Empty rules are trivially bounded 207.88/68.78 207.88/68.78 Hurray, we answered YES(O(1),O(n^1)) 208.18/68.98 EOF