Termination w.r.t. Q proof of /tmp/tmphUQYfI/LISTUTILITIES_nokinds_noand

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS

↳1 QTRSToCSRProof (⇔)

↳2 CSR

↳3 CSDependencyPairsProof (⇔)

↳4 QCSDP

↳5 QCSDependencyGraphProof (⇔)

↳6 AND

  ↳7 QCSDP

    ↳8 QCSUsableRulesProof (⇔)

    ↳9 QCSDP

    ↳10 QCSDPMuMonotonicPoloProof (⇔)

    ↳11 QCSDP

    ↳12 QCSDependencyGraphProof (⇔)

    ↳13 TRUE

  ↳14 QCSDP

    ↳15 QCSDPSubtermProof (⇔)

    ↳16 QCSDP

    ↳17 QCSDependencyGraphProof (⇔)

    ↳18 TRUE

  ↳19 QCSDP

    ↳20 QCSDPSubtermProof (⇔)

    ↳21 QCSDP

    ↳22 QCSDependencyGraphProof (⇔)

    ↳23 TRUE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(U101(tt, V2)) → mark(U102(isLNat(V2)))
active(U102(tt)) → mark(tt)
active(U11(tt, N, XS)) → mark(U12(isLNat(XS), N, XS))
active(U111(tt)) → mark(tt)
active(U12(tt, N, XS)) → mark(snd(splitAt(N, XS)))
active(U121(tt)) → mark(tt)
active(U131(tt, V2)) → mark(U132(isLNat(V2)))
active(U132(tt)) → mark(tt)
active(U141(tt, V2)) → mark(U142(isLNat(V2)))
active(U142(tt)) → mark(tt)
active(U151(tt, V2)) → mark(U152(isLNat(V2)))
active(U152(tt)) → mark(tt)
active(U161(tt, N)) → mark(cons(N, natsFrom(s(N))))
active(U171(tt, N, XS)) → mark(U172(isLNat(XS), N, XS))
active(U172(tt, N, XS)) → mark(head(afterNth(N, XS)))
active(U181(tt, Y)) → mark(U182(isLNat(Y), Y))
active(U182(tt, Y)) → mark(Y)
active(U191(tt, XS)) → mark(pair(nil, XS))
active(U201(tt, N, X, XS)) → mark(U202(isNatural(X), N, X, XS))
active(U202(tt, N, X, XS)) → mark(U203(isLNat(XS), N, X, XS))
active(U203(tt, N, X, XS)) → mark(U204(splitAt(N, XS), X))
active(U204(pair(YS, ZS), X)) → mark(pair(cons(X, YS), ZS))
active(U21(tt, X, Y)) → mark(U22(isLNat(Y), X))
active(U211(tt, XS)) → mark(U212(isLNat(XS), XS))
active(U212(tt, XS)) → mark(XS)
active(U22(tt, X)) → mark(X)
active(U221(tt, N, XS)) → mark(U222(isLNat(XS), N, XS))
active(U222(tt, N, XS)) → mark(fst(splitAt(N, XS)))
active(U31(tt, N, XS)) → mark(U32(isLNat(XS), N))
active(U32(tt, N)) → mark(N)
active(U41(tt, V2)) → mark(U42(isLNat(V2)))
active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isLNat(V2)))
active(U52(tt)) → mark(tt)
active(U61(tt)) → mark(tt)
active(U71(tt)) → mark(tt)
active(U81(tt)) → mark(tt)
active(U91(tt)) → mark(tt)
active(afterNth(N, XS)) → mark(U11(isNatural(N), N, XS))
active(fst(pair(X, Y))) → mark(U21(isLNat(X), X, Y))
active(head(cons(N, XS))) → mark(U31(isNatural(N), N, XS))
active(isLNat(nil)) → mark(tt)
active(isLNat(afterNth(V1, V2))) → mark(U41(isNatural(V1), V2))
active(isLNat(cons(V1, V2))) → mark(U51(isNatural(V1), V2))
active(isLNat(fst(V1))) → mark(U61(isPLNat(V1)))
active(isLNat(natsFrom(V1))) → mark(U71(isNatural(V1)))
active(isLNat(snd(V1))) → mark(U81(isPLNat(V1)))
active(isLNat(tail(V1))) → mark(U91(isLNat(V1)))
active(isLNat(take(V1, V2))) → mark(U101(isNatural(V1), V2))
active(isNatural(0)) → mark(tt)
active(isNatural(head(V1))) → mark(U111(isLNat(V1)))
active(isNatural(s(V1))) → mark(U121(isNatural(V1)))
active(isNatural(sel(V1, V2))) → mark(U131(isNatural(V1), V2))
active(isPLNat(pair(V1, V2))) → mark(U141(isLNat(V1), V2))
active(isPLNat(splitAt(V1, V2))) → mark(U151(isNatural(V1), V2))
active(natsFrom(N)) → mark(U161(isNatural(N), N))
active(sel(N, XS)) → mark(U171(isNatural(N), N, XS))
active(snd(pair(X, Y))) → mark(U181(isLNat(X), Y))
active(splitAt(0, XS)) → mark(U191(isLNat(XS), XS))
active(splitAt(s(N), cons(X, XS))) → mark(U201(isNatural(N), N, X, XS))
active(tail(cons(N, XS))) → mark(U211(isNatural(N), XS))
active(take(N, XS)) → mark(U221(isNatural(N), N, XS))
active(U101(X1, X2)) → U101(active(X1), X2)
active(U102(X)) → U102(active(X))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(U111(X)) → U111(active(X))
active(snd(X)) → snd(active(X))
active(splitAt(X1, X2)) → splitAt(active(X1), X2)
active(splitAt(X1, X2)) → splitAt(X1, active(X2))
active(U121(X)) → U121(active(X))
active(U131(X1, X2)) → U131(active(X1), X2)
active(U132(X)) → U132(active(X))
active(U141(X1, X2)) → U141(active(X1), X2)
active(U142(X)) → U142(active(X))
active(U151(X1, X2)) → U151(active(X1), X2)
active(U152(X)) → U152(active(X))
active(U161(X1, X2)) → U161(active(X1), X2)
active(cons(X1, X2)) → cons(active(X1), X2)
active(natsFrom(X)) → natsFrom(active(X))
active(s(X)) → s(active(X))
active(U171(X1, X2, X3)) → U171(active(X1), X2, X3)
active(U172(X1, X2, X3)) → U172(active(X1), X2, X3)
active(head(X)) → head(active(X))
active(afterNth(X1, X2)) → afterNth(active(X1), X2)
active(afterNth(X1, X2)) → afterNth(X1, active(X2))
active(U181(X1, X2)) → U181(active(X1), X2)
active(U182(X1, X2)) → U182(active(X1), X2)
active(U191(X1, X2)) → U191(active(X1), X2)
active(pair(X1, X2)) → pair(active(X1), X2)
active(pair(X1, X2)) → pair(X1, active(X2))
active(U201(X1, X2, X3, X4)) → U201(active(X1), X2, X3, X4)
active(U202(X1, X2, X3, X4)) → U202(active(X1), X2, X3, X4)
active(U203(X1, X2, X3, X4)) → U203(active(X1), X2, X3, X4)
active(U204(X1, X2)) → U204(active(X1), X2)
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2)) → U22(active(X1), X2)
active(U211(X1, X2)) → U211(active(X1), X2)
active(U212(X1, X2)) → U212(active(X1), X2)
active(U221(X1, X2, X3)) → U221(active(X1), X2, X3)
active(U222(X1, X2, X3)) → U222(active(X1), X2, X3)
active(fst(X)) → fst(active(X))
active(U31(X1, X2, X3)) → U31(active(X1), X2, X3)
active(U32(X1, X2)) → U32(active(X1), X2)
active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))
active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))
active(U61(X)) → U61(active(X))
active(U71(X)) → U71(active(X))
active(U81(X)) → U81(active(X))
active(U91(X)) → U91(active(X))
active(tail(X)) → tail(active(X))
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
U101(mark(X1), X2) → mark(U101(X1, X2))
U102(mark(X)) → mark(U102(X))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
U111(mark(X)) → mark(U111(X))
snd(mark(X)) → mark(snd(X))
splitAt(mark(X1), X2) → mark(splitAt(X1, X2))
splitAt(X1, mark(X2)) → mark(splitAt(X1, X2))
U121(mark(X)) → mark(U121(X))
U131(mark(X1), X2) → mark(U131(X1, X2))
U132(mark(X)) → mark(U132(X))
U141(mark(X1), X2) → mark(U141(X1, X2))
U142(mark(X)) → mark(U142(X))
U151(mark(X1), X2) → mark(U151(X1, X2))
U152(mark(X)) → mark(U152(X))
U161(mark(X1), X2) → mark(U161(X1, X2))
cons(mark(X1), X2) → mark(cons(X1, X2))
natsFrom(mark(X)) → mark(natsFrom(X))
s(mark(X)) → mark(s(X))
U171(mark(X1), X2, X3) → mark(U171(X1, X2, X3))
U172(mark(X1), X2, X3) → mark(U172(X1, X2, X3))
head(mark(X)) → mark(head(X))
afterNth(mark(X1), X2) → mark(afterNth(X1, X2))
afterNth(X1, mark(X2)) → mark(afterNth(X1, X2))
U181(mark(X1), X2) → mark(U181(X1, X2))
U182(mark(X1), X2) → mark(U182(X1, X2))
U191(mark(X1), X2) → mark(U191(X1, X2))
pair(mark(X1), X2) → mark(pair(X1, X2))
pair(X1, mark(X2)) → mark(pair(X1, X2))
U201(mark(X1), X2, X3, X4) → mark(U201(X1, X2, X3, X4))
U202(mark(X1), X2, X3, X4) → mark(U202(X1, X2, X3, X4))
U203(mark(X1), X2, X3, X4) → mark(U203(X1, X2, X3, X4))
U204(mark(X1), X2) → mark(U204(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2) → mark(U22(X1, X2))
U211(mark(X1), X2) → mark(U211(X1, X2))
U212(mark(X1), X2) → mark(U212(X1, X2))
U221(mark(X1), X2, X3) → mark(U221(X1, X2, X3))
U222(mark(X1), X2, X3) → mark(U222(X1, X2, X3))
fst(mark(X)) → mark(fst(X))
U31(mark(X1), X2, X3) → mark(U31(X1, X2, X3))
U32(mark(X1), X2) → mark(U32(X1, X2))
U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))
U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))
U61(mark(X)) → mark(U61(X))
U71(mark(X)) → mark(U71(X))
U81(mark(X)) → mark(U81(X))
U91(mark(X)) → mark(U91(X))
tail(mark(X)) → mark(tail(X))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
proper(U101(X1, X2)) → U101(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(U102(X)) → U102(proper(X))
proper(isLNat(X)) → isLNat(proper(X))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(U111(X)) → U111(proper(X))
proper(snd(X)) → snd(proper(X))
proper(splitAt(X1, X2)) → splitAt(proper(X1), proper(X2))
proper(U121(X)) → U121(proper(X))
proper(U131(X1, X2)) → U131(proper(X1), proper(X2))
proper(U132(X)) → U132(proper(X))
proper(U141(X1, X2)) → U141(proper(X1), proper(X2))
proper(U142(X)) → U142(proper(X))
proper(U151(X1, X2)) → U151(proper(X1), proper(X2))
proper(U152(X)) → U152(proper(X))
proper(U161(X1, X2)) → U161(proper(X1), proper(X2))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(natsFrom(X)) → natsFrom(proper(X))
proper(s(X)) → s(proper(X))
proper(U171(X1, X2, X3)) → U171(proper(X1), proper(X2), proper(X3))
proper(U172(X1, X2, X3)) → U172(proper(X1), proper(X2), proper(X3))
proper(head(X)) → head(proper(X))
proper(afterNth(X1, X2)) → afterNth(proper(X1), proper(X2))
proper(U181(X1, X2)) → U181(proper(X1), proper(X2))
proper(U182(X1, X2)) → U182(proper(X1), proper(X2))
proper(U191(X1, X2)) → U191(proper(X1), proper(X2))
proper(pair(X1, X2)) → pair(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(U201(X1, X2, X3, X4)) → U201(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U202(X1, X2, X3, X4)) → U202(proper(X1), proper(X2), proper(X3), proper(X4))
proper(isNatural(X)) → isNatural(proper(X))
proper(U203(X1, X2, X3, X4)) → U203(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U204(X1, X2)) → U204(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2)) → U22(proper(X1), proper(X2))
proper(U211(X1, X2)) → U211(proper(X1), proper(X2))
proper(U212(X1, X2)) → U212(proper(X1), proper(X2))
proper(U221(X1, X2, X3)) → U221(proper(X1), proper(X2), proper(X3))
proper(U222(X1, X2, X3)) → U222(proper(X1), proper(X2), proper(X3))
proper(fst(X)) → fst(proper(X))
proper(U31(X1, X2, X3)) → U31(proper(X1), proper(X2), proper(X3))
proper(U32(X1, X2)) → U32(proper(X1), proper(X2))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))
proper(U42(X)) → U42(proper(X))
proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))
proper(U61(X)) → U61(proper(X))
proper(U71(X)) → U71(proper(X))
proper(U81(X)) → U81(proper(X))
proper(U91(X)) → U91(proper(X))
proper(isPLNat(X)) → isPLNat(proper(X))
proper(tail(X)) → tail(proper(X))
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(0) → ok(0)
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
U101(ok(X1), ok(X2)) → ok(U101(X1, X2))
U102(ok(X)) → ok(U102(X))
isLNat(ok(X)) → ok(isLNat(X))
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
U111(ok(X)) → ok(U111(X))
snd(ok(X)) → ok(snd(X))
splitAt(ok(X1), ok(X2)) → ok(splitAt(X1, X2))
U121(ok(X)) → ok(U121(X))
U131(ok(X1), ok(X2)) → ok(U131(X1, X2))
U132(ok(X)) → ok(U132(X))
U141(ok(X1), ok(X2)) → ok(U141(X1, X2))
U142(ok(X)) → ok(U142(X))
U151(ok(X1), ok(X2)) → ok(U151(X1, X2))
U152(ok(X)) → ok(U152(X))
U161(ok(X1), ok(X2)) → ok(U161(X1, X2))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
natsFrom(ok(X)) → ok(natsFrom(X))
s(ok(X)) → ok(s(X))
U171(ok(X1), ok(X2), ok(X3)) → ok(U171(X1, X2, X3))
U172(ok(X1), ok(X2), ok(X3)) → ok(U172(X1, X2, X3))
head(ok(X)) → ok(head(X))
afterNth(ok(X1), ok(X2)) → ok(afterNth(X1, X2))
U181(ok(X1), ok(X2)) → ok(U181(X1, X2))
U182(ok(X1), ok(X2)) → ok(U182(X1, X2))
U191(ok(X1), ok(X2)) → ok(U191(X1, X2))
pair(ok(X1), ok(X2)) → ok(pair(X1, X2))
U201(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U201(X1, X2, X3, X4))
U202(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U202(X1, X2, X3, X4))
isNatural(ok(X)) → ok(isNatural(X))
U203(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U203(X1, X2, X3, X4))
U204(ok(X1), ok(X2)) → ok(U204(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2)) → ok(U22(X1, X2))
U211(ok(X1), ok(X2)) → ok(U211(X1, X2))
U212(ok(X1), ok(X2)) → ok(U212(X1, X2))
U221(ok(X1), ok(X2), ok(X3)) → ok(U221(X1, X2, X3))
U222(ok(X1), ok(X2), ok(X3)) → ok(U222(X1, X2, X3))
fst(ok(X)) → ok(fst(X))
U31(ok(X1), ok(X2), ok(X3)) → ok(U31(X1, X2, X3))
U32(ok(X1), ok(X2)) → ok(U32(X1, X2))
U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))
U52(ok(X)) → ok(U52(X))
U61(ok(X)) → ok(U61(X))
U71(ok(X)) → ok(U71(X))
U81(ok(X)) → ok(U81(X))
U91(ok(X)) → ok(U91(X))
isPLNat(ok(X)) → ok(isPLNat(X))
tail(ok(X)) → ok(tail(X))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

