YES
Termination Proof using AProVETerm Rewriting System R:
[N, XS, X, Y, YS, ZS]
U11(tt, N, XS) -> U12(tt, N, XS)
U12(tt, N, XS) -> snd(splitAt(N, XS))
U21(tt, X) -> U22(tt, X)
U22(tt, X) -> X
U31(tt, N) -> U32(tt, N)
U32(tt, N) -> N
U41(tt, N, XS) -> U42(tt, N, XS)
U42(tt, N, XS) -> head(afterNth(N, XS))
U51(tt, Y) -> U52(tt, Y)
U52(tt, Y) -> Y
U61(tt, N, X, XS) -> U62(tt, N, X, XS)
U62(tt, N, X, XS) -> U63(tt, N, X, XS)
U63(tt, N, X, XS) -> U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
U71(tt, XS) -> U72(tt, XS)
U72(tt, XS) -> XS
U81(tt, N, XS) -> U82(tt, N, XS)
U82(tt, N, XS) -> fst(splitAt(N, XS))
afterNth(N, XS) -> U11(tt, N, XS)
fst(pair(X, Y)) -> U21(tt, X)
head(cons(N, XS)) -> U31(tt, N)
natsFrom(N) -> cons(N, natsFrom(s(N)))
sel(N, XS) -> U41(tt, N, XS)
snd(pair(X, Y)) -> U51(tt, Y)
splitAt(0, XS) -> pair(nil, XS)
splitAt(s(N), cons(X, XS)) -> U61(tt, N, X, XS)
tail(cons(N, XS)) -> U71(tt, XS)
take(N, XS) -> U81(tt, N, XS)
Termination of R to be shown.
R
↳Orthogonal Check
This CSR is orthogonal, so it is sufficient to show innermost termination.
R
↳OrthoCSR
→TRS1
↳CSR to TRS Transformation
Zantema-Transformation successful.
Replacement map:
U71(1, 2)
splitAt(1, 2)
U42(1, 2, 3)
take(1, 2)
tail(1)
U52(1, 2)
U63(1, 2, 3, 4)
U11(1, 2, 3)
U51(1, 2)
U62(1, 2, 3, 4)
afterNth(1, 2)
cons(1, 2)
pair(1, 2)
U21(1, 2)
U72(1, 2)
head(1)
U64(1, 2)
U82(1, 2, 3)
natsFrom(1)
U31(1, 2)
U12(1, 2, 3)
sel(1, 2)
U22(1, 2)
U81(1, 2, 3)
U41(1, 2, 3)
U32(1, 2)
snd(1)
fst(1)
s(1)
U61(1, 2, 3, 4)
Old CSR:
U11(tt, N, XS) -> U12(tt, N, XS)
U12(tt, N, XS) -> snd(splitAt(N, XS))
U21(tt, X) -> U22(tt, X)
U22(tt, X) -> X
U31(tt, N) -> U32(tt, N)
U32(tt, N) -> N
U41(tt, N, XS) -> U42(tt, N, XS)
U42(tt, N, XS) -> head(afterNth(N, XS))
U51(tt, Y) -> U52(tt, Y)
U52(tt, Y) -> Y
U61(tt, N, X, XS) -> U62(tt, N, X, XS)
U62(tt, N, X, XS) -> U63(tt, N, X, XS)
U63(tt, N, X, XS) -> U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
U71(tt, XS) -> U72(tt, XS)
U72(tt, XS) -> XS
U81(tt, N, XS) -> U82(tt, N, XS)
U82(tt, N, XS) -> fst(splitAt(N, XS))
afterNth(N, XS) -> U11(tt, N, XS)
fst(pair(X, Y)) -> U21(tt, X)
head(cons(N, XS)) -> U31(tt, N)
natsFrom(N) -> cons(N, natsFrom(s(N)))
sel(N, XS) -> U41(tt, N, XS)
snd(pair(X, Y)) -> U51(tt, Y)
splitAt(0, XS) -> pair(nil, XS)
splitAt(s(N), cons(X, XS)) -> U61(tt, N, X, XS)
tail(cons(N, XS)) -> U71(tt, XS)
take(N, XS) -> U81(tt, N, XS)
new TRS:
U11(tt, N, XS) -> U12(tt, a(N), a(XS))
U12(tt, N, XS) -> snd(splitAt(a(N), a(XS)))
a(natsFrom(x0)) -> natsFrom(x0)
snd(pair(X, Y)) -> U51(tt, Y)
splitAt(0, XS) -> pair(nil, XS)
splitAt(s(N), cons(X, XS)) -> U61(tt, N, X, a(XS))
U21(tt, X) -> U22(tt, a(X))
U22(tt, X) -> a(X)
U31(tt, N) -> U32(tt, a(N))
U32(tt, N) -> a(N)
U41(tt, N, XS) -> U42(tt, a(N), a(XS))
U42(tt, N, XS) -> head(afterNth(a(N), a(XS)))
head(cons(N, XS)) -> U31(tt, N)
afterNth(N, XS) -> U11(tt, N, XS)
U51(tt, Y) -> U52(tt, a(Y))
U52(tt, Y) -> a(Y)
U61(tt, N, X, XS) -> U62(tt, a(N), a(X), a(XS))
U62(tt, N, X, XS) -> U63(tt, a(N), a(X), a(XS))
U63(tt, N, X, XS) -> U64(splitAt(a(N), a(XS)), a(X))
U64(pair(YS, ZS), X) -> pair(cons(a(X), YS), ZS)
U71(tt, XS) -> U72(tt, a(XS))
U72(tt, XS) -> a(XS)
U81(tt, N, XS) -> U82(tt, a(N), a(XS))
U82(tt, N, XS) -> fst(splitAt(a(N), a(XS)))
fst(pair(X, Y)) -> U21(tt, X)
natsFrom(N) -> cons(N, natsFrom(s(N)))
natsFrom(x0) -> natsFrom(x0)
sel(N, XS) -> U41(tt, N, XS)
tail(cons(N, XS)) -> U71(tt, a(XS))
take(N, XS) -> U81(tt, N, XS)
R
↳OrthoCSR
→TRS1
↳CSRtoTRS
→TRS2
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
U11'(tt, N, XS) -> U12'(tt, a(N), a(XS))
U11'(tt, N, XS) -> A(N)
U11'(tt, N, XS) -> A(XS)
U12'(tt, N, XS) -> SND(splitAt(a(N), a(XS)))
U12'(tt, N, XS) -> SPLITAT(a(N), a(XS))
U12'(tt, N, XS) -> A(N)
U12'(tt, N, XS) -> A(XS)
A(natsFrom(x0)) -> NATSFROM(x0)
SND(pair(X, Y)) -> U51'(tt, Y)
SPLITAT(s(N), cons(X, XS)) -> U61'(tt, N, X, a(XS))
SPLITAT(s(N), cons(X, XS)) -> A(XS)
U21'(tt, X) -> U22'(tt, a(X))
U21'(tt, X) -> A(X)
U22'(tt, X) -> A(X)
U31'(tt, N) -> U32'(tt, a(N))
U31'(tt, N) -> A(N)
U32'(tt, N) -> A(N)
U41'(tt, N, XS) -> U42'(tt, a(N), a(XS))
U41'(tt, N, XS) -> A(N)
U41'(tt, N, XS) -> A(XS)
U42'(tt, N, XS) -> HEAD(afterNth(a(N), a(XS)))
U42'(tt, N, XS) -> AFTERNTH(a(N), a(XS))
U42'(tt, N, XS) -> A(N)
U42'(tt, N, XS) -> A(XS)
HEAD(cons(N, XS)) -> U31'(tt, N)
AFTERNTH(N, XS) -> U11'(tt, N, XS)
U51'(tt, Y) -> U52'(tt, a(Y))
U51'(tt, Y) -> A(Y)
U52'(tt, Y) -> A(Y)
U61'(tt, N, X, XS) -> U62'(tt, a(N), a(X), a(XS))
U61'(tt, N, X, XS) -> A(N)
U61'(tt, N, X, XS) -> A(X)
U61'(tt, N, X, XS) -> A(XS)
U62'(tt, N, X, XS) -> U63'(tt, a(N), a(X), a(XS))
U62'(tt, N, X, XS) -> A(N)
U62'(tt, N, X, XS) -> A(X)
U62'(tt, N, X, XS) -> A(XS)
U63'(tt, N, X, XS) -> U64'(splitAt(a(N), a(XS)), a(X))
U63'(tt, N, X, XS) -> SPLITAT(a(N), a(XS))
U63'(tt, N, X, XS) -> A(N)
U63'(tt, N, X, XS) -> A(XS)
U63'(tt, N, X, XS) -> A(X)
U64'(pair(YS, ZS), X) -> A(X)
U71'(tt, XS) -> U72'(tt, a(XS))
U71'(tt, XS) -> A(XS)
U72'(tt, XS) -> A(XS)
U81'(tt, N, XS) -> U82'(tt, a(N), a(XS))
U81'(tt, N, XS) -> A(N)
U81'(tt, N, XS) -> A(XS)
U82'(tt, N, XS) -> FST(splitAt(a(N), a(XS)))
U82'(tt, N, XS) -> SPLITAT(a(N), a(XS))
U82'(tt, N, XS) -> A(N)
U82'(tt, N, XS) -> A(XS)
FST(pair(X, Y)) -> U21'(tt, X)
SEL(N, XS) -> U41'(tt, N, XS)
TAIL(cons(N, XS)) -> U71'(tt, a(XS))
TAIL(cons(N, XS)) -> A(XS)
TAKE(N, XS) -> U81'(tt, N, XS)
R contains no SCCs.
Termination of R successfully shown.
Duration:
0:52 minutes