KILLED
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).

(0) CpxRelTRS


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   A__U101(tt, z0) -> c(A__U102(a__isLNat(z0)), A__ISLNAT(z0))
   A__U101(z0, z1) -> c1
   A__U102(tt) -> c2
   A__U102(z0) -> c3
   A__U11(tt, z0, z1) -> c4(A__U12(a__isLNat(z1), z0, z1), A__ISLNAT(z1))
   A__U11(z0, z1, z2) -> c5
   A__U111(tt) -> c6
   A__U111(z0) -> c7
   A__U12(tt, z0, z1) -> c8(A__SND(a__splitAt(mark(z0), mark(z1))), A__SPLITAT(mark(z0), mark(z1)), MARK(z0))
   A__U12(tt, z0, z1) -> c9(A__SND(a__splitAt(mark(z0), mark(z1))), A__SPLITAT(mark(z0), mark(z1)), MARK(z1))
   A__U12(z0, z1, z2) -> c10
   A__U121(tt) -> c11
   A__U121(z0) -> c12
   A__U131(tt, z0) -> c13(A__U132(a__isLNat(z0)), A__ISLNAT(z0))
   A__U131(z0, z1) -> c14
   A__U132(tt) -> c15
   A__U132(z0) -> c16
   A__U141(tt, z0) -> c17(A__U142(a__isLNat(z0)), A__ISLNAT(z0))
   A__U141(z0, z1) -> c18
   A__U142(tt) -> c19
   A__U142(z0) -> c20
   A__U151(tt, z0) -> c21(A__U152(a__isLNat(z0)), A__ISLNAT(z0))
   A__U151(z0, z1) -> c22
   A__U152(tt) -> c23
   A__U152(z0) -> c24
   A__U161(tt, z0) -> c25(MARK(z0))
   A__U161(z0, z1) -> c26
   A__U171(tt, z0, z1) -> c27(A__U172(a__isLNat(z1), z0, z1), A__ISLNAT(z1))
   A__U171(z0, z1, z2) -> c28
   A__U172(tt, z0, z1) -> c29(A__HEAD(a__afterNth(mark(z0), mark(z1))), A__AFTERNTH(mark(z0), mark(z1)), MARK(z0))
   A__U172(tt, z0, z1) -> c30(A__HEAD(a__afterNth(mark(z0), mark(z1))), A__AFTERNTH(mark(z0), mark(z1)), MARK(z1))
   A__U172(z0, z1, z2) -> c31
   A__U181(tt, z0) -> c32(A__U182(a__isLNat(z0), z0), A__ISLNAT(z0))
   A__U181(z0, z1) -> c33
   A__U182(tt, z0) -> c34(MARK(z0))
   A__U182(z0, z1) -> c35
   A__U191(tt, z0) -> c36(MARK(z0))
   A__U191(z0, z1) -> c37
   A__U201(tt, z0, z1, z2) -> c38(A__U202(a__isNatural(z1), z0, z1, z2), A__ISNATURAL(z1))
   A__U201(z0, z1, z2, z3) -> c39
   A__U202(tt, z0, z1, z2) -> c40(A__U203(a__isLNat(z2), z0, z1, z2), A__ISLNAT(z2))
   A__U202(z0, z1, z2, z3) -> c41
   A__U203(tt, z0, z1, z2) -> c42(A__U204(a__splitAt(mark(z0), mark(z2)), z1), A__SPLITAT(mark(z0), mark(z2)), MARK(z0))
   A__U203(tt, z0, z1, z2) -> c43(A__U204(a__splitAt(mark(z0), mark(z2)), z1), A__SPLITAT(mark(z0), mark(z2)), MARK(z2))
   A__U203(z0, z1, z2, z3) -> c44
   A__U204(pair(z0, z1), z2) -> c45(MARK(z2))
   A__U204(pair(z0, z1), z2) -> c46(MARK(z1))
   A__U204(z0, z1) -> c47
   A__U21(tt, z0, z1) -> c48(A__U22(a__isLNat(z1), z0), A__ISLNAT(z1))
   A__U21(z0, z1, z2) -> c49
   A__U211(tt, z0) -> c50(A__U212(a__isLNat(z0), z0), A__ISLNAT(z0))
   A__U211(z0, z1) -> c51
   A__U212(tt, z0) -> c52(MARK(z0))
   A__U212(z0, z1) -> c53
   A__U22(tt, z0) -> c54(MARK(z0))
   A__U22(z0, z1) -> c55
   A__U221(tt, z0, z1) -> c56(A__U222(a__isLNat(z1), z0, z1), A__ISLNAT(z1))
   A__U221(z0, z1, z2) -> c57
   A__U222(tt, z0, z1) -> c58(A__FST(a__splitAt(mark(z0), mark(z1))), A__SPLITAT(mark(z0), mark(z1)), MARK(z0))
   A__U222(tt, z0, z1) -> c59(A__FST(a__splitAt(mark(z0), mark(z1))), A__SPLITAT(mark(z0), mark(z1)), MARK(z1))
   A__U222(z0, z1, z2) -> c60
   A__U31(tt, z0, z1) -> c61(A__U32(a__isLNat(z1), z0), A__ISLNAT(z1))
   A__U31(z0, z1, z2) -> c62
   A__U32(tt, z0) -> c63(MARK(z0))
   A__U32(z0, z1) -> c64
   A__U41(tt, z0) -> c65(A__U42(a__isLNat(z0)), A__ISLNAT(z0))
   A__U41(z0, z1) -> c66
   A__U42(tt) -> c67
   A__U42(z0) -> c68
   A__U51(tt, z0) -> c69(A__U52(a__isLNat(z0)), A__ISLNAT(z0))
   A__U51(z0, z1) -> c70
   A__U52(tt) -> c71
   A__U52(z0) -> c72
   A__U61(tt) -> c73
   A__U61(z0) -> c74
   A__U71(tt) -> c75
   A__U71(z0) -> c76
   A__U81(tt) -> c77
   A__U81(z0) -> c78
   A__U91(tt) -> c79
   A__U91(z0) -> c80
   A__AFTERNTH(z0, z1) -> c81(A__U11(a__isNatural(z0), z0, z1), A__ISNATURAL(z0))
   A__AFTERNTH(z0, z1) -> c82
   A__FST(pair(z0, z1)) -> c83(A__U21(a__isLNat(z0), z0, z1), A__ISLNAT(z0))
   A__FST(z0) -> c84
   A__HEAD(cons(z0, z1)) -> c85(A__U31(a__isNatural(z0), z0, z1), A__ISNATURAL(z0))
   A__HEAD(z0) -> c86
   A__ISLNAT(nil) -> c87
   A__ISLNAT(afterNth(z0, z1)) -> c88(A__U41(a__isNatural(z0), z1), A__ISNATURAL(z0))
   A__ISLNAT(cons(z0, z1)) -> c89(A__U51(a__isNatural(z0), z1), A__ISNATURAL(z0))
   A__ISLNAT(fst(z0)) -> c90(A__U61(a__isPLNat(z0)), A__ISPLNAT(z0))
   A__ISLNAT(natsFrom(z0)) -> c91(A__U71(a__isNatural(z0)), A__ISNATURAL(z0))
   A__ISLNAT(snd(z0)) -> c92(A__U81(a__isPLNat(z0)), A__ISPLNAT(z0))
   A__ISLNAT(tail(z0)) -> c93(A__U91(a__isLNat(z0)), A__ISLNAT(z0))
   A__ISLNAT(take(z0, z1)) -> c94(A__U101(a__isNatural(z0), z1), A__ISNATURAL(z0))
   A__ISLNAT(z0) -> c95
   A__ISNATURAL(0) -> c96
   A__ISNATURAL(head(z0)) -> c97(A__U111(a__isLNat(z0)), A__ISLNAT(z0))
   A__ISNATURAL(s(z0)) -> c98(A__U121(a__isNatural(z0)), A__ISNATURAL(z0))
   A__ISNATURAL(sel(z0, z1)) -> c99(A__U131(a__isNatural(z0), z1), A__ISNATURAL(z0))
   A__ISNATURAL(z0) -> c100
   A__ISPLNAT(pair(z0, z1)) -> c101(A__U141(a__isLNat(z0), z1), A__ISLNAT(z0))
   A__ISPLNAT(splitAt(z0, z1)) -> c102(A__U151(a__isNatural(z0), z1), A__ISNATURAL(z0))
   A__ISPLNAT(z0) -> c103
   A__NATSFROM(z0) -> c104(A__U161(a__isNatural(z0), z0), A__ISNATURAL(z0))
   A__NATSFROM(z0) -> c105
   A__SEL(z0, z1) -> c106(A__U171(a__isNatural(z0), z0, z1), A__ISNATURAL(z0))
   A__SEL(z0, z1) -> c107
   A__SND(pair(z0, z1)) -> c108(A__U181(a__isLNat(z0), z1), A__ISLNAT(z0))
   A__SND(z0) -> c109
   A__SPLITAT(0, z0) -> c110(A__U191(a__isLNat(z0), z0), A__ISLNAT(z0))
   A__SPLITAT(s(z0), cons(z1, z2)) -> c111(A__U201(a__isNatural(z0), z0, z1, z2), A__ISNATURAL(z0))
   A__SPLITAT(z0, z1) -> c112
   A__TAIL(cons(z0, z1)) -> c113(A__U211(a__isNatural(z0), z1), A__ISNATURAL(z0))
   A__TAIL(z0) -> c114
   A__TAKE(z0, z1) -> c115(A__U221(a__isNatural(z0), z0, z1), A__ISNATURAL(z0))
   A__TAKE(z0, z1) -> c116
   MARK(U101(z0, z1)) -> c117(A__U101(mark(z0), z1), MARK(z0))
   MARK(U102(z0)) -> c118(A__U102(mark(z0)), MARK(z0))
   MARK(isLNat(z0)) -> c119(A__ISLNAT(z0))
   MARK(U11(z0, z1, z2)) -> c120(A__U11(mark(z0), z1, z2), MARK(z0))
   MARK(U12(z0, z1, z2)) -> c121(A__U12(mark(z0), z1, z2), MARK(z0))
   MARK(U111(z0)) -> c122(A__U111(mark(z0)), MARK(z0))
   MARK(snd(z0)) -> c123(A__SND(mark(z0)), MARK(z0))
   MARK(splitAt(z0, z1)) -> c124(A__SPLITAT(mark(z0), mark(z1)), MARK(z0))
   MARK(splitAt(z0, z1)) -> c125(A__SPLITAT(mark(z0), mark(z1)), MARK(z1))
   MARK(U121(z0)) -> c126(A__U121(mark(z0)), MARK(z0))
   MARK(U131(z0, z1)) -> c127(A__U131(mark(z0), z1), MARK(z0))
   MARK(U132(z0)) -> c128(A__U132(mark(z0)), MARK(z0))
   MARK(U141(z0, z1)) -> c129(A__U141(mark(z0), z1), MARK(z0))
   MARK(U142(z0)) -> c130(A__U142(mark(z0)), MARK(z0))
   MARK(U151(z0, z1)) -> c131(A__U151(mark(z0), z1), MARK(z0))
   MARK(U152(z0)) -> c132(A__U152(mark(z0)), MARK(z0))
   MARK(U161(z0, z1)) -> c133(A__U161(mark(z0), z1), MARK(z0))
   MARK(natsFrom(z0)) -> c134(A__NATSFROM(mark(z0)), MARK(z0))
   MARK(U171(z0, z1, z2)) -> c135(A__U171(mark(z0), z1, z2), MARK(z0))
   MARK(U172(z0, z1, z2)) -> c136(A__U172(mark(z0), z1, z2), MARK(z0))
   MARK(head(z0)) -> c137(A__HEAD(mark(z0)), MARK(z0))
   MARK(afterNth(z0, z1)) -> c138(A__AFTERNTH(mark(z0), mark(z1)), MARK(z0))
   MARK(afterNth(z0, z1)) -> c139(A__AFTERNTH(mark(z0), mark(z1)), MARK(z1))
   MARK(U181(z0, z1)) -> c140(A__U181(mark(z0), z1), MARK(z0))
   MARK(U182(z0, z1)) -> c141(A__U182(mark(z0), z1), MARK(z0))
   MARK(U191(z0, z1)) -> c142(A__U191(mark(z0), z1), MARK(z0))
   MARK(U201(z0, z1, z2, z3)) -> c143(A__U201(mark(z0), z1, z2, z3), MARK(z0))
   MARK(U202(z0, z1, z2, z3)) -> c144(A__U202(mark(z0), z1, z2, z3), MARK(z0))
   MARK(isNatural(z0)) -> c145(A__ISNATURAL(z0))
   MARK(U203(z0, z1, z2, z3)) -> c146(A__U203(mark(z0), z1, z2, z3), MARK(z0))
   MARK(U204(z0, z1)) -> c147(A__U204(mark(z0), z1), MARK(z0))
   MARK(U21(z0, z1, z2)) -> c148(A__U21(mark(z0), z1, z2), MARK(z0))
   MARK(U22(z0, z1)) -> c149(A__U22(mark(z0), z1), MARK(z0))
   MARK(U211(z0, z1)) -> c150(A__U211(mark(z0), z1), MARK(z0))
   MARK(U212(z0, z1)) -> c151(A__U212(mark(z0), z1), MARK(z0))
   MARK(U221(z0, z1, z2)) -> c152(A__U221(mark(z0), z1, z2), MARK(z0))
   MARK(U222(z0, z1, z2)) -> c153(A__U222(mark(z0), z1, z2), MARK(z0))
   MARK(fst(z0)) -> c154(A__FST(mark(z0)), MARK(z0))
   MARK(U31(z0, z1, z2)) -> c155(A__U31(mark(z0), z1, z2), MARK(z0))
   MARK(U32(z0, z1)) -> c156(A__U32(mark(z0), z1), MARK(z0))
   MARK(U41(z0, z1)) -> c157(A__U41(mark(z0), z1), MARK(z0))
   MARK(U42(z0)) -> c158(A__U42(mark(z0)), MARK(z0))
   MARK(U51(z0, z1)) -> c159(A__U51(mark(z0), z1), MARK(z0))
   MARK(U52(z0)) -> c160(A__U52(mark(z0)), MARK(z0))
   MARK(U61(z0)) -> c161(A__U61(mark(z0)), MARK(z0))
   MARK(U71(z0)) -> c162(A__U71(mark(z0)), MARK(z0))
   MARK(U81(z0)) -> c163(A__U81(mark(z0)), MARK(z0))
   MARK(U91(z0)) -> c164(A__U91(mark(z0)), MARK(z0))
   MARK(isPLNat(z0)) -> c165(A__ISPLNAT(z0))
   MARK(tail(z0)) -> c166(A__TAIL(mark(z0)), MARK(z0))
   MARK(take(z0, z1)) -> c167(A__TAKE(mark(z0), mark(z1)), MARK(z0))
   MARK(take(z0, z1)) -> c168(A__TAKE(mark(z0), mark(z1)), MARK(z1))
   MARK(sel(z0, z1)) -> c169(A__SEL(mark(z0), mark(z1)), MARK(z0))
   MARK(sel(z0, z1)) -> c170(A__SEL(mark(z0), mark(z1)), MARK(z1))
   MARK(tt) -> c171
   MARK(cons(z0, z1)) -> c172(MARK(z0))
   MARK(s(z0)) -> c173(MARK(z0))
   MARK(pair(z0, z1)) -> c174(MARK(z0))
   MARK(pair(z0, z1)) -> c175(MARK(z1))
   MARK(nil) -> c176
   MARK(0) -> c177