(1) QTRSToCSRProof (EQUIVALENT transformation)

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

active(U101(tt, V2)) → mark(U102(isLNat(V2)))
active(U102(tt)) → mark(tt)
active(U11(tt, N, XS)) → mark(U12(isLNat(XS), N, XS))
active(U111(tt)) → mark(tt)
active(U12(tt, N, XS)) → mark(snd(splitAt(N, XS)))
active(U121(tt)) → mark(tt)
active(U131(tt, V2)) → mark(U132(isLNat(V2)))
active(U132(tt)) → mark(tt)
active(U141(tt, V2)) → mark(U142(isLNat(V2)))
active(U142(tt)) → mark(tt)
active(U151(tt, V2)) → mark(U152(isLNat(V2)))
active(U152(tt)) → mark(tt)
active(U161(tt, N)) → mark(cons(N, natsFrom(s(N))))
active(U171(tt, N, XS)) → mark(U172(isLNat(XS), N, XS))
active(U172(tt, N, XS)) → mark(head(afterNth(N, XS)))
active(U181(tt, Y)) → mark(U182(isLNat(Y), Y))
active(U182(tt, Y)) → mark(Y)
active(U191(tt, XS)) → mark(pair(nil, XS))
active(U201(tt, N, X, XS)) → mark(U202(isNatural(X), N, X, XS))
active(U202(tt, N, X, XS)) → mark(U203(isLNat(XS), N, X, XS))
active(U203(tt, N, X, XS)) → mark(U204(splitAt(N, XS), X))
active(U204(pair(YS, ZS), X)) → mark(pair(cons(X, YS), ZS))
active(U21(tt, X, Y)) → mark(U22(isLNat(Y), X))
active(U211(tt, XS)) → mark(U212(isLNat(XS), XS))
active(U212(tt, XS)) → mark(XS)
active(U22(tt, X)) → mark(X)
active(U221(tt, N, XS)) → mark(U222(isLNat(XS), N, XS))
active(U222(tt, N, XS)) → mark(fst(splitAt(N, XS)))
active(U31(tt, N, XS)) → mark(U32(isLNat(XS), N))
active(U32(tt, N)) → mark(N)
active(U41(tt, V2)) → mark(U42(isLNat(V2)))
active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isLNat(V2)))
active(U52(tt)) → mark(tt)
active(U61(tt)) → mark(tt)
active(U71(tt)) → mark(tt)
active(U81(tt)) → mark(tt)
active(U91(tt)) → mark(tt)
active(afterNth(N, XS)) → mark(U11(isNatural(N), N, XS))
active(fst(pair(X, Y))) → mark(U21(isLNat(X), X, Y))
active(head(cons(N, XS))) → mark(U31(isNatural(N), N, XS))
active(isLNat(nil)) → mark(tt)
active(isLNat(afterNth(V1, V2))) → mark(U41(isNatural(V1), V2))
active(isLNat(cons(V1, V2))) → mark(U51(isNatural(V1), V2))
active(isLNat(fst(V1))) → mark(U61(isPLNat(V1)))
active(isLNat(natsFrom(V1))) → mark(U71(isNatural(V1)))
active(isLNat(snd(V1))) → mark(U81(isPLNat(V1)))
active(isLNat(tail(V1))) → mark(U91(isLNat(V1)))
active(isLNat(take(V1, V2))) → mark(U101(isNatural(V1), V2))
active(isNatural(0)) → mark(tt)
active(isNatural(head(V1))) → mark(U111(isLNat(V1)))
active(isNatural(s(V1))) → mark(U121(isNatural(V1)))
active(isNatural(sel(V1, V2))) → mark(U131(isNatural(V1), V2))
active(isPLNat(pair(V1, V2))) → mark(U141(isLNat(V1), V2))
active(isPLNat(splitAt(V1, V2))) → mark(U151(isNatural(V1), V2))
active(natsFrom(N)) → mark(U161(isNatural(N), N))
active(sel(N, XS)) → mark(U171(isNatural(N), N, XS))
active(snd(pair(X, Y))) → mark(U181(isLNat(X), Y))
active(splitAt(0, XS)) → mark(U191(isLNat(XS), XS))
active(splitAt(s(N), cons(X, XS))) → mark(U201(isNatural(N), N, X, XS))
active(tail(cons(N, XS))) → mark(U211(isNatural(N), XS))
active(take(N, XS)) → mark(U221(isNatural(N), N, XS))
active(U101(X1, X2)) → U101(active(X1), X2)
active(U102(X)) → U102(active(X))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(U111(X)) → U111(active(X))
active(snd(X)) → snd(active(X))
active(splitAt(X1, X2)) → splitAt(active(X1), X2)
active(splitAt(X1, X2)) → splitAt(X1, active(X2))
active(U121(X)) → U121(active(X))
active(U131(X1, X2)) → U131(active(X1), X2)
active(U132(X)) → U132(active(X))
active(U141(X1, X2)) → U141(active(X1), X2)
active(U142(X)) → U142(active(X))
active(U151(X1, X2)) → U151(active(X1), X2)
active(U152(X)) → U152(active(X))
active(U161(X1, X2)) → U161(active(X1), X2)
active(cons(X1, X2)) → cons(active(X1), X2)
active(natsFrom(X)) → natsFrom(active(X))
active(s(X)) → s(active(X))
active(U171(X1, X2, X3)) → U171(active(X1), X2, X3)
active(U172(X1, X2, X3)) → U172(active(X1), X2, X3)
active(head(X)) → head(active(X))
active(afterNth(X1, X2)) → afterNth(active(X1), X2)
active(afterNth(X1, X2)) → afterNth(X1, active(X2))
active(U181(X1, X2)) → U181(active(X1), X2)
active(U182(X1, X2)) → U182(active(X1), X2)
active(U191(X1, X2)) → U191(active(X1), X2)
active(pair(X1, X2)) → pair(active(X1), X2)
active(pair(X1, X2)) → pair(X1, active(X2))
active(U201(X1, X2, X3, X4)) → U201(active(X1), X2, X3, X4)
active(U202(X1, X2, X3, X4)) → U202(active(X1), X2, X3, X4)
active(U203(X1, X2, X3, X4)) → U203(active(X1), X2, X3, X4)
active(U204(X1, X2)) → U204(active(X1), X2)
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2)) → U22(active(X1), X2)
active(U211(X1, X2)) → U211(active(X1), X2)
active(U212(X1, X2)) → U212(active(X1), X2)
active(U221(X1, X2, X3)) → U221(active(X1), X2, X3)
active(U222(X1, X2, X3)) → U222(active(X1), X2, X3)
active(fst(X)) → fst(active(X))
active(U31(X1, X2, X3)) → U31(active(X1), X2, X3)
active(U32(X1, X2)) → U32(active(X1), X2)
active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))
active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))
active(U61(X)) → U61(active(X))
active(U71(X)) → U71(active(X))
active(U81(X)) → U81(active(X))
active(U91(X)) → U91(active(X))
active(tail(X)) → tail(active(X))
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(sel(X1, X2)) → sel(active(X1), X2)
active(sel(X1, X2)) → sel(X1, active(X2))
U101(mark(X1), X2) → mark(U101(X1, X2))
U102(mark(X)) → mark(U102(X))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
U111(mark(X)) → mark(U111(X))
snd(mark(X)) → mark(snd(X))
splitAt(mark(X1), X2) → mark(splitAt(X1, X2))
splitAt(X1, mark(X2)) → mark(splitAt(X1, X2))
U121(mark(X)) → mark(U121(X))
U131(mark(X1), X2) → mark(U131(X1, X2))
U132(mark(X)) → mark(U132(X))
U141(mark(X1), X2) → mark(U141(X1, X2))
U142(mark(X)) → mark(U142(X))
U151(mark(X1), X2) → mark(U151(X1, X2))
U152(mark(X)) → mark(U152(X))
U161(mark(X1), X2) → mark(U161(X1, X2))
cons(mark(X1), X2) → mark(cons(X1, X2))
natsFrom(mark(X)) → mark(natsFrom(X))
s(mark(X)) → mark(s(X))
U171(mark(X1), X2, X3) → mark(U171(X1, X2, X3))
U172(mark(X1), X2, X3) → mark(U172(X1, X2, X3))
head(mark(X)) → mark(head(X))
afterNth(mark(X1), X2) → mark(afterNth(X1, X2))
afterNth(X1, mark(X2)) → mark(afterNth(X1, X2))
U181(mark(X1), X2) → mark(U181(X1, X2))
U182(mark(X1), X2) → mark(U182(X1, X2))
U191(mark(X1), X2) → mark(U191(X1, X2))
pair(mark(X1), X2) → mark(pair(X1, X2))
pair(X1, mark(X2)) → mark(pair(X1, X2))
U201(mark(X1), X2, X3, X4) → mark(U201(X1, X2, X3, X4))
U202(mark(X1), X2, X3, X4) → mark(U202(X1, X2, X3, X4))
U203(mark(X1), X2, X3, X4) → mark(U203(X1, X2, X3, X4))
U204(mark(X1), X2) → mark(U204(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2) → mark(U22(X1, X2))
U211(mark(X1), X2) → mark(U211(X1, X2))
U212(mark(X1), X2) → mark(U212(X1, X2))
U221(mark(X1), X2, X3) → mark(U221(X1, X2, X3))
U222(mark(X1), X2, X3) → mark(U222(X1, X2, X3))
fst(mark(X)) → mark(fst(X))
U31(mark(X1), X2, X3) → mark(U31(X1, X2, X3))
U32(mark(X1), X2) → mark(U32(X1, X2))
U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))
U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))
U61(mark(X)) → mark(U61(X))
U71(mark(X)) → mark(U71(X))
U81(mark(X)) → mark(U81(X))
U91(mark(X)) → mark(U91(X))
tail(mark(X)) → mark(tail(X))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
sel(mark(X1), X2) → mark(sel(X1, X2))
sel(X1, mark(X2)) → mark(sel(X1, X2))
proper(U101(X1, X2)) → U101(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(U102(X)) → U102(proper(X))
proper(isLNat(X)) → isLNat(proper(X))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(U111(X)) → U111(proper(X))
proper(snd(X)) → snd(proper(X))
proper(splitAt(X1, X2)) → splitAt(proper(X1), proper(X2))
proper(U121(X)) → U121(proper(X))
proper(U131(X1, X2)) → U131(proper(X1), proper(X2))
proper(U132(X)) → U132(proper(X))
proper(U141(X1, X2)) → U141(proper(X1), proper(X2))
proper(U142(X)) → U142(proper(X))
proper(U151(X1, X2)) → U151(proper(X1), proper(X2))
proper(U152(X)) → U152(proper(X))
proper(U161(X1, X2)) → U161(proper(X1), proper(X2))
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(natsFrom(X)) → natsFrom(proper(X))
proper(s(X)) → s(proper(X))
proper(U171(X1, X2, X3)) → U171(proper(X1), proper(X2), proper(X3))
proper(U172(X1, X2, X3)) → U172(proper(X1), proper(X2), proper(X3))
proper(head(X)) → head(proper(X))
proper(afterNth(X1, X2)) → afterNth(proper(X1), proper(X2))
proper(U181(X1, X2)) → U181(proper(X1), proper(X2))
proper(U182(X1, X2)) → U182(proper(X1), proper(X2))
proper(U191(X1, X2)) → U191(proper(X1), proper(X2))
proper(pair(X1, X2)) → pair(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(U201(X1, X2, X3, X4)) → U201(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U202(X1, X2, X3, X4)) → U202(proper(X1), proper(X2), proper(X3), proper(X4))
proper(isNatural(X)) → isNatural(proper(X))
proper(U203(X1, X2, X3, X4)) → U203(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U204(X1, X2)) → U204(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2)) → U22(proper(X1), proper(X2))
proper(U211(X1, X2)) → U211(proper(X1), proper(X2))
proper(U212(X1, X2)) → U212(proper(X1), proper(X2))
proper(U221(X1, X2, X3)) → U221(proper(X1), proper(X2), proper(X3))
proper(U222(X1, X2, X3)) → U222(proper(X1), proper(X2), proper(X3))
proper(fst(X)) → fst(proper(X))
proper(U31(X1, X2, X3)) → U31(proper(X1), proper(X2), proper(X3))
proper(U32(X1, X2)) → U32(proper(X1), proper(X2))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))
proper(U42(X)) → U42(proper(X))
proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))
proper(U61(X)) → U61(proper(X))
proper(U71(X)) → U71(proper(X))
proper(U81(X)) → U81(proper(X))
proper(U91(X)) → U91(proper(X))
proper(isPLNat(X)) → isPLNat(proper(X))
proper(tail(X)) → tail(proper(X))
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(0) → ok(0)
proper(sel(X1, X2)) → sel(proper(X1), proper(X2))
U101(ok(X1), ok(X2)) → ok(U101(X1, X2))
U102(ok(X)) → ok(U102(X))
isLNat(ok(X)) → ok(isLNat(X))
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
U111(ok(X)) → ok(U111(X))
snd(ok(X)) → ok(snd(X))
splitAt(ok(X1), ok(X2)) → ok(splitAt(X1, X2))
U121(ok(X)) → ok(U121(X))
U131(ok(X1), ok(X2)) → ok(U131(X1, X2))
U132(ok(X)) → ok(U132(X))
U141(ok(X1), ok(X2)) → ok(U141(X1, X2))
U142(ok(X)) → ok(U142(X))
U151(ok(X1), ok(X2)) → ok(U151(X1, X2))
U152(ok(X)) → ok(U152(X))
U161(ok(X1), ok(X2)) → ok(U161(X1, X2))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
natsFrom(ok(X)) → ok(natsFrom(X))
s(ok(X)) → ok(s(X))
U171(ok(X1), ok(X2), ok(X3)) → ok(U171(X1, X2, X3))
U172(ok(X1), ok(X2), ok(X3)) → ok(U172(X1, X2, X3))
head(ok(X)) → ok(head(X))
afterNth(ok(X1), ok(X2)) → ok(afterNth(X1, X2))
U181(ok(X1), ok(X2)) → ok(U181(X1, X2))
U182(ok(X1), ok(X2)) → ok(U182(X1, X2))
U191(ok(X1), ok(X2)) → ok(U191(X1, X2))
pair(ok(X1), ok(X2)) → ok(pair(X1, X2))
U201(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U201(X1, X2, X3, X4))
U202(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U202(X1, X2, X3, X4))
isNatural(ok(X)) → ok(isNatural(X))
U203(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U203(X1, X2, X3, X4))
U204(ok(X1), ok(X2)) → ok(U204(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2)) → ok(U22(X1, X2))
U211(ok(X1), ok(X2)) → ok(U211(X1, X2))
U212(ok(X1), ok(X2)) → ok(U212(X1, X2))
U221(ok(X1), ok(X2), ok(X3)) → ok(U221(X1, X2, X3))
U222(ok(X1), ok(X2), ok(X3)) → ok(U222(X1, X2, X3))
fst(ok(X)) → ok(fst(X))
U31(ok(X1), ok(X2), ok(X3)) → ok(U31(X1, X2, X3))
U32(ok(X1), ok(X2)) → ok(U32(X1, X2))
U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))
U52(ok(X)) → ok(U52(X))
U61(ok(X)) → ok(U61(X))
U71(ok(X)) → ok(U71(X))
U81(ok(X)) → ok(U81(X))
U91(ok(X)) → ok(U91(X))
isPLNat(ok(X)) → ok(isPLNat(X))
tail(ok(X)) → ok(tail(X))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
sel(ok(X1), ok(X2)) → ok(sel(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
Special symbols used for the transformation (see [GM04]):
top: top, active: active, mark: mark, ok: ok, proper: proper
The replacement map contains the following entries:

U101: {1}
tt: empty set
U102: {1}
isLNat: empty set
U11: {1}
U12: {1}
U111: {1}
snd: {1}
splitAt: {1, 2}
U121: {1}
U131: {1}
U132: {1}
U141: {1}
U142: {1}
U151: {1}
U152: {1}
U161: {1}
cons: {1}
natsFrom: {1}
s: {1}
U171: {1}
U172: {1}
head: {1}
afterNth: {1, 2}
U181: {1}
U182: {1}
U191: {1}
pair: {1, 2}
nil: empty set
U201: {1}
U202: {1}
isNatural: empty set
U203: {1}
U204: {1}
U21: {1}
U22: {1}
U211: {1}
U212: {1}
U221: {1}
U222: {1}
fst: {1}
U31: {1}
U32: {1}
U41: {1}
U42: {1}
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U81: {1}
U91: {1}
isPLNat: empty set
tail: {1}
take: {1, 2}
0: empty set
sel: {1, 2}
The QTRS contained all rules created by the complete Giesl-Middeldorp transformation. Therefore, the inverse transformation is complete (and sound).

(2) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, XS)
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

The replacement map contains the following entries:

(3) CSDependencyPairsProof (EQUIVALENT transformation)

Using Improved CS-DPs [LPAR08] we result in the following initial Q-CSDP problem.

(4) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, U102', SND, SPLITAT, U132', U142', U152', HEAD, AFTERNTH, FST, U42', U52', U61', U71', U81', U91', U111', U121', NATSFROM, SEL, TAIL, TAKE} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U101', U12', U11', U131', U141', U151', U172', U171', U182', U181', U202', U201', U203', U204', U22', U21', U212', U211', U222', U221', U32', U31', U41', U51', U161', U191'} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat, ISLNAT, ISNATURAL, ISPLNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

