WORST_CASE(?,O(n^1))
proof of input_a9WUBT4umm.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
(8) CdtProblem
(9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CdtProblem
(11) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CpxRelTRS
(13) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxWeightedTrs
(15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(16) CpxTypedWeightedTrs
(17) CompletionProof [UPPER BOUND(ID), 0 ms]
(18) CpxTypedWeightedCompleteTrs
(19) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CpxTypedWeightedCompleteTrs
(21) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(22) CpxRNTS
(23) InliningProof [UPPER BOUND(ID), 64 ms]
(24) CpxRNTS
(25) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
(26) CpxRNTS
(27) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
(28) CpxRNTS
(29) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(30) CpxRNTS
(31) IntTrsBoundProof [UPPER BOUND(ID), 170 ms]
(32) CpxRNTS
(33) IntTrsBoundProof [UPPER BOUND(ID), 2 ms]
(34) CpxRNTS
(35) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(36) CpxRNTS
(37) IntTrsBoundProof [UPPER BOUND(ID), 303 ms]
(38) CpxRNTS
(39) IntTrsBoundProof [UPPER BOUND(ID), 43 ms]
(40) CpxRNTS
(41) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(42) CpxRNTS
(43) IntTrsBoundProof [UPPER BOUND(ID), 468 ms]
(44) CpxRNTS
(45) IntTrsBoundProof [UPPER BOUND(ID), 208 ms]
(46) CpxRNTS
(47) FinalProof [FINISHED, 0 ms]
(48) BOUNDS(1, n^1)


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

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


The TRS R consists of the following rules:

   natsFrom(N) -> cons(N, n__natsFrom(s(N)))
   fst(pair(XS, YS)) -> XS
   snd(pair(XS, YS)) -> YS
   splitAt(0, XS) -> pair(nil, XS)
   splitAt(s(N), cons(X, XS)) -> u(splitAt(N, activate(XS)), N, X, activate(XS))
   u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
   head(cons(N, XS)) -> N
   tail(cons(N, XS)) -> activate(XS)
   sel(N, XS) -> head(afterNth(N, XS))
   take(N, XS) -> fst(splitAt(N, XS))
   afterNth(N, XS) -> snd(splitAt(N, XS))
   natsFrom(X) -> n__natsFrom(X)
   activate(n__natsFrom(X)) -> natsFrom(X)
   activate(X) -> X

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
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
Tuples:
   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
S tuples:
   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
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

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

Compound Symbols:   c, c1, c2, c3, c4, c5_3, c6_2, c7_1, c8, c9_1, c10_2, c11_2, c12_2, c13_1, c14


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 11 trailing nodes:
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   HEAD(cons(z0, z1)) -> c8
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   ACTIVATE(z0) -> c14
   NATSFROM(z0) -> c
   FST(pair(z0, z1)) -> c2
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   SPLITAT(0, z0) -> c4
   SND(pair(z0, z1)) -> c3
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   NATSFROM(z0) -> c1

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

(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
Tuples:
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   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))
S tuples:
   SPLITAT(s(z0), cons(z1, z2)) -> c5(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), SPLITAT(z0, activate(z2)), ACTIVATE(z2))
   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))
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

Defined Pair Symbols:   SPLITAT_2, SEL_2, TAKE_2, AFTERNTH_2

Compound Symbols:   c5_3, c10_2, c11_2, c12_2


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

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

(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
Tuples:
   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, activate(z2)))
   SEL(z0, z1) -> c10(AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(SPLITAT(z0, z1))
S tuples:
   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, activate(z2)))
   SEL(z0, z1) -> c10(AFTERNTH(z0, z1))
   TAKE(z0, z1) -> c11(SPLITAT(z0, z1))
   AFTERNTH(z0, z1) -> c12(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

Defined Pair Symbols:   SPLITAT_2, SEL_2, TAKE_2, AFTERNTH_2

Compound Symbols:   c5_1, c10_1, c11_1, c12_1


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

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 3 leading nodes:
   TAKE(z0, z1) -> c11(SPLITAT(z0, z1))
   SEL(z0, z1) -> c10(AFTERNTH(z0, z1))
   AFTERNTH(z0, z1) -> c12(SPLITAT(z0, z1))

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

(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
Tuples:
   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, activate(z2)))
