We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, U21(tt(), X) -> U22(tt(), activate(X))
, U22(tt(), X) -> activate(X)
, U31(tt(), N) -> U32(tt(), activate(N))
, U32(tt(), N) -> activate(N)
, U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS))
, U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
, head(cons(N, XS)) -> U31(tt(), N)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, U61(tt(), N, X, XS) ->
U62(tt(), activate(N), activate(X), activate(XS))
, U62(tt(), N, X, XS) ->
U63(tt(), activate(N), activate(X), activate(XS))
, U63(tt(), N, X, XS) ->
U64(splitAt(activate(N), activate(XS)), activate(X))
, U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
, U71(tt(), XS) -> U72(tt(), activate(XS))
, U72(tt(), XS) -> activate(XS)
, U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS))
, U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
, fst(pair(X, Y)) -> U21(tt(), X)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, s(X) -> n__s(X)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
Arguments of following rules are not normal-forms:
{ splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) }
All above mentioned rules can be savely removed.
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, U21(tt(), X) -> U22(tt(), activate(X))
, U22(tt(), X) -> activate(X)
, U31(tt(), N) -> U32(tt(), activate(N))
, U32(tt(), N) -> activate(N)
, U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS))
, U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
, head(cons(N, XS)) -> U31(tt(), N)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, U61(tt(), N, X, XS) ->
U62(tt(), activate(N), activate(X), activate(XS))
, U62(tt(), N, X, XS) ->
U63(tt(), activate(N), activate(X), activate(XS))
, U63(tt(), N, X, XS) ->
U64(splitAt(activate(N), activate(XS)), activate(X))
, U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
, U71(tt(), XS) -> U72(tt(), activate(XS))
, U72(tt(), XS) -> activate(XS)
, U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS))
, U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
, fst(pair(X, Y)) -> U21(tt(), X)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, s(X) -> n__s(X)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order
(PS)' as induced by the safe mapping
safe(U11) = {}, safe(tt) = {}, safe(U12) = {}, safe(activate) = {},
safe(snd) = {}, safe(splitAt) = {2}, safe(U21) = {1},
safe(U22) = {}, safe(U31) = {1}, safe(U32) = {}, safe(U41) = {},
safe(U42) = {}, safe(head) = {}, safe(afterNth) = {},
safe(U51) = {1}, safe(U52) = {}, safe(U61) = {}, safe(U62) = {},
safe(U63) = {1}, safe(U64) = {}, safe(pair) = {1, 2},
safe(cons) = {1, 2}, safe(U71) = {1}, safe(U72) = {},
safe(U81) = {}, safe(U82) = {}, safe(fst) = {},
safe(natsFrom) = {1}, safe(n__natsFrom) = {1}, safe(n__s) = {1},
safe(sel) = {}, safe(0) = {}, safe(nil) = {}, safe(s) = {1},
safe(tail) = {}, safe(take) = {}
and precedence
U11 > U12, U11 > activate, U12 > activate, U12 > snd,
U12 > splitAt, activate > natsFrom, activate > s, snd > U51,
U21 > activate, U21 > U22, U22 > activate, U31 > activate,
U31 > U32, U32 > activate, U41 > activate, U41 > U42,
U42 > activate, U42 > head, U42 > afterNth, head > U31,
afterNth > U11, U51 > activate, U51 > U52, U52 > activate,
U61 > activate, U61 > U62, U62 > activate, U62 > U63,
U63 > activate, U63 > splitAt, U63 > U64, U71 > activate,
U71 > U72, U72 > activate, U81 > activate, U81 > U82,
U82 > activate, U82 > splitAt, U82 > fst, fst > U21, sel > U41,
tail > activate, tail > U71, take > U81, activate ~ U64 .
Following symbols are considered recursive:
{U11, activate, snd, U21, U22, U31, U32, U42, head, afterNth, U51,
U52, U62, U64, U72, fst, natsFrom, sel, s, tail, take}
The recursion depth is 9.
For your convenience, here are the satisfied ordering constraints:
U11(tt(), N, XS;) > U12(tt(), activate(N;), activate(XS;);)
U12(tt(), N, XS;) > snd(splitAt(activate(N;); activate(XS;));)
activate(X;) > X
activate(n__natsFrom(; X);) > natsFrom(; activate(X;))
activate(n__s(; X);) > s(; activate(X;))
snd(pair(; X, Y);) > U51(Y; tt())
splitAt(0(); XS) > pair(; nil(), XS)
U21(X; tt()) > U22(tt(), activate(X;);)
U22(tt(), X;) > activate(X;)
U31(N; tt()) > U32(tt(), activate(N;);)
U32(tt(), N;) > activate(N;)
U41(tt(), N, XS;) > U42(tt(), activate(N;), activate(XS;);)
U42(tt(), N, XS;) > head(afterNth(activate(N;), activate(XS;););)
head(cons(; N, XS);) > U31(N; tt())
afterNth(N, XS;) > U11(tt(), N, XS;)
U51(Y; tt()) > U52(tt(), activate(Y;);)
U52(tt(), Y;) > activate(Y;)
U61(tt(), N, X, XS;) > U62(tt(), activate(N;), activate(X;), activate(XS;);)
U62(tt(), N, X, XS;) > U63(activate(N;), activate(X;), activate(XS;); tt())
U63(N, X, XS; tt()) > U64(splitAt(activate(N;); activate(XS;)), activate(X;);)
U64(pair(; YS, ZS), X;) > pair(; cons(; activate(X;), YS), ZS)
U71(XS; tt()) > U72(tt(), activate(XS;);)
U72(tt(), XS;) > activate(XS;)
U81(tt(), N, XS;) > U82(tt(), activate(N;), activate(XS;);)
U82(tt(), N, XS;) > fst(splitAt(activate(N;); activate(XS;));)
fst(pair(; X, Y);) > U21(X; tt())
natsFrom(; N) > cons(; N, n__natsFrom(; n__s(; N)))
natsFrom(; X) > n__natsFrom(; X)
sel(N, XS;) > U41(tt(), N, XS;)
s(; X) > n__s(; X)
tail(cons(; N, XS);) > U71(activate(XS;); tt())
take(N, XS;) > U81(tt(), N, XS;)
Hurray, we answered YES(?,POLY)