WORST_CASE(Omega(n^1),O(n^1))
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(n^1, n^1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 350 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (12) CdtProblem
    (13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 50 ms]
    (16) CdtProblem
    (17) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) BOUNDS(1, 1)
(19) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(20) TRS for Loop Detection
    (21) DecreasingLoopProof [LOWER BOUND(ID), 42 ms]
    (22) BEST
        (23) proven lower bound
            (24) LowerBoundPropagationProof [FINISHED, 0 ms]
            (25) BOUNDS(n^1, INF)
        (26) TRS for Loop Detection


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

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


The TRS R consists of the following rules:

   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14

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

   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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


The TRS R consists of the following rules:

   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14

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

   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0

Rewrite Strategy: INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14
Tuples:
   NATSFROM'(z0) -> c15
   NATSFROM'(z0) -> c16
   FST'(pair(z0, z1)) -> c17
   SND'(pair(z0, z1)) -> c18
   SPLITAT'(0, z0) -> c19
   SPLITAT'(s(z0), cons(z1, z2)) -> c20(U'(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2))
   U'(pair(z0, z1), z2, z3, z4) -> c21(ACTIVATE'(z3))
   HEAD'(cons(z0, z1)) -> c22
   TAIL'(cons(z0, z1)) -> c23(ACTIVATE'(z1))
   SEL'(z0, z1) -> c24(HEAD'(afterNth(z0, z1)), AFTERNTH'(z0, z1))
   TAKE'(z0, z1) -> c25(FST'(splitAt(z0, z1)), SPLITAT'(z0, z1))
   AFTERNTH'(z0, z1) -> c26(SND'(splitAt(z0, z1)), SPLITAT'(z0, z1))
   ACTIVATE'(n__natsFrom(z0)) -> c27(NATSFROM'(z0))
   ACTIVATE'(z0) -> c28
   NATSFROM''(z0) -> c29
   NATSFROM''(z0) -> c30
   FST''(pair(z0, z1)) -> c31
   SND''(pair(z0, z1)) -> c32
   SPLITAT''(0, z0) -> c33
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(U''(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2), SPLITAT''(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(U''(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2), ACTIVATE''(z2))
   U''(pair(z0, z1), z2, z3, z4) -> c36(ACTIVATE''(z3))
   HEAD''(cons(z0, z1)) -> c37
   TAIL''(cons(z0, z1)) -> c38(ACTIVATE''(z1))
   SEL''(z0, z1) -> c39(HEAD''(afterNth(z0, z1)), AFTERNTH'(z0, z1), AFTERNTH''(z0, z1))
   TAKE''(z0, z1) -> c40(FST''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1))
   AFTERNTH''(z0, z1) -> c41(SND''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1))
   ACTIVATE''(n__natsFrom(z0)) -> c42(NATSFROM''(z0))
   ACTIVATE''(z0) -> c43
S tuples:
   NATSFROM''(z0) -> c29
   NATSFROM''(z0) -> c30
   FST''(pair(z0, z1)) -> c31
   SND''(pair(z0, z1)) -> c32
   SPLITAT''(0, z0) -> c33
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(U''(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2), SPLITAT''(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(U''(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2), ACTIVATE''(z2))
   U''(pair(z0, z1), z2, z3, z4) -> c36(ACTIVATE''(z3))
   HEAD''(cons(z0, z1)) -> c37
   TAIL''(cons(z0, z1)) -> c38(ACTIVATE''(z1))
   SEL''(z0, z1) -> c39(HEAD''(afterNth(z0, z1)), AFTERNTH'(z0, z1), AFTERNTH''(z0, z1))
   TAKE''(z0, z1) -> c40(FST''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1))
   AFTERNTH''(z0, z1) -> c41(SND''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1))
   ACTIVATE''(n__natsFrom(z0)) -> c42(NATSFROM''(z0))
   ACTIVATE''(z0) -> c43
K tuples:none
Defined Rule Symbols:   NATSFROM_1, FST_1, SND_1, SPLITAT_2, U_4, HEAD_1, TAIL_1, SEL_2, TAKE_2, AFTERNTH_2, ACTIVATE_1, natsFrom_1, fst_1, snd_1, splitAt_2, u_4, head_1, tail_1, sel_2, take_2, afterNth_2, activate_1

Defined Pair Symbols:   NATSFROM'_1, FST'_1, SND'_1, SPLITAT'_2, U'_4, HEAD'_1, TAIL'_1, SEL'_2, TAKE'_2, AFTERNTH'_2, ACTIVATE'_1, NATSFROM''_1, FST''_1, SND''_1, SPLITAT''_2, U''_4, HEAD''_1, TAIL''_1, SEL''_2, TAKE''_2, AFTERNTH''_2, ACTIVATE''_1

Compound Symbols:   c15, c16, c17, c18, c19, c20_4, c21_1, c22, c23_1, c24_2, c25_2, c26_2, c27_1, c28, c29, c30, c31, c32, c33, c34_7, c35_5, c36_1, c37, c38_1, c39_3, c40_3, c41_3, c42_1, c43


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 20 trailing nodes:
   NATSFROM''(z0) -> c29
   NATSFROM'(z0) -> c16
   HEAD''(cons(z0, z1)) -> c37
   TAIL''(cons(z0, z1)) -> c38(ACTIVATE''(z1))
   HEAD'(cons(z0, z1)) -> c22
   NATSFROM''(z0) -> c30
   FST''(pair(z0, z1)) -> c31
   SPLITAT'(0, z0) -> c19
   U''(pair(z0, z1), z2, z3, z4) -> c36(ACTIVATE''(z3))
   SND'(pair(z0, z1)) -> c18
   U'(pair(z0, z1), z2, z3, z4) -> c21(ACTIVATE'(z3))
   NATSFROM'(z0) -> c15
   ACTIVATE'(n__natsFrom(z0)) -> c27(NATSFROM'(z0))
   ACTIVATE'(z0) -> c28
   ACTIVATE''(n__natsFrom(z0)) -> c42(NATSFROM''(z0))
   TAIL'(cons(z0, z1)) -> c23(ACTIVATE'(z1))
   SND''(pair(z0, z1)) -> c32
   FST'(pair(z0, z1)) -> c17
   SPLITAT''(0, z0) -> c33
   ACTIVATE''(z0) -> c43

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14
Tuples:
   SPLITAT'(s(z0), cons(z1, z2)) -> c20(U'(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2))
   SEL'(z0, z1) -> c24(HEAD'(afterNth(z0, z1)), AFTERNTH'(z0, z1))
   TAKE'(z0, z1) -> c25(FST'(splitAt(z0, z1)), SPLITAT'(z0, z1))
   AFTERNTH'(z0, z1) -> c26(SND'(splitAt(z0, z1)), SPLITAT'(z0, z1))
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(U''(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2), SPLITAT''(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(U''(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2), ACTIVATE''(z2))
   SEL''(z0, z1) -> c39(HEAD''(afterNth(z0, z1)), AFTERNTH'(z0, z1), AFTERNTH''(z0, z1))
   TAKE''(z0, z1) -> c40(FST''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1))
   AFTERNTH''(z0, z1) -> c41(SND''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1))
S tuples:
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(U''(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2), SPLITAT''(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE''(z2))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(U''(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT'(z0, activate(z2)), ACTIVATE'(z2), ACTIVATE'(z2), ACTIVATE''(z2))
   SEL''(z0, z1) -> c39(HEAD''(afterNth(z0, z1)), AFTERNTH'(z0, z1), AFTERNTH''(z0, z1))
   TAKE''(z0, z1) -> c40(FST''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1))
   AFTERNTH''(z0, z1) -> c41(SND''(splitAt(z0, z1)), SPLITAT'(z0, z1), SPLITAT''(z0, z1))
K tuples:none
Defined Rule Symbols:   NATSFROM_1, FST_1, SND_1, SPLITAT_2, U_4, HEAD_1, TAIL_1, SEL_2, TAKE_2, AFTERNTH_2, ACTIVATE_1, natsFrom_1, fst_1, snd_1, splitAt_2, u_4, head_1, tail_1, sel_2, take_2, afterNth_2, activate_1

Defined Pair Symbols:   SPLITAT'_2, SEL'_2, TAKE'_2, AFTERNTH'_2, SPLITAT''_2, SEL''_2, TAKE''_2, AFTERNTH''_2

Compound Symbols:   c20_4, c24_2, c25_2, c26_2, c34_7, c35_5, c39_3, c40_3, c41_3


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

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 18 trailing tuple parts
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14
Tuples:
   SPLITAT'(s(z0), cons(z1, z2)) -> c20(SPLITAT'(z0, activate(z2)))
   SEL'(z0, z1) -> c24(AFTERNTH'(z0, z1))
   TAKE'(z0, z1) -> c25(SPLITAT'(z0, z1))
   AFTERNTH'(z0, z1) -> c26(SPLITAT'(z0, z1))
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
   SEL''(z0, z1) -> c39(AFTERNTH'(z0, z1), AFTERNTH''(z0, z1))
   TAKE''(z0, z1) -> c40(SPLITAT'(z0, z1), SPLITAT''(z0, z1))
   AFTERNTH''(z0, z1) -> c41(SPLITAT'(z0, z1), SPLITAT''(z0, z1))
S tuples:
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
   SEL''(z0, z1) -> c39(AFTERNTH'(z0, z1), AFTERNTH''(z0, z1))
   TAKE''(z0, z1) -> c40(SPLITAT'(z0, z1), SPLITAT''(z0, z1))
   AFTERNTH''(z0, z1) -> c41(SPLITAT'(z0, z1), SPLITAT''(z0, z1))
K tuples:none
Defined Rule Symbols:   NATSFROM_1, FST_1, SND_1, SPLITAT_2, U_4, HEAD_1, TAIL_1, SEL_2, TAKE_2, AFTERNTH_2, ACTIVATE_1, natsFrom_1, fst_1, snd_1, splitAt_2, u_4, head_1, tail_1, sel_2, take_2, afterNth_2, activate_1

Defined Pair Symbols:   SPLITAT'_2, SEL'_2, TAKE'_2, AFTERNTH'_2, SPLITAT''_2, SEL''_2, TAKE''_2, AFTERNTH''_2

Compound Symbols:   c20_1, c24_1, c25_1, c26_1, c34_2, c35_1, c39_2, c40_2, c41_2


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

(9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14
Tuples:
   SPLITAT'(s(z0), cons(z1, z2)) -> c20(SPLITAT'(z0, activate(z2)))
   SEL'(z0, z1) -> c24(AFTERNTH'(z0, z1))
   TAKE'(z0, z1) -> c25(SPLITAT'(z0, z1))
   AFTERNTH'(z0, z1) -> c26(SPLITAT'(z0, z1))
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
   SEL''(z0, z1) -> c15(AFTERNTH'(z0, z1))
   SEL''(z0, z1) -> c15(AFTERNTH''(z0, z1))
   TAKE''(z0, z1) -> c15(SPLITAT'(z0, z1))
   TAKE''(z0, z1) -> c15(SPLITAT''(z0, z1))
   AFTERNTH''(z0, z1) -> c15(SPLITAT'(z0, z1))
   AFTERNTH''(z0, z1) -> c15(SPLITAT''(z0, z1))
S tuples:
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
   SEL''(z0, z1) -> c15(AFTERNTH'(z0, z1))
   SEL''(z0, z1) -> c15(AFTERNTH''(z0, z1))
   TAKE''(z0, z1) -> c15(SPLITAT'(z0, z1))
   TAKE''(z0, z1) -> c15(SPLITAT''(z0, z1))
   AFTERNTH''(z0, z1) -> c15(SPLITAT'(z0, z1))
   AFTERNTH''(z0, z1) -> c15(SPLITAT''(z0, z1))
K tuples:none
Defined Rule Symbols:   NATSFROM_1, FST_1, SND_1, SPLITAT_2, U_4, HEAD_1, TAIL_1, SEL_2, TAKE_2, AFTERNTH_2, ACTIVATE_1, natsFrom_1, fst_1, snd_1, splitAt_2, u_4, head_1, tail_1, sel_2, take_2, afterNth_2, activate_1

Defined Pair Symbols:   SPLITAT'_2, SEL'_2, TAKE'_2, AFTERNTH'_2, SPLITAT''_2, SEL''_2, TAKE''_2, AFTERNTH''_2

Compound Symbols:   c20_1, c24_1, c25_1, c26_1, c34_2, c35_1, c15_1


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

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 9 leading nodes:
   TAKE'(z0, z1) -> c25(SPLITAT'(z0, z1))
   SEL'(z0, z1) -> c24(AFTERNTH'(z0, z1))
   SEL''(z0, z1) -> c15(AFTERNTH'(z0, z1))
   AFTERNTH'(z0, z1) -> c26(SPLITAT'(z0, z1))
   TAKE''(z0, z1) -> c15(SPLITAT''(z0, z1))
   SEL''(z0, z1) -> c15(AFTERNTH''(z0, z1))
   AFTERNTH''(z0, z1) -> c15(SPLITAT''(z0, z1))
   TAKE''(z0, z1) -> c15(SPLITAT'(z0, z1))
   AFTERNTH''(z0, z1) -> c15(SPLITAT'(z0, z1))

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14
Tuples:
   SPLITAT'(s(z0), cons(z1, z2)) -> c20(SPLITAT'(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
S tuples:
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
K tuples:none
Defined Rule Symbols:   NATSFROM_1, FST_1, SND_1, SPLITAT_2, U_4, HEAD_1, TAIL_1, SEL_2, TAKE_2, AFTERNTH_2, ACTIVATE_1, natsFrom_1, fst_1, snd_1, splitAt_2, u_4, head_1, tail_1, sel_2, take_2, afterNth_2, activate_1

Defined Pair Symbols:   SPLITAT'_2, SPLITAT''_2

Compound Symbols:   c20_1, c34_2, c35_1


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

(13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
Tuples:
   SPLITAT'(s(z0), cons(z1, z2)) -> c20(SPLITAT'(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
S tuples:
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
K tuples:none
Defined Rule Symbols:   activate_1, natsFrom_1

Defined Pair Symbols:   SPLITAT'_2, SPLITAT''_2

Compound Symbols:   c20_1, c34_2, c35_1


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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
We considered the (Usable) Rules:
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   natsFrom(z0) -> n__natsFrom(z0)
And the Tuples:
   SPLITAT'(s(z0), cons(z1, z2)) -> c20(SPLITAT'(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(SPLITAT'(x_1, x_2)) = 0
   POL(SPLITAT''(x_1, x_2)) = [1] + x_1 + x_2
   POL(activate(x_1)) = [1] + x_1
   POL(c20(x_1)) = x_1
   POL(c34(x_1, x_2)) = x_1 + x_2
   POL(c35(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_2
   POL(n__natsFrom(x_1)) = 0
   POL(natsFrom(x_1)) = [1]
   POL(s(x_1)) = [1] + x_1

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
Tuples:
   SPLITAT'(s(z0), cons(z1, z2)) -> c20(SPLITAT'(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
S tuples:none
K tuples:
   SPLITAT''(s(z0), cons(z1, z2)) -> c34(SPLITAT'(z0, activate(z2)), SPLITAT''(z0, activate(z2)))
   SPLITAT''(s(z0), cons(z1, z2)) -> c35(SPLITAT'(z0, activate(z2)))
Defined Rule Symbols:   activate_1, natsFrom_1

Defined Pair Symbols:   SPLITAT'_2, SPLITAT''_2

Compound Symbols:   c20_1, c34_2, c35_1


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

(17) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(18)
BOUNDS(1, 1)

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

(19) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(20)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14

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

   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0

Rewrite Strategy: INNERMOST
----------------------------------------

(21) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

SPLITAT(s(z0), cons(z1, z2)) ->^+ c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, z2), ACTIVATE(z2))

gives rise to a decreasing loop by considering the right hand sides subterm at position [1].

The pumping substitution is [z0 / s(z0), z2 / cons(z1, z2)].

The result substitution is [ ].




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

(22)
Complex Obligation (BEST)

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

(23)
Obligation:
Proved the lower bound n^1 for the following obligation:

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


The TRS R consists of the following rules:

   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14

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

   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0

Rewrite Strategy: INNERMOST
----------------------------------------

(24) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(25)
BOUNDS(n^1, INF)

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

(26)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   NATSFROM(z0) -> c
   NATSFROM(z0) -> c1
   FST(pair(z0, z1)) -> c2
   SND(pair(z0, z1)) -> c3
   SPLITAT(0, z0) -> c4
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   SEL(z0, z1) -> c10(HEAD(afterNth(z0, z1)), AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(FST(splitAt(z0, z1)), SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SND(splitAt(z0, z1)), SPLITAT(z0, z1))
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   ACTIVATE(z0) -> c14

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

   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)
   fst(pair(z0, z1)) -> z0
   snd(pair(z0, z1)) -> z1
   splitAt(0, z0) -> pair(nil, z0)
   splitAt(s(z0), cons(z1, z2)) -> u(splitAt(z0, activate(z2)), z0, z1, activate(z2))
   u(pair(z0, z1), z2, z3, z4) -> pair(cons(activate(z3), z0), z1)
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> activate(z1)
   sel(z0, z1) -> head(afterNth(z0, z1))
   take(z0, z1) -> fst(splitAt(z0, z1))
   afterNth(z0, z1) -> snd(splitAt(z0, z1))
   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0

Rewrite Strategy: INNERMOST