S tuples:
   SPLITAT(s(z0), cons(z1, z2)) -> c5(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

Defined Pair Symbols:   SPLITAT_2

Compound Symbols:   c5_1


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

(9) 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))

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

(10)
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)) -> c5(SPLITAT(z0, activate(z2)))
S tuples:
   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, activate(z2)))
K tuples:none
Defined Rule Symbols:   activate_1, natsFrom_1

Defined Pair Symbols:   SPLITAT_2

Compound Symbols:   c5_1


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

(11) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, activate(z2)))

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

   activate(n__natsFrom(z0)) -> natsFrom(z0)
   activate(z0) -> z0
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0)))
   natsFrom(z0) -> n__natsFrom(z0)

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

(13) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, activate(z2))) [1]
   activate(n__natsFrom(z0)) -> natsFrom(z0) [0]
   activate(z0) -> z0 [0]
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) [0]
   natsFrom(z0) -> n__natsFrom(z0) [0]

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

(15) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(16)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, activate(z2))) [1]
   activate(n__natsFrom(z0)) -> natsFrom(z0) [0]
   activate(z0) -> z0 [0]
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) [0]
   natsFrom(z0) -> n__natsFrom(z0) [0]

The TRS has the following type information:
SPLITAT :: s -> cons:n__natsFrom -> c5
s :: s -> s
cons :: s -> cons:n__natsFrom -> cons:n__natsFrom
c5 :: c5 -> c5
activate :: cons:n__natsFrom -> cons:n__natsFrom
n__natsFrom :: s -> cons:n__natsFrom
natsFrom :: s -> cons:n__natsFrom

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

(17) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

   SPLITAT_2

(c) The following functions are completely defined:

   activate_1
   natsFrom_1

Due to the following rules being added:

   activate(v0) -> const2 [0]
   natsFrom(v0) -> const2 [0]

And the following fresh constants:    const2, const, const1

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

(18)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, activate(z2))) [1]
   activate(n__natsFrom(z0)) -> natsFrom(z0) [0]
   activate(z0) -> z0 [0]
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) [0]
   natsFrom(z0) -> n__natsFrom(z0) [0]
   activate(v0) -> const2 [0]
   natsFrom(v0) -> const2 [0]

The TRS has the following type information:
SPLITAT :: s -> cons:n__natsFrom:const2 -> c5
s :: s -> s
cons :: s -> cons:n__natsFrom:const2 -> cons:n__natsFrom:const2
c5 :: c5 -> c5
activate :: cons:n__natsFrom:const2 -> cons:n__natsFrom:const2
n__natsFrom :: s -> cons:n__natsFrom:const2
natsFrom :: s -> cons:n__natsFrom:const2
const2 :: cons:n__natsFrom:const2
const :: c5
const1 :: s

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

(19) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(20)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   SPLITAT(s(z0), cons(z1, n__natsFrom(z0'))) -> c5(SPLITAT(z0, natsFrom(z0'))) [1]
   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, z2)) [1]
   SPLITAT(s(z0), cons(z1, z2)) -> c5(SPLITAT(z0, const2)) [1]
   activate(n__natsFrom(z0)) -> natsFrom(z0) [0]
   activate(z0) -> z0 [0]
   natsFrom(z0) -> cons(z0, n__natsFrom(s(z0))) [0]
   natsFrom(z0) -> n__natsFrom(z0) [0]
   activate(v0) -> const2 [0]
   natsFrom(v0) -> const2 [0]

The TRS has the following type information:
SPLITAT :: s -> cons:n__natsFrom:const2 -> c5
s :: s -> s
cons :: s -> cons:n__natsFrom:const2 -> cons:n__natsFrom:const2
c5 :: c5 -> c5
activate :: cons:n__natsFrom:const2 -> cons:n__natsFrom:const2
n__natsFrom :: s -> cons:n__natsFrom:const2
natsFrom :: s -> cons:n__natsFrom:const2
const2 :: cons:n__natsFrom:const2
const :: c5
const1 :: s

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

(21) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   const2 => 0
   const => 0
   const1 => 0

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

