WORST_CASE(?,O(n^1))
proof of input_C2IdGi6mpm.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 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) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(20) CpxRNTS
(21) CompleteCoflocoProof [FINISHED, 126 ms]
(22) 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:
   U(pair(z0, z1), z2, z3, z4) -> c7(ACTIVATE(z3))
   ACTIVATE(z0) -> c14
   NATSFROM(z0) -> c
   SPLITAT(s(z0), cons(z1, z2)) -> c6(U(splitAt(z0, activate(z2)), z0, z1, activate(z2)), ACTIVATE(z2))
   SPLITAT(0, z0) -> c4
   SND(pair(z0, z1)) -> c3
   ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0))
   TAIL(cons(z0, z1)) -> c9(ACTIVATE(z1))
   FST(pair(z0, z1)) -> c2
   HEAD(cons(z0, z1)) -> c8
   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 TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   activate(v0) -> null_activate [0]
   natsFrom(v0) -> null_natsFrom [0]
   SPLITAT(v0, v1) -> null_SPLITAT [0]

And the following fresh constants:    null_activate, null_natsFrom, null_SPLITAT, const

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

(18)
Obligation:
Runtime Complexity Weighted TRS where all 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) -> null_activate [0]
   natsFrom(v0) -> null_natsFrom [0]
   SPLITAT(v0, v1) -> null_SPLITAT [0]

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

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

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

   null_activate => 0
   null_natsFrom => 0
   null_SPLITAT => 0
   const => 0

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

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

   SPLITAT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   SPLITAT(z, z') -{ 1 }-> 1 + SPLITAT(z0, activate(z2)) :|: 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

Only complete derivations are relevant for the runtime complexity.

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

(21) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V1, V),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[activate(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[natsFrom(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[activate(V4, Ret11),fun(V3, Ret11, Ret1)],[Out = 1 + Ret1,V2 >= 0,V = 1 + V2 + V4,V1 = 1 + V3,V3 >= 0,V4 >= 0]).
eq(activate(V1, Out),0,[natsFrom(V5, Ret)],[Out = Ret,V1 = 1 + V5,V5 >= 0]).
eq(activate(V1, Out),0,[],[Out = V6,V1 = V6,V6 >= 0]).
eq(natsFrom(V1, Out),0,[],[Out = 3 + 2*V7,V1 = V7,V7 >= 0]).
eq(natsFrom(V1, Out),0,[],[Out = 1 + V8,V1 = V8,V8 >= 0]).
eq(activate(V1, Out),0,[],[Out = 0,V9 >= 0,V1 = V9]).
eq(natsFrom(V1, Out),0,[],[Out = 0,V10 >= 0,V1 = V10]).
eq(fun(V1, V, Out),0,[],[Out = 0,V12 >= 0,V11 >= 0,V1 = V12,V = V11]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(activate(V1,Out),[V1],[Out]).
input_output_vars(natsFrom(V1,Out),[V1],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. non_recursive  : [natsFrom/2]
1. non_recursive  : [activate/2]
2. recursive  : [fun/3]
3. non_recursive  : [start/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into natsFrom/2
1. SCC is partially evaluated into activate/2
2. SCC is partially evaluated into fun/3
3. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations natsFrom/2 
* CE 9 is refined into CE [12] 
* CE 10 is refined into CE [13] 
* CE 11 is refined into CE [14] 


### Cost equations --> "Loop" of natsFrom/2 
* CEs [12] --> Loop 10 
* CEs [13] --> Loop 11 
* CEs [14] --> Loop 12 

### Ranking functions of CR natsFrom(V1,Out) 

#### Partial ranking functions of CR natsFrom(V1,Out) 


### Specialization of cost equations activate/2 
* CE 6 is refined into CE [15,16,17] 
* CE 7 is refined into CE [18] 
* CE 8 is refined into CE [19] 


### Cost equations --> "Loop" of activate/2 
* CEs [17] --> Loop 13 
* CEs [16,18] --> Loop 14 
* CEs [15,19] --> Loop 15 

### Ranking functions of CR activate(V1,Out) 

#### Partial ranking functions of CR activate(V1,Out) 


### Specialization of cost equations fun/3 
* CE 5 is refined into CE [20] 
* CE 4 is refined into CE [21,22,23] 


### Cost equations --> "Loop" of fun/3 
* CEs [23] --> Loop 16 
* CEs [21,22] --> Loop 17 
* CEs [20] --> Loop 18 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [16,17]: [V1]

#### Partial ranking functions of CR fun(V1,V,Out) 
* Partial RF of phase [16,17]:
  - RF of loop [16:1,17:1]:
    V1
  - RF of loop [17:1]:
    V depends on loops [16:1] 


### Specialization of cost equations start/2 
* CE 1 is refined into CE [24,25] 
* CE 2 is refined into CE [26,27,28] 
* CE 3 is refined into CE [29,30,31] 


### Cost equations --> "Loop" of start/2 
* CEs [24,25,26,27,28,29,30,31] --> Loop 19 

### Ranking functions of CR start(V1,V) 

#### Partial ranking functions of CR start(V1,V) 


Computing Bounds
=====================================

#### Cost of chains of natsFrom(V1,Out):
* Chain [12]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [11]: 0
  with precondition: [V1+1=Out,V1>=0] 

* Chain [10]: 0
  with precondition: [2*V1+3=Out,V1>=0] 


#### Cost of chains of activate(V1,Out):
* Chain [15]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [14]: 0
  with precondition: [V1=Out,V1>=0] 

* Chain [13]: 0
  with precondition: [2*V1+1=Out,V1>=1] 


#### Cost of chains of fun(V1,V,Out):
* Chain [[16,17],18]: 2*it(16)+0
  Such that:aux(7) =< V1
aux(8) =< Out
it(16) =< aux(7)
it(16) =< aux(8)

  with precondition: [V>=1,Out>=1,V1>=Out] 

* Chain [18]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of start(V1,V):
* Chain [19]: 2*s(3)+0
  Such that:aux(9) =< V1
s(3) =< aux(9)

  with precondition: [V1>=0] 


Closed-form bounds of start(V1,V): 
-------------------------------------
* Chain [19] with precondition: [V1>=0] 
    - Upper bound: 2*V1 
    - Complexity: n 

### Maximum cost of start(V1,V): 2*V1 
Asymptotic class: n 
* Total analysis performed in 107 ms.


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

(22)
BOUNDS(1, n^1)