The (relative) TRS S consists of the following rules:

   a__U101(tt, z0) -> a__U102(a__isLNat(z0))
   a__U101(z0, z1) -> U101(z0, z1)
   a__U102(tt) -> tt
   a__U102(z0) -> U102(z0)
   a__U11(tt, z0, z1) -> a__U12(a__isLNat(z1), z0, z1)
   a__U11(z0, z1, z2) -> U11(z0, z1, z2)
   a__U111(tt) -> tt
   a__U111(z0) -> U111(z0)
   a__U12(tt, z0, z1) -> a__snd(a__splitAt(mark(z0), mark(z1)))
   a__U12(z0, z1, z2) -> U12(z0, z1, z2)
   a__U121(tt) -> tt
   a__U121(z0) -> U121(z0)
   a__U131(tt, z0) -> a__U132(a__isLNat(z0))
   a__U131(z0, z1) -> U131(z0, z1)
   a__U132(tt) -> tt
   a__U132(z0) -> U132(z0)
   a__U141(tt, z0) -> a__U142(a__isLNat(z0))
   a__U141(z0, z1) -> U141(z0, z1)
   a__U142(tt) -> tt
   a__U142(z0) -> U142(z0)
   a__U151(tt, z0) -> a__U152(a__isLNat(z0))
   a__U151(z0, z1) -> U151(z0, z1)
   a__U152(tt) -> tt
   a__U152(z0) -> U152(z0)
   a__U161(tt, z0) -> cons(mark(z0), natsFrom(s(z0)))
   a__U161(z0, z1) -> U161(z0, z1)
   a__U171(tt, z0, z1) -> a__U172(a__isLNat(z1), z0, z1)
   a__U171(z0, z1, z2) -> U171(z0, z1, z2)
   a__U172(tt, z0, z1) -> a__head(a__afterNth(mark(z0), mark(z1)))
   a__U172(z0, z1, z2) -> U172(z0, z1, z2)
   a__U181(tt, z0) -> a__U182(a__isLNat(z0), z0)
   a__U181(z0, z1) -> U181(z0, z1)
   a__U182(tt, z0) -> mark(z0)
   a__U182(z0, z1) -> U182(z0, z1)
   a__U191(tt, z0) -> pair(nil, mark(z0))
   a__U191(z0, z1) -> U191(z0, z1)
   a__U201(tt, z0, z1, z2) -> a__U202(a__isNatural(z1), z0, z1, z2)
   a__U201(z0, z1, z2, z3) -> U201(z0, z1, z2, z3)
   a__U202(tt, z0, z1, z2) -> a__U203(a__isLNat(z2), z0, z1, z2)
   a__U202(z0, z1, z2, z3) -> U202(z0, z1, z2, z3)
   a__U203(tt, z0, z1, z2) -> a__U204(a__splitAt(mark(z0), mark(z2)), z1)
   a__U203(z0, z1, z2, z3) -> U203(z0, z1, z2, z3)
   a__U204(pair(z0, z1), z2) -> pair(cons(mark(z2), z0), mark(z1))
   a__U204(z0, z1) -> U204(z0, z1)
   a__U21(tt, z0, z1) -> a__U22(a__isLNat(z1), z0)
   a__U21(z0, z1, z2) -> U21(z0, z1, z2)
   a__U211(tt, z0) -> a__U212(a__isLNat(z0), z0)
   a__U211(z0, z1) -> U211(z0, z1)
   a__U212(tt, z0) -> mark(z0)
   a__U212(z0, z1) -> U212(z0, z1)
   a__U22(tt, z0) -> mark(z0)
   a__U22(z0, z1) -> U22(z0, z1)
   a__U221(tt, z0, z1) -> a__U222(a__isLNat(z1), z0, z1)
   a__U221(z0, z1, z2) -> U221(z0, z1, z2)
   a__U222(tt, z0, z1) -> a__fst(a__splitAt(mark(z0), mark(z1)))
   a__U222(z0, z1, z2) -> U222(z0, z1, z2)
   a__U31(tt, z0, z1) -> a__U32(a__isLNat(z1), z0)
   a__U31(z0, z1, z2) -> U31(z0, z1, z2)
   a__U32(tt, z0) -> mark(z0)
   a__U32(z0, z1) -> U32(z0, z1)
   a__U41(tt, z0) -> a__U42(a__isLNat(z0))
   a__U41(z0, z1) -> U41(z0, z1)
   a__U42(tt) -> tt
   a__U42(z0) -> U42(z0)
   a__U51(tt, z0) -> a__U52(a__isLNat(z0))
   a__U51(z0, z1) -> U51(z0, z1)
   a__U52(tt) -> tt
   a__U52(z0) -> U52(z0)
   a__U61(tt) -> tt
   a__U61(z0) -> U61(z0)
   a__U71(tt) -> tt
   a__U71(z0) -> U71(z0)
   a__U81(tt) -> tt
   a__U81(z0) -> U81(z0)
   a__U91(tt) -> tt
   a__U91(z0) -> U91(z0)
   a__afterNth(z0, z1) -> a__U11(a__isNatural(z0), z0, z1)
   a__afterNth(z0, z1) -> afterNth(z0, z1)
   a__fst(pair(z0, z1)) -> a__U21(a__isLNat(z0), z0, z1)
   a__fst(z0) -> fst(z0)
   a__head(cons(z0, z1)) -> a__U31(a__isNatural(z0), z0, z1)
   a__head(z0) -> head(z0)
   a__isLNat(nil) -> tt
   a__isLNat(afterNth(z0, z1)) -> a__U41(a__isNatural(z0), z1)
   a__isLNat(cons(z0, z1)) -> a__U51(a__isNatural(z0), z1)
   a__isLNat(fst(z0)) -> a__U61(a__isPLNat(z0))
   a__isLNat(natsFrom(z0)) -> a__U71(a__isNatural(z0))
   a__isLNat(snd(z0)) -> a__U81(a__isPLNat(z0))
   a__isLNat(tail(z0)) -> a__U91(a__isLNat(z0))
   a__isLNat(take(z0, z1)) -> a__U101(a__isNatural(z0), z1)
   a__isLNat(z0) -> isLNat(z0)
   a__isNatural(0) -> tt
   a__isNatural(head(z0)) -> a__U111(a__isLNat(z0))
   a__isNatural(s(z0)) -> a__U121(a__isNatural(z0))
   a__isNatural(sel(z0, z1)) -> a__U131(a__isNatural(z0), z1)
   a__isNatural(z0) -> isNatural(z0)
   a__isPLNat(pair(z0, z1)) -> a__U141(a__isLNat(z0), z1)
   a__isPLNat(splitAt(z0, z1)) -> a__U151(a__isNatural(z0), z1)
   a__isPLNat(z0) -> isPLNat(z0)
   a__natsFrom(z0) -> a__U161(a__isNatural(z0), z0)
   a__natsFrom(z0) -> natsFrom(z0)
   a__sel(z0, z1) -> a__U171(a__isNatural(z0), z0, z1)
   a__sel(z0, z1) -> sel(z0, z1)
   a__snd(pair(z0, z1)) -> a__U181(a__isLNat(z0), z1)
   a__snd(z0) -> snd(z0)
   a__splitAt(0, z0) -> a__U191(a__isLNat(z0), z0)
   a__splitAt(s(z0), cons(z1, z2)) -> a__U201(a__isNatural(z0), z0, z1, z2)
   a__splitAt(z0, z1) -> splitAt(z0, z1)
   a__tail(cons(z0, z1)) -> a__U211(a__isNatural(z0), z1)
   a__tail(z0) -> tail(z0)
   a__take(z0, z1) -> a__U221(a__isNatural(z0), z0, z1)
   a__take(z0, z1) -> take(z0, z1)
   mark(U101(z0, z1)) -> a__U101(mark(z0), z1)
   mark(U102(z0)) -> a__U102(mark(z0))
   mark(isLNat(z0)) -> a__isLNat(z0)
   mark(U11(z0, z1, z2)) -> a__U11(mark(z0), z1, z2)
   mark(U12(z0, z1, z2)) -> a__U12(mark(z0), z1, z2)
   mark(U111(z0)) -> a__U111(mark(z0))
   mark(snd(z0)) -> a__snd(mark(z0))
   mark(splitAt(z0, z1)) -> a__splitAt(mark(z0), mark(z1))
   mark(U121(z0)) -> a__U121(mark(z0))
   mark(U131(z0, z1)) -> a__U131(mark(z0), z1)
   mark(U132(z0)) -> a__U132(mark(z0))
   mark(U141(z0, z1)) -> a__U141(mark(z0), z1)
   mark(U142(z0)) -> a__U142(mark(z0))
   mark(U151(z0, z1)) -> a__U151(mark(z0), z1)
   mark(U152(z0)) -> a__U152(mark(z0))
   mark(U161(z0, z1)) -> a__U161(mark(z0), z1)
   mark(natsFrom(z0)) -> a__natsFrom(mark(z0))
   mark(U171(z0, z1, z2)) -> a__U171(mark(z0), z1, z2)
   mark(U172(z0, z1, z2)) -> a__U172(mark(z0), z1, z2)
   mark(head(z0)) -> a__head(mark(z0))
   mark(afterNth(z0, z1)) -> a__afterNth(mark(z0), mark(z1))
   mark(U181(z0, z1)) -> a__U181(mark(z0), z1)
   mark(U182(z0, z1)) -> a__U182(mark(z0), z1)
   mark(U191(z0, z1)) -> a__U191(mark(z0), z1)
   mark(U201(z0, z1, z2, z3)) -> a__U201(mark(z0), z1, z2, z3)
   mark(U202(z0, z1, z2, z3)) -> a__U202(mark(z0), z1, z2, z3)
   mark(isNatural(z0)) -> a__isNatural(z0)
   mark(U203(z0, z1, z2, z3)) -> a__U203(mark(z0), z1, z2, z3)
   mark(U204(z0, z1)) -> a__U204(mark(z0), z1)
   mark(U21(z0, z1, z2)) -> a__U21(mark(z0), z1, z2)
   mark(U22(z0, z1)) -> a__U22(mark(z0), z1)
   mark(U211(z0, z1)) -> a__U211(mark(z0), z1)
   mark(U212(z0, z1)) -> a__U212(mark(z0), z1)
   mark(U221(z0, z1, z2)) -> a__U221(mark(z0), z1, z2)
   mark(U222(z0, z1, z2)) -> a__U222(mark(z0), z1, z2)
   mark(fst(z0)) -> a__fst(mark(z0))
   mark(U31(z0, z1, z2)) -> a__U31(mark(z0), z1, z2)
   mark(U32(z0, z1)) -> a__U32(mark(z0), z1)
   mark(U41(z0, z1)) -> a__U41(mark(z0), z1)
   mark(U42(z0)) -> a__U42(mark(z0))
   mark(U51(z0, z1)) -> a__U51(mark(z0), z1)
   mark(U52(z0)) -> a__U52(mark(z0))
   mark(U61(z0)) -> a__U61(mark(z0))
   mark(U71(z0)) -> a__U71(mark(z0))
   mark(U81(z0)) -> a__U81(mark(z0))
   mark(U91(z0)) -> a__U91(mark(z0))
   mark(isPLNat(z0)) -> a__isPLNat(z0)
   mark(tail(z0)) -> a__tail(mark(z0))
   mark(take(z0, z1)) -> a__take(mark(z0), mark(z1))
   mark(sel(z0, z1)) -> a__sel(mark(z0), mark(z1))
   mark(tt) -> tt
   mark(cons(z0, z1)) -> cons(mark(z0), z1)
   mark(s(z0)) -> s(mark(z0))
   mark(pair(z0, z1)) -> pair(mark(z0), mark(z1))
   mark(nil) -> nil
   mark(0) -> 0

Rewrite Strategy: INNERMOST