(22)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, natsFrom(z0')) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z = 1 + z0, z0 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   activate(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0
   activate(z) -{ 0 }-> natsFrom(z0) :|: z = 1 + z0, z0 >= 0
   activate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   natsFrom(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   natsFrom(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0
   natsFrom(z) -{ 0 }-> 1 + z0 + (1 + (1 + z0)) :|: z = z0, z0 >= 0


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

(23) InliningProof (UPPER BOUND(ID))
Inlined the following terminating rules on right-hand sides where appropriate:

   natsFrom(z) -{ 0 }-> 1 + z0 + (1 + (1 + z0)) :|: z = z0, z0 >= 0
   natsFrom(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0
   natsFrom(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

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

(24)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z = 1 + z0, z0 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z = 1 + z0, z0 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z = 1 + z0, z0 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0
   activate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   activate(z) -{ 0 }-> 0 :|: z = 1 + z0, z0 >= 0, v0 >= 0, z0 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z = 1 + z0, z0 >= 0, z0 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z = 1 + z0, z0 >= 0, z0 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   natsFrom(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0
   natsFrom(z) -{ 0 }-> 1 + z0 + (1 + (1 + z0)) :|: z = z0, z0 >= 0


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

(25) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(26)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0


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

(27) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { natsFrom }
   { activate }
   { SPLITAT }

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

(28)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {natsFrom}, {activate}, {SPLITAT}

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

(29) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(30)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {natsFrom}, {activate}, {SPLITAT}

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

(31) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: natsFrom
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 3 + 2*z

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

(32)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {natsFrom}, {activate}, {SPLITAT}
Previous analysis results are:
  natsFrom: runtime: ?, size: O(n^1) [3 + 2*z]

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

(33) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: natsFrom
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(34)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}, {SPLITAT}
Previous analysis results are:
  natsFrom: runtime: O(1) [0], size: O(n^1) [3 + 2*z]

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

(35) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(36)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}, {SPLITAT}
Previous analysis results are:
  natsFrom: runtime: O(1) [0], size: O(n^1) [3 + 2*z]

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

(37) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + 2*z

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

(38)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}, {SPLITAT}
Previous analysis results are:
  natsFrom: runtime: O(1) [0], size: O(n^1) [3 + 2*z]
  activate: runtime: ?, size: O(n^1) [1 + 2*z]

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

(39) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(40)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {SPLITAT}
Previous analysis results are:
  natsFrom: runtime: O(1) [0], size: O(n^1) [3 + 2*z]
  activate: runtime: O(1) [0], size: O(n^1) [1 + 2*z]

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

(41) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(42)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {SPLITAT}
Previous analysis results are:
  natsFrom: runtime: O(1) [0], size: O(n^1) [3 + 2*z]
  activate: runtime: O(1) [0], size: O(n^1) [1 + 2*z]

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

(43) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: SPLITAT
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(44)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {SPLITAT}
Previous analysis results are:
  natsFrom: runtime: O(1) [0], size: O(n^1) [3 + 2*z]
  activate: runtime: O(1) [0], size: O(n^1) [1 + 2*z]
  SPLITAT: runtime: ?, size: O(1) [0]

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

(45) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: SPLITAT
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

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

(46)
Obligation:
Complexity RNTS consisting of the following rules:

   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 0) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, v0 >= 0, z0' = v0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'') :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z - 1, 1 + z0'' + (1 + (1 + z0''))) :|: z' = 1 + z1 + (1 + z0'), z1 >= 0, z0' >= 0, z - 1 >= 0, z0' = z0'', z0'' >= 0
   activate(z) -{ 0 }-> z :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z >= 0
   activate(z) -{ 0 }-> 0 :|: z - 1 >= 0, v0 >= 0, z - 1 = v0
   activate(z) -{ 0 }-> 1 + z0' :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   activate(z) -{ 0 }-> 1 + z0' + (1 + (1 + z0')) :|: z - 1 >= 0, z - 1 = z0', z0' >= 0
   natsFrom(z) -{ 0 }-> 0 :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z :|: z >= 0
   natsFrom(z) -{ 0 }-> 1 + z + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  natsFrom: runtime: O(1) [0], size: O(n^1) [3 + 2*z]
  activate: runtime: O(1) [0], size: O(n^1) [1 + 2*z]
  SPLITAT: runtime: O(n^1) [z], size: O(1) [0]

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

(47) FinalProof (FINISHED)
Computed overall runtime complexity
----------------------------------------

(48)
BOUNDS(1, n^1)