Runtime Complexity TRS:
The TRS R consists of the following rules:

a__U101(tt, N, XS) → a__fst(a__splitAt(mark(N), mark(XS)))
a__U11(tt, N, XS) → a__snd(a__splitAt(mark(N), mark(XS)))
a__U21(tt, X) → mark(X)
a__U31(tt, N) → mark(N)
a__U41(tt, N) → cons(mark(N), natsFrom(s(N)))
a__U51(tt, N, XS) → a__head(a__afterNth(mark(N), mark(XS)))
a__U61(tt, Y) → mark(Y)
a__U71(tt, XS) → pair(nil, mark(XS))
a__U81(tt, N, X, XS) → a__U82(a__splitAt(mark(N), mark(XS)), X)
a__U82(pair(YS, ZS), X) → pair(cons(mark(X), YS), mark(ZS))
a__U91(tt, XS) → mark(XS)
a__afterNth(N, XS) → a__U11(a__and(a__isNatural(N), isLNat(XS)), N, XS)
a__and(tt, X) → mark(X)
a__fst(pair(X, Y)) → a__U21(a__and(a__isLNat(X), isLNat(Y)), X)
a__head(cons(N, XS)) → a__U31(a__and(a__isNatural(N), isLNat(XS)), N)
a__isLNat(nil) → tt
a__isLNat(afterNth(V1, V2)) → a__and(a__isNatural(V1), isLNat(V2))
a__isLNat(cons(V1, V2)) → a__and(a__isNatural(V1), isLNat(V2))
a__isLNat(fst(V1)) → a__isPLNat(V1)
a__isLNat(natsFrom(V1)) → a__isNatural(V1)
a__isLNat(snd(V1)) → a__isPLNat(V1)
a__isLNat(tail(V1)) → a__isLNat(V1)
a__isLNat(take(V1, V2)) → a__and(a__isNatural(V1), isLNat(V2))
a__isNatural(0) → tt
a__isNatural(head(V1)) → a__isLNat(V1)
a__isNatural(s(V1)) → a__isNatural(V1)
a__isNatural(sel(V1, V2)) → a__and(a__isNatural(V1), isLNat(V2))
a__isPLNat(pair(V1, V2)) → a__and(a__isLNat(V1), isLNat(V2))
a__isPLNat(splitAt(V1, V2)) → a__and(a__isNatural(V1), isLNat(V2))
a__natsFrom(N) → a__U41(a__isNatural(N), N)
a__sel(N, XS) → a__U51(a__and(a__isNatural(N), isLNat(XS)), N, XS)
a__snd(pair(X, Y)) → a__U61(a__and(a__isLNat(X), isLNat(Y)), Y)
a__splitAt(0, XS) → a__U71(a__isLNat(XS), XS)
a__splitAt(s(N), cons(X, XS)) → a__U81(a__and(a__isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)
a__tail(cons(N, XS)) → a__U91(a__and(a__isNatural(N), isLNat(XS)), XS)
a__take(N, XS) → a__U101(a__and(a__isNatural(N), isLNat(XS)), N, XS)
mark(U101(X1, X2, X3)) → a__U101(mark(X1), X2, X3)
mark(fst(X)) → a__fst(mark(X))
mark(splitAt(X1, X2)) → a__splitAt(mark(X1), mark(X2))
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)
mark(snd(X)) → a__snd(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(natsFrom(X)) → a__natsFrom(mark(X))
mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(head(X)) → a__head(mark(X))
mark(afterNth(X1, X2)) → a__afterNth(mark(X1), mark(X2))
mark(U61(X1, X2)) → a__U61(mark(X1), X2)
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U81(X1, X2, X3, X4)) → a__U81(mark(X1), X2, X3, X4)
mark(U82(X1, X2)) → a__U82(mark(X1), X2)
mark(U91(X1, X2)) → a__U91(mark(X1), X2)
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatural(X)) → a__isNatural(X)
mark(isLNat(X)) → a__isLNat(X)
mark(isPLNat(X)) → a__isPLNat(X)
mark(tail(X)) → a__tail(mark(X))
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(tt) → tt
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(pair(X1, X2)) → pair(mark(X1), mark(X2))
mark(nil) → nil
mark(0) → 0
a__U101(X1, X2, X3) → U101(X1, X2, X3)
a__fst(X) → fst(X)
a__splitAt(X1, X2) → splitAt(X1, X2)
a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__snd(X) → snd(X)
a__U21(X1, X2) → U21(X1, X2)
a__U31(X1, X2) → U31(X1, X2)
a__U41(X1, X2) → U41(X1, X2)
a__natsFrom(X) → natsFrom(X)
a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__head(X) → head(X)
a__afterNth(X1, X2) → afterNth(X1, X2)
a__U61(X1, X2) → U61(X1, X2)
a__U71(X1, X2) → U71(X1, X2)
a__U81(X1, X2, X3, X4) → U81(X1, X2, X3, X4)
a__U82(X1, X2) → U82(X1, X2)
a__U91(X1, X2) → U91(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNatural(X) → isNatural(X)
a__isLNat(X) → isLNat(X)
a__isPLNat(X) → isPLNat(X)
a__tail(X) → tail(X)
a__take(X1, X2) → take(X1, X2)
a__sel(X1, X2) → sel(X1, X2)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

a__U101'(tt', N, XS) → a__fst'(a__splitAt'(mark'(N), mark'(XS)))
a__U11'(tt', N, XS) → a__snd'(a__splitAt'(mark'(N), mark'(XS)))
a__U21'(tt', X) → mark'(X)
a__U31'(tt', N) → mark'(N)
a__U41'(tt', N) → cons'(mark'(N), natsFrom'(s'(N)))
a__U51'(tt', N, XS) → a__head'(a__afterNth'(mark'(N), mark'(XS)))
a__U61'(tt', Y) → mark'(Y)
a__U71'(tt', XS) → pair'(nil', mark'(XS))
a__U81'(tt', N, X, XS) → a__U82'(a__splitAt'(mark'(N), mark'(XS)), X)
a__U82'(pair'(YS, ZS), X) → pair'(cons'(mark'(X), YS), mark'(ZS))
a__U91'(tt', XS) → mark'(XS)
a__afterNth'(N, XS) → a__U11'(a__and'(a__isNatural'(N), isLNat'(XS)), N, XS)
a__and'(tt', X) → mark'(X)
a__fst'(pair'(X, Y)) → a__U21'(a__and'(a__isLNat'(X), isLNat'(Y)), X)
a__head'(cons'(N, XS)) → a__U31'(a__and'(a__isNatural'(N), isLNat'(XS)), N)
a__isLNat'(nil') → tt'
a__isLNat'(afterNth'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__isLNat'(cons'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__isLNat'(fst'(V1)) → a__isPLNat'(V1)
a__isLNat'(natsFrom'(V1)) → a__isNatural'(V1)
a__isLNat'(snd'(V1)) → a__isPLNat'(V1)
a__isLNat'(tail'(V1)) → a__isLNat'(V1)
a__isLNat'(take'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__isNatural'(0') → tt'
a__isNatural'(head'(V1)) → a__isLNat'(V1)
a__isNatural'(s'(V1)) → a__isNatural'(V1)
a__isNatural'(sel'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__isPLNat'(pair'(V1, V2)) → a__and'(a__isLNat'(V1), isLNat'(V2))
a__isPLNat'(splitAt'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__natsFrom'(N) → a__U41'(a__isNatural'(N), N)
a__sel'(N, XS) → a__U51'(a__and'(a__isNatural'(N), isLNat'(XS)), N, XS)
a__snd'(pair'(X, Y)) → a__U61'(a__and'(a__isLNat'(X), isLNat'(Y)), Y)
a__splitAt'(0', XS) → a__U71'(a__isLNat'(XS), XS)
a__splitAt'(s'(N), cons'(X, XS)) → a__U81'(a__and'(a__isNatural'(N), and'(isNatural'(X), isLNat'(XS))), N, X, XS)
a__tail'(cons'(N, XS)) → a__U91'(a__and'(a__isNatural'(N), isLNat'(XS)), XS)
a__take'(N, XS) → a__U101'(a__and'(a__isNatural'(N), isLNat'(XS)), N, XS)
mark'(U101'(X1, X2, X3)) → a__U101'(mark'(X1), X2, X3)
mark'(fst'(X)) → a__fst'(mark'(X))
mark'(splitAt'(X1, X2)) → a__splitAt'(mark'(X1), mark'(X2))
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(snd'(X)) → a__snd'(mark'(X))
mark'(U21'(X1, X2)) → a__U21'(mark'(X1), X2)
mark'(U31'(X1, X2)) → a__U31'(mark'(X1), X2)
mark'(U41'(X1, X2)) → a__U41'(mark'(X1), X2)
mark'(natsFrom'(X)) → a__natsFrom'(mark'(X))
mark'(U51'(X1, X2, X3)) → a__U51'(mark'(X1), X2, X3)
mark'(head'(X)) → a__head'(mark'(X))
mark'(afterNth'(X1, X2)) → a__afterNth'(mark'(X1), mark'(X2))
mark'(U61'(X1, X2)) → a__U61'(mark'(X1), X2)
mark'(U71'(X1, X2)) → a__U71'(mark'(X1), X2)
mark'(U81'(X1, X2, X3, X4)) → a__U81'(mark'(X1), X2, X3, X4)
mark'(U82'(X1, X2)) → a__U82'(mark'(X1), X2)
mark'(U91'(X1, X2)) → a__U91'(mark'(X1), X2)
mark'(and'(X1, X2)) → a__and'(mark'(X1), X2)
mark'(isNatural'(X)) → a__isNatural'(X)
mark'(isLNat'(X)) → a__isLNat'(X)
mark'(isPLNat'(X)) → a__isPLNat'(X)
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(take'(X1, X2)) → a__take'(mark'(X1), mark'(X2))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(tt') → tt'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(pair'(X1, X2)) → pair'(mark'(X1), mark'(X2))
mark'(nil') → nil'
mark'(0') → 0'
a__U101'(X1, X2, X3) → U101'(X1, X2, X3)
a__fst'(X) → fst'(X)
a__splitAt'(X1, X2) → splitAt'(X1, X2)
a__U11'(X1, X2, X3) → U11'(X1, X2, X3)
a__snd'(X) → snd'(X)
a__U21'(X1, X2) → U21'(X1, X2)
a__U31'(X1, X2) → U31'(X1, X2)
a__U41'(X1, X2) → U41'(X1, X2)
a__natsFrom'(X) → natsFrom'(X)
a__U51'(X1, X2, X3) → U51'(X1, X2, X3)
a__head'(X) → head'(X)
a__afterNth'(X1, X2) → afterNth'(X1, X2)
a__U61'(X1, X2) → U61'(X1, X2)
a__U71'(X1, X2) → U71'(X1, X2)
a__U81'(X1, X2, X3, X4) → U81'(X1, X2, X3, X4)
a__U82'(X1, X2) → U82'(X1, X2)
a__U91'(X1, X2) → U91'(X1, X2)
a__and'(X1, X2) → and'(X1, X2)
a__isNatural'(X) → isNatural'(X)
a__isLNat'(X) → isLNat'(X)
a__isPLNat'(X) → isPLNat'(X)
a__tail'(X) → tail'(X)
a__take'(X1, X2) → take'(X1, X2)
a__sel'(X1, X2) → sel'(X1, X2)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__U101'(tt', N, XS) → a__fst'(a__splitAt'(mark'(N), mark'(XS)))
a__U11'(tt', N, XS) → a__snd'(a__splitAt'(mark'(N), mark'(XS)))
a__U21'(tt', X) → mark'(X)
a__U31'(tt', N) → mark'(N)
a__U41'(tt', N) → cons'(mark'(N), natsFrom'(s'(N)))
a__U51'(tt', N, XS) → a__head'(a__afterNth'(mark'(N), mark'(XS)))
a__U61'(tt', Y) → mark'(Y)
a__U71'(tt', XS) → pair'(nil', mark'(XS))
a__U81'(tt', N, X, XS) → a__U82'(a__splitAt'(mark'(N), mark'(XS)), X)
a__U82'(pair'(YS, ZS), X) → pair'(cons'(mark'(X), YS), mark'(ZS))
a__U91'(tt', XS) → mark'(XS)
a__afterNth'(N, XS) → a__U11'(a__and'(a__isNatural'(N), isLNat'(XS)), N, XS)
a__and'(tt', X) → mark'(X)
a__fst'(pair'(X, Y)) → a__U21'(a__and'(a__isLNat'(X), isLNat'(Y)), X)
a__head'(cons'(N, XS)) → a__U31'(a__and'(a__isNatural'(N), isLNat'(XS)), N)
a__isLNat'(nil') → tt'
a__isLNat'(afterNth'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__isLNat'(cons'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__isLNat'(fst'(V1)) → a__isPLNat'(V1)
a__isLNat'(natsFrom'(V1)) → a__isNatural'(V1)
a__isLNat'(snd'(V1)) → a__isPLNat'(V1)
a__isLNat'(tail'(V1)) → a__isLNat'(V1)
a__isLNat'(take'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__isNatural'(0') → tt'
a__isNatural'(head'(V1)) → a__isLNat'(V1)
a__isNatural'(s'(V1)) → a__isNatural'(V1)
a__isNatural'(sel'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__isPLNat'(pair'(V1, V2)) → a__and'(a__isLNat'(V1), isLNat'(V2))
a__isPLNat'(splitAt'(V1, V2)) → a__and'(a__isNatural'(V1), isLNat'(V2))
a__natsFrom'(N) → a__U41'(a__isNatural'(N), N)
a__sel'(N, XS) → a__U51'(a__and'(a__isNatural'(N), isLNat'(XS)), N, XS)
a__snd'(pair'(X, Y)) → a__U61'(a__and'(a__isLNat'(X), isLNat'(Y)), Y)
a__splitAt'(0', XS) → a__U71'(a__isLNat'(XS), XS)
a__splitAt'(s'(N), cons'(X, XS)) → a__U81'(a__and'(a__isNatural'(N), and'(isNatural'(X), isLNat'(XS))), N, X, XS)
a__tail'(cons'(N, XS)) → a__U91'(a__and'(a__isNatural'(N), isLNat'(XS)), XS)
a__take'(N, XS) → a__U101'(a__and'(a__isNatural'(N), isLNat'(XS)), N, XS)
mark'(U101'(X1, X2, X3)) → a__U101'(mark'(X1), X2, X3)
mark'(fst'(X)) → a__fst'(mark'(X))
mark'(splitAt'(X1, X2)) → a__splitAt'(mark'(X1), mark'(X2))
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(snd'(X)) → a__snd'(mark'(X))
mark'(U21'(X1, X2)) → a__U21'(mark'(X1), X2)
mark'(U31'(X1, X2)) → a__U31'(mark'(X1), X2)
mark'(U41'(X1, X2)) → a__U41'(mark'(X1), X2)
mark'(natsFrom'(X)) → a__natsFrom'(mark'(X))
mark'(U51'(X1, X2, X3)) → a__U51'(mark'(X1), X2, X3)
mark'(head'(X)) → a__head'(mark'(X))
mark'(afterNth'(X1, X2)) → a__afterNth'(mark'(X1), mark'(X2))
mark'(U61'(X1, X2)) → a__U61'(mark'(X1), X2)
mark'(U71'(X1, X2)) → a__U71'(mark'(X1), X2)
mark'(U81'(X1, X2, X3, X4)) → a__U81'(mark'(X1), X2, X3, X4)
mark'(U82'(X1, X2)) → a__U82'(mark'(X1), X2)
mark'(U91'(X1, X2)) → a__U91'(mark'(X1), X2)
mark'(and'(X1, X2)) → a__and'(mark'(X1), X2)
mark'(isNatural'(X)) → a__isNatural'(X)
mark'(isLNat'(X)) → a__isLNat'(X)
mark'(isPLNat'(X)) → a__isPLNat'(X)
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(take'(X1, X2)) → a__take'(mark'(X1), mark'(X2))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(tt') → tt'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(pair'(X1, X2)) → pair'(mark'(X1), mark'(X2))
mark'(nil') → nil'
mark'(0') → 0'
a__U101'(X1, X2, X3) → U101'(X1, X2, X3)
a__fst'(X) → fst'(X)
a__splitAt'(X1, X2) → splitAt'(X1, X2)
a__U11'(X1, X2, X3) → U11'(X1, X2, X3)
a__snd'(X) → snd'(X)
a__U21'(X1, X2) → U21'(X1, X2)
a__U31'(X1, X2) → U31'(X1, X2)
a__U41'(X1, X2) → U41'(X1, X2)
a__natsFrom'(X) → natsFrom'(X)
a__U51'(X1, X2, X3) → U51'(X1, X2, X3)
a__head'(X) → head'(X)
a__afterNth'(X1, X2) → afterNth'(X1, X2)
a__U61'(X1, X2) → U61'(X1, X2)
a__U71'(X1, X2) → U71'(X1, X2)
a__U81'(X1, X2, X3, X4) → U81'(X1, X2, X3, X4)
a__U82'(X1, X2) → U82'(X1, X2)
a__U91'(X1, X2) → U91'(X1, X2)
a__and'(X1, X2) → and'(X1, X2)
a__isNatural'(X) → isNatural'(X)
a__isLNat'(X) → isLNat'(X)
a__isPLNat'(X) → isPLNat'(X)
a__tail'(X) → tail'(X)
a__take'(X1, X2) → take'(X1, X2)
a__sel'(X1, X2) → sel'(X1, X2)

Types:
a__U101' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
tt' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__fst' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__splitAt' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
mark' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U11' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__snd' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U21' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U31' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U41' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
cons' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
natsFrom' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
s' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U51' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__head' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__afterNth' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U61' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U71' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
pair' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
nil' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U81' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U82' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__U91' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__and' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__isNatural' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
isLNat' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__isLNat' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
afterNth' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
fst' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__isPLNat' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
snd' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
tail' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
take' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
0' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
head' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
sel' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
splitAt' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__natsFrom' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__sel' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
and' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
isNatural' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__tail' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
a__take' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U101' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U11' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U21' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U31' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U41' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U51' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U61' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U71' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U81' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U82' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
U91' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
isPLNat' :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat' → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
_hole_tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'1 :: tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'
_gen_tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'2 :: Nat → tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'

Heuristically decided to analyse the following defined symbols:
a__U101', a__fst', a__splitAt', mark', a__U11', a__snd', a__U21', a__U31', a__U41', a__U51', a__head', a__afterNth', a__U61', a__U71', a__U81', a__U82', a__U91', a__and', a__isNatural', a__isLNat', a__isPLNat', a__natsFrom', a__tail'

They will be analysed ascendingly in the following order:
a__U101' = a__fst'
a__U101' = a__splitAt'
a__U101' = mark'
a__U101' = a__U11'
a__U101' = a__snd'
a__U101' = a__U21'
a__U101' = a__U31'
a__U101' = a__U41'
a__U101' = a__U51'
a__U101' = a__head'
a__U101' = a__afterNth'
a__U101' = a__U61'
a__U101' = a__U71'
a__U101' = a__U81'
a__U101' = a__U82'
a__U101' = a__U91'
a__U101' = a__and'
a__U101' = a__isNatural'
a__U101' = a__isLNat'
a__U101' = a__isPLNat'
a__U101' = a__natsFrom'
a__U101' = a__tail'
a__fst' = a__splitAt'
a__fst' = mark'
a__fst' = a__U11'
a__fst' = a__snd'
a__fst' = a__U21'
a__fst' = a__U31'
a__fst' = a__U41'
a__fst' = a__U51'
a__fst' = a__head'
a__fst' = a__afterNth'
a__fst' = a__U61'
a__fst' = a__U71'
a__fst' = a__U81'
a__fst' = a__U82'
a__fst' = a__U91'
a__fst' = a__and'
a__fst' = a__isNatural'
a__fst' = a__isLNat'
a__fst' = a__isPLNat'
a__fst' = a__natsFrom'
a__fst' = a__tail'
a__splitAt' = mark'
a__splitAt' = a__U11'
a__splitAt' = a__snd'
a__splitAt' = a__U21'
a__splitAt' = a__U31'
a__splitAt' = a__U41'
a__splitAt' = a__U51'
a__splitAt' = a__head'
a__splitAt' = a__afterNth'
a__splitAt' = a__U61'
a__splitAt' = a__U71'
a__splitAt' = a__U81'
a__splitAt' = a__U82'
a__splitAt' = a__U91'
a__splitAt' = a__and'
a__splitAt' = a__isNatural'
a__splitAt' = a__isLNat'
a__splitAt' = a__isPLNat'
a__splitAt' = a__natsFrom'
a__splitAt' = a__tail'
mark' = a__U11'
mark' = a__snd'
mark' = a__U21'
mark' = a__U31'
mark' = a__U41'
mark' = a__U51'
mark' = a__head'
mark' = a__afterNth'
mark' = a__U61'
mark' = a__U71'
mark' = a__U81'
mark' = a__U82'
mark' = a__U91'
mark' = a__and'
mark' = a__isNatural'
mark' = a__isLNat'
mark' = a__isPLNat'
mark' = a__natsFrom'
mark' = a__tail'
a__U11' = a__snd'
a__U11' = a__U21'
a__U11' = a__U31'
a__U11' = a__U41'
a__U11' = a__U51'
a__U11' = a__head'
a__U11' = a__afterNth'
a__U11' = a__U61'
a__U11' = a__U71'
a__U11' = a__U81'
a__U11' = a__U82'
a__U11' = a__U91'
a__U11' = a__and'
a__U11' = a__isNatural'
a__U11' = a__isLNat'
a__U11' = a__isPLNat'
a__U11' = a__natsFrom'
a__U11' = a__tail'
a__snd' = a__U21'
a__snd' = a__U31'
a__snd' = a__U41'
a__snd' = a__U51'
a__snd' = a__head'
a__snd' = a__afterNth'
a__snd' = a__U61'
a__snd' = a__U71'
a__snd' = a__U81'
a__snd' = a__U82'
a__snd' = a__U91'
a__snd' = a__and'
a__snd' = a__isNatural'
a__snd' = a__isLNat'
a__snd' = a__isPLNat'
a__snd' = a__natsFrom'
a__snd' = a__tail'
a__U21' = a__U31'
a__U21' = a__U41'
a__U21' = a__U51'
a__U21' = a__head'
a__U21' = a__afterNth'
a__U21' = a__U61'
a__U21' = a__U71'
a__U21' = a__U81'
a__U21' = a__U82'
a__U21' = a__U91'
a__U21' = a__and'
a__U21' = a__isNatural'
a__U21' = a__isLNat'
a__U21' = a__isPLNat'
a__U21' = a__natsFrom'
a__U21' = a__tail'
a__U31' = a__U41'
a__U31' = a__U51'
a__U31' = a__head'
a__U31' = a__afterNth'
a__U31' = a__U61'
a__U31' = a__U71'
a__U31' = a__U81'
a__U31' = a__U82'
a__U31' = a__U91'
a__U31' = a__and'
a__U31' = a__isNatural'
a__U31' = a__isLNat'
a__U31' = a__isPLNat'
a__U31' = a__natsFrom'
a__U31' = a__tail'
a__U41' = a__U51'
a__U41' = a__head'
a__U41' = a__afterNth'
a__U41' = a__U61'
a__U41' = a__U71'
a__U41' = a__U81'
a__U41' = a__U82'
a__U41' = a__U91'
a__U41' = a__and'
a__U41' = a__isNatural'
a__U41' = a__isLNat'
a__U41' = a__isPLNat'
a__U41' = a__natsFrom'
a__U41' = a__tail'
a__U51' = a__head'
a__U51' = a__afterNth'
a__U51' = a__U61'
a__U51' = a__U71'
a__U51' = a__U81'
a__U51' = a__U82'
a__U51' = a__U91'
a__U51' = a__and'
a__U51' = a__isNatural'
a__U51' = a__isLNat'
a__U51' = a__isPLNat'
a__U51' = a__natsFrom'
a__U51' = a__tail'
a__head' = a__afterNth'
a__head' = a__U61'
a__head' = a__U71'
a__head' = a__U81'
a__head' = a__U82'
a__head' = a__U91'
a__head' = a__and'
a__head' = a__isNatural'
a__head' = a__isLNat'
a__head' = a__isPLNat'
a__head' = a__natsFrom'
a__head' = a__tail'
a__afterNth' = a__U61'
a__afterNth' = a__U71'
a__afterNth' = a__U81'
a__afterNth' = a__U82'
a__afterNth' = a__U91'
a__afterNth' = a__and'
a__afterNth' = a__isNatural'
a__afterNth' = a__isLNat'
a__afterNth' = a__isPLNat'
a__afterNth' = a__natsFrom'
a__afterNth' = a__tail'
a__U61' = a__U71'
a__U61' = a__U81'
a__U61' = a__U82'
a__U61' = a__U91'
a__U61' = a__and'
a__U61' = a__isNatural'
a__U61' = a__isLNat'
a__U61' = a__isPLNat'
a__U61' = a__natsFrom'
a__U61' = a__tail'
a__U71' = a__U81'
a__U71' = a__U82'
a__U71' = a__U91'
a__U71' = a__and'
a__U71' = a__isNatural'
a__U71' = a__isLNat'
a__U71' = a__isPLNat'
a__U71' = a__natsFrom'
a__U71' = a__tail'
a__U81' = a__U82'
a__U81' = a__U91'
a__U81' = a__and'
a__U81' = a__isNatural'
a__U81' = a__isLNat'
a__U81' = a__isPLNat'
a__U81' = a__natsFrom'
a__U81' = a__tail'
a__U82' = a__U91'
a__U82' = a__and'
a__U82' = a__isNatural'
a__U82' = a__isLNat'
a__U82' = a__isPLNat'
a__U82' = a__natsFrom'
a__U82' = a__tail'
a__U91' = a__and'
a__U91' = a__isNatural'
a__U91' = a__isLNat'
a__U91' = a__isPLNat'
a__U91' = a__natsFrom'
a__U91' = a__tail'
a__and' = a__isNatural'
a__and' = a__isLNat'
a__and' = a__isPLNat'
a__and' = a__natsFrom'
a__and' = a__tail'
a__isNatural' = a__isLNat'
a__isNatural' = a__isPLNat'
a__isNatural' = a__natsFrom'
a__isNatural' = a__tail'
a__isLNat' = a__isPLNat'
a__isLNat' = a__natsFrom'
a__isLNat' = a__tail'
a__isPLNat' = a__natsFrom'
a__isPLNat' = a__tail'
a__natsFrom' = a__tail'

Generator Equations:
_gen_tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'2(0) ⇔ tt'
_gen_tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'2(+(x, 1)) ⇔ cons'(_gen_tt':s':natsFrom':cons':nil':pair':isLNat':afterNth':fst':snd':tail':take':0':head':sel':splitAt':isNatural':and':U101':U11':U21':U31':U41':U51':U61':U71':U81':U82':U91':isPLNat'2(x), tt')

The following defined symbols remain to be analysed:
a__fst', a__U101', a__splitAt', mark', a__U11', a__snd', a__U21', a__U31', a__U41', a__U51', a__head', a__afterNth', a__U61', a__U71', a__U81', a__U82', a__U91', a__and', a__isNatural', a__isLNat', a__isPLNat', a__natsFrom', a__tail'

Could not prove a rewrite lemma for the defined symbol a__fst'.

The following defined symbols remain to be analysed:
a__U21', a__U101', a__splitAt', mark', a__U11', a__snd', a__U31', a__U41', a__U51', a__head', a__afterNth', a__U61', a__U71', a__U81', a__U82', a__U91', a__and', a__isNatural', a__isLNat', a__isPLNat', a__natsFrom', a__tail'