U101'(tt, V2) → U102'(isLNat(V2))
U101'(tt, V2) → ISLNAT(V2)
U11'(tt, N, XS) → U12'(isLNat(XS), N, XS)
U11'(tt, N, XS) → ISLNAT(XS)
U12'(tt, N, XS) → SND(splitAt(N, XS))
U12'(tt, N, XS) → SPLITAT(N, XS)
U131'(tt, V2) → U132'(isLNat(V2))
U131'(tt, V2) → ISLNAT(V2)
U141'(tt, V2) → U142'(isLNat(V2))
U141'(tt, V2) → ISLNAT(V2)
U151'(tt, V2) → U152'(isLNat(V2))
U151'(tt, V2) → ISLNAT(V2)
U171'(tt, N, XS) → U172'(isLNat(XS), N, XS)
U171'(tt, N, XS) → ISLNAT(XS)
U172'(tt, N, XS) → HEAD(afterNth(N, XS))
U172'(tt, N, XS) → AFTERNTH(N, XS)
U181'(tt, Y) → U182'(isLNat(Y), Y)
U181'(tt, Y) → ISLNAT(Y)
U201'(tt, N, X, XS) → U202'(isNatural(X), N, X, XS)
U201'(tt, N, X, XS) → ISNATURAL(X)
U202'(tt, N, X, XS) → U203'(isLNat(XS), N, X, XS)
U202'(tt, N, X, XS) → ISLNAT(XS)
U203'(tt, N, X, XS) → U204'(splitAt(N, XS), X)
U203'(tt, N, X, XS) → SPLITAT(N, XS)
U21'(tt, X, Y) → U22'(isLNat(Y), X)
U21'(tt, X, Y) → ISLNAT(Y)
U211'(tt, XS) → U212'(isLNat(XS), XS)
U211'(tt, XS) → ISLNAT(XS)
U221'(tt, N, XS) → U222'(isLNat(XS), N, XS)
U221'(tt, N, XS) → ISLNAT(XS)
U222'(tt, N, XS) → FST(splitAt(N, XS))
U222'(tt, N, XS) → SPLITAT(N, XS)
U31'(tt, N, XS) → U32'(isLNat(XS), N)
U31'(tt, N, XS) → ISLNAT(XS)
U41'(tt, V2) → U42'(isLNat(V2))
U41'(tt, V2) → ISLNAT(V2)
U51'(tt, V2) → U52'(isLNat(V2))
U51'(tt, V2) → ISLNAT(V2)
AFTERNTH(N, XS) → U11'(isNatural(N), N, XS)
AFTERNTH(N, XS) → ISNATURAL(N)
FST(pair(X, Y)) → U21'(isLNat(X), X, Y)
FST(pair(X, Y)) → ISLNAT(X)
HEAD(cons(N, XS)) → U31'(isNatural(N), N, XS)
HEAD(cons(N, XS)) → ISNATURAL(N)
ISLNAT(afterNth(V1, V2)) → U41'(isNatural(V1), V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISLNAT(cons(V1, V2)) → U51'(isNatural(V1), V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISLNAT(fst(V1)) → U61'(isPLNat(V1))
ISLNAT(fst(V1)) → ISPLNAT(V1)
ISLNAT(natsFrom(V1)) → U71'(isNatural(V1))
ISLNAT(natsFrom(V1)) → ISNATURAL(V1)
ISLNAT(snd(V1)) → U81'(isPLNat(V1))
ISLNAT(snd(V1)) → ISPLNAT(V1)
ISLNAT(tail(V1)) → U91'(isLNat(V1))
ISLNAT(tail(V1)) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U101'(isNatural(V1), V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → U111'(isLNat(V1))
ISNATURAL(head(V1)) → ISLNAT(V1)
ISNATURAL(s(V1)) → U121'(isNatural(V1))
ISNATURAL(s(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U131'(isNatural(V1), V2)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISPLNAT(pair(V1, V2)) → U141'(isLNat(V1), V2)
ISPLNAT(pair(V1, V2)) → ISLNAT(V1)
ISPLNAT(splitAt(V1, V2)) → U151'(isNatural(V1), V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURAL(V1)
NATSFROM(N) → U161'(isNatural(N), N)
NATSFROM(N) → ISNATURAL(N)
SEL(N, XS) → U171'(isNatural(N), N, XS)
SEL(N, XS) → ISNATURAL(N)
SND(pair(X, Y)) → U181'(isLNat(X), Y)
SND(pair(X, Y)) → ISLNAT(X)
SPLITAT(0, XS) → U191'(isLNat(XS), XS)
SPLITAT(0, XS) → ISLNAT(XS)
SPLITAT(s(N), cons(X, XS)) → U201'(isNatural(N), N, X, XS)
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → U211'(isNatural(N), XS)
TAIL(cons(N, XS)) → ISNATURAL(N)
TAKE(N, XS) → U221'(isNatural(N), N, XS)
TAKE(N, XS) → ISNATURAL(N)

The collapsing dependency pairs are DP_c:

U12'(tt, N, XS) → N
U12'(tt, N, XS) → XS
U161'(tt, N) → N
U172'(tt, N, XS) → N
U172'(tt, N, XS) → XS
U182'(tt, Y) → Y
U191'(tt, XS) → XS
U203'(tt, N, X, XS) → N
U203'(tt, N, X, XS) → XS
U204'(pair(YS, ZS), X) → X
U212'(tt, XS) → XS
U22'(tt, X) → X
U222'(tt, N, XS) → N
U222'(tt, N, XS) → XS
U32'(tt, N) → N

The hidden terms of R are:

natsFrom(s(x0))

Every hiding context is built from:

s on positions {1}
natsFrom on positions {1}

Hence, the new unhiding pairs DP_u are :

U12'(tt, N, XS) → U(N)
U12'(tt, N, XS) → U(XS)
U161'(tt, N) → U(N)
U172'(tt, N, XS) → U(N)
U172'(tt, N, XS) → U(XS)
U182'(tt, Y) → U(Y)
U191'(tt, XS) → U(XS)
U203'(tt, N, X, XS) → U(N)
U203'(tt, N, X, XS) → U(XS)
U204'(pair(YS, ZS), X) → U(X)
U212'(tt, XS) → U(XS)
U22'(tt, X) → U(X)
U222'(tt, N, XS) → U(N)
U222'(tt, N, XS) → U(XS)
U32'(tt, N) → U(N)
U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)
U(natsFrom(s(x0))) → NATSFROM(s(x0))

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, XS)
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

(5) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 3 SCCs with 67 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U41', U51', U131', U141', U101', U151'} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat, ISLNAT, ISNATURAL, ISPLNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISLNAT(afterNth(V1, V2)) → U41'(isNatural(V1), V2)
U41'(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U51'(isNatural(V1), V2)
U51'(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISNATURAL(s(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U131'(isNatural(V1), V2)
U131'(tt, V2) → ISLNAT(V2)
ISLNAT(fst(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U141'(isLNat(V1), V2)
U141'(tt, V2) → ISLNAT(V2)
ISLNAT(natsFrom(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISLNAT(snd(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → ISLNAT(V1)
ISLNAT(tail(V1)) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U101'(isNatural(V1), V2)
U101'(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)
ISPLNAT(splitAt(V1, V2)) → U151'(isNatural(V1), V2)
U151'(tt, V2) → ISLNAT(V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURAL(V1)

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, XS)
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

(8) QCSUsableRulesProof (EQUIVALENT transformation)

The following rules are not useable [DA_EMMES] and can be deleted:

U11(tt, x0, x1) → U12(isLNat(x1), x0, x1)
U12(tt, x0, x1) → snd(splitAt(x0, x1))
U161(tt, x0) → cons(x0, natsFrom(s(x0)))
U171(tt, x0, x1) → U172(isLNat(x1), x0, x1)
U172(tt, x0, x1) → head(afterNth(x0, x1))
U181(tt, x0) → U182(isLNat(x0), x0)
U182(tt, x0) → x0
U191(tt, x0) → pair(nil, x0)
U201(tt, x0, x1, x2) → U202(isNatural(x1), x0, x1, x2)
U202(tt, x0, x1, x2) → U203(isLNat(x2), x0, x1, x2)
U203(tt, x0, x1, x2) → U204(splitAt(x0, x2), x1)
U204(pair(x0, x1), x2) → pair(cons(x2, x0), x1)
U21(tt, x0, x1) → U22(isLNat(x1), x0)
U211(tt, x0) → U212(isLNat(x0), x0)
U212(tt, x0) → x0
U22(tt, x0) → x0
U221(tt, x0, x1) → U222(isLNat(x1), x0, x1)
U222(tt, x0, x1) → fst(splitAt(x0, x1))
U31(tt, x0, x1) → U32(isLNat(x1), x0)
U32(tt, x0) → x0
afterNth(x0, x1) → U11(isNatural(x0), x0, x1)
fst(pair(x0, x1)) → U21(isLNat(x0), x0, x1)
head(cons(x0, x1)) → U31(isNatural(x0), x0, x1)
natsFrom(x0) → U161(isNatural(x0), x0)
sel(x0, x1) → U171(isNatural(x0), x0, x1)
snd(pair(x0, x1)) → U181(isLNat(x0), x1)
splitAt(0, x0) → U191(isLNat(x0), x0)
splitAt(s(x0), cons(x1, x2)) → U201(isNatural(x0), x0, x1, x2)
tail(cons(x0, x1)) → U211(isNatural(x0), x1)
take(x0, x1) → U221(isNatural(x0), x0, x1)

(9) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {head, U111, afterNth, s, U121, sel, U132, U52, fst, U61, pair, natsFrom, U71, snd, U81, splitAt, U152, tail, U91, take, U102, U142, U42} are replacing on all positions.
For all symbols f in {U41, U131, cons, U51, U141, U151, U101, U41', U51', U131', U141', U101', U151'} we have µ(f) = {1}.
The symbols in {isNatural, isLNat, isPLNat, ISLNAT, ISNATURAL, ISPLNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISLNAT(afterNth(V1, V2)) → U41'(isNatural(V1), V2)
U41'(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U51'(isNatural(V1), V2)
U51'(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISNATURAL(s(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U131'(isNatural(V1), V2)
U131'(tt, V2) → ISLNAT(V2)
ISLNAT(fst(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U141'(isLNat(V1), V2)
U141'(tt, V2) → ISLNAT(V2)
ISLNAT(natsFrom(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISLNAT(snd(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → ISLNAT(V1)
ISLNAT(tail(V1)) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U101'(isNatural(V1), V2)
U101'(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)
ISPLNAT(splitAt(V1, V2)) → U151'(isNatural(V1), V2)
U151'(tt, V2) → ISLNAT(V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURAL(V1)

The TRS R consists of the following rules:

isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U131(tt, V2) → U132(isLNat(V2))
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
U51(tt, V2) → U52(isLNat(V2))
isLNat(fst(V1)) → U61(isPLNat(V1))
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isLNat(natsFrom(V1)) → U71(isNatural(V1))
U71(tt) → tt
isLNat(snd(V1)) → U81(isPLNat(V1))
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
U151(tt, V2) → U152(isLNat(V2))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U91(tt) → tt
U152(tt) → tt
U81(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U61(tt) → tt
U52(tt) → tt
U132(tt) → tt
U121(tt) → tt
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U111(tt) → tt

Q is empty.

(10) QCSDPMuMonotonicPoloProof (EQUIVALENT transformation)

By using the following µ-monotonic polynomial ordering [POLO], at least one Dependency Pair or term rewrite system rule of this Q-CSDP problem can be strictly oriented and thus deleted.
Strictly oriented dependency pairs:

ISLNAT(afterNth(V1, V2)) → U41'(isNatural(V1), V2)
U41'(tt, V2) → ISLNAT(V2)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U51'(isNatural(V1), V2)
U51'(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISNATURAL(s(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U131'(isNatural(V1), V2)
U131'(tt, V2) → ISLNAT(V2)
ISLNAT(fst(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U141'(isLNat(V1), V2)
U141'(tt, V2) → ISLNAT(V2)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISLNAT(snd(V1)) → ISPLNAT(V1)
ISLNAT(tail(V1)) → ISLNAT(V1)
U101'(tt, V2) → ISLNAT(V2)
ISPLNAT(splitAt(V1, V2)) → U151'(isNatural(V1), V2)
U151'(tt, V2) → ISLNAT(V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURAL(V1)

Strictly oriented rules of the TRS R:

isNatural(0) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U131(tt, V2) → U132(isLNat(V2))
U51(tt, V2) → U52(isLNat(V2))
U71(tt) → tt
isLNat(snd(V1)) → U81(isPLNat(V1))
U151(tt, V2) → U152(isLNat(V2))
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U91(tt) → tt
U152(tt) → tt
U81(tt) → tt
U142(tt) → tt
U61(tt) → tt
U52(tt) → tt
U132(tt) → tt
U121(tt) → tt
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U111(tt) → tt

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 2
POL(ISLNAT(x₁)) = 1 + x₁
POL(ISNATURAL(x₁)) = 2 + 2·x₁
POL(ISPLNAT(x₁)) = 1 + 2·x₁
POL(U101(x₁, x₂)) = 1 + x₁ + x₂
POL(U101'(x₁, x₂)) = 2 + x₁ + x₂
POL(U102(x₁)) = 1 + x₁
POL(U111(x₁)) = 2·x₁
POL(U121(x₁)) = 1 + x₁
POL(U131(x₁, x₂)) = 2·x₁ + 2·x₂
POL(U131'(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(U132(x₁)) = 1 + 2·x₁
POL(U141(x₁, x₂)) = x₁ + 2·x₂
POL(U141'(x₁, x₂)) = 2·x₁ + 2·x₂
POL(U142(x₁)) = 2 + x₁
POL(U151(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(U151'(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(U152(x₁)) = 1 + 2·x₁
POL(U41(x₁, x₂)) = x₁ + 2·x₂
POL(U41'(x₁, x₂)) = x₁ + x₂
POL(U42(x₁)) = 1 + x₁
POL(U51(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(U51'(x₁, x₂)) = 1 + x₁ + x₂
POL(U52(x₁)) = 2 + x₁
POL(U61(x₁)) = 1 + x₁
POL(U71(x₁)) = 1 + x₁
POL(U81(x₁)) = 2·x₁
POL(U91(x₁)) = 2 + x₁
POL(afterNth(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(fst(x₁)) = 1 + 2·x₁
POL(head(x₁)) = x₁
POL(isLNat(x₁)) = x₁
POL(isNatural(x₁)) = 2·x₁
POL(isPLNat(x₁)) = x₁
POL(natsFrom(x₁)) = 1 + 2·x₁
POL(nil) = 2
POL(pair(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 2 + x₁
POL(sel(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(snd(x₁)) = 2 + 2·x₁
POL(splitAt(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(tail(x₁)) = 2 + x₁
POL(take(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(tt) = 2

(11) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {head, U111, fst, U61, pair, natsFrom, U71, splitAt, tail, U91, take, U142, afterNth} are replacing on all positions.
For all symbols f in {cons, U51, U141, U151, U101, U101'} we have µ(f) = {1}.
The symbols in {isNatural, isLNat, isPLNat, ISNATURAL, ISLNAT, ISPLNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISLNAT(natsFrom(V1)) → ISNATURAL(V1)
ISPLNAT(pair(V1, V2)) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U101'(isNatural(V1), V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)

The TRS R consists of the following rules:

isNatural(head(V1)) → U111(isLNat(V1))
isLNat(nil) → tt
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U141(tt, V2) → U142(isLNat(V2))

Q is empty.

(12) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 0 SCCs with 5 less nodes.

(13) TRUE

(14) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, NATSFROM} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U161'} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat, U} are not replacing on any position.

The TRS P consists of the following rules:

NATSFROM(N) → U161'(isNatural(N), N)
U161'(tt, N) → U(N)
U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)
U(natsFrom(s(x0))) → NATSFROM(s(x0))

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, XS)
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

(15) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].

The following pairs can be oriented strictly and are deleted.

U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)
U(natsFrom(s(x0))) → NATSFROM(s(x0))

The remaining pairs can at least be oriented weakly.

NATSFROM(N) → U161'(isNatural(N), N)
U161'(tt, N) → U(N)

Used ordering: Combined order from the following AFS and order.
U161'(x1, x2) = x2
NATSFROM(x1) = x1
U(x1) = x1

Subterm Order

(16) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, NATSFROM} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U161'} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat, U} are not replacing on any position.

The TRS P consists of the following rules:

NATSFROM(N) → U161'(isNatural(N), N)
U161'(tt, N) → U(N)

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, XS)
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

(17) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 0 SCCs with 2 less nodes.

(18) TRUE

(19) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, SPLITAT} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U202', U201', U203'} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat} are not replacing on any position.

The TRS P consists of the following rules:

U201'(tt, N, X, XS) → U202'(isNatural(X), N, X, XS)
U202'(tt, N, X, XS) → U203'(isLNat(XS), N, X, XS)
U203'(tt, N, X, XS) → SPLITAT(N, XS)
SPLITAT(s(N), cons(X, XS)) → U201'(isNatural(N), N, X, XS)

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, XS)
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

(20) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].

The following pairs can be oriented strictly and are deleted.

SPLITAT(s(N), cons(X, XS)) → U201'(isNatural(N), N, X, XS)

The remaining pairs can at least be oriented weakly.

U201'(tt, N, X, XS) → U202'(isNatural(X), N, X, XS)
U202'(tt, N, X, XS) → U203'(isLNat(XS), N, X, XS)
U203'(tt, N, X, XS) → SPLITAT(N, XS)

Used ordering: Combined order from the following AFS and order.
U202'(x1, x2, x3, x4) = x2
U201'(x1, x2, x3, x4) = x2
U203'(x1, x2, x3, x4) = x2
SPLITAT(x1, x2) = x1

Subterm Order

(21) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, SPLITAT} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U202', U201', U203'} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat} are not replacing on any position.

The TRS P consists of the following rules:

U201'(tt, N, X, XS) → U202'(isNatural(X), N, X, XS)
U202'(tt, N, X, XS) → U203'(isLNat(XS), N, X, XS)
U203'(tt, N, X, XS) → SPLITAT(N, XS)

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, XS)
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

(22) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 0 SCCs with 3 less nodes.

(0) Obligation:

(1) QTRSToCSRProof (EQUIVALENT transformation)

(2) Obligation:

(3) CSDependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) QCSDependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) QCSUsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) QCSDPMuMonotonicPoloProof (EQUIVALENT transformation)

(11) Obligation:

(12) QCSDependencyGraphProof (EQUIVALENT transformation)

(13) TRUE

(14) Obligation:

(15) QCSDPSubtermProof (EQUIVALENT transformation)

(16) Obligation:

(17) QCSDependencyGraphProof (EQUIVALENT transformation)

(18) TRUE

(19) Obligation:

(20) QCSDPSubtermProof (EQUIVALENT transformation)

(21) Obligation:

(22) QCSDependencyGraphProof (EQUIVALENT transformation)

(23) TRUE