WORST_CASE(?,O(n^2))
proof of input_qUCgbesnP3.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^2).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxWeightedTrs
(9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CpxTypedWeightedTrs
(11) CompletionProof [UPPER BOUND(ID), 0 ms]
(12) CpxTypedWeightedCompleteTrs
(13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(14) CpxRNTS
(15) CompleteCoflocoProof [FINISHED, 507 ms]
(16) BOUNDS(1, n^2)


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

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


The TRS R consists of the following rules:

   plus(x, 0) -> x
   plus(x, s(y)) -> s(plus(x, y))
   times(0, y) -> 0
   times(x, 0) -> 0
   times(s(x), y) -> plus(times(x, y), y)
   p(s(s(x))) -> s(p(s(x)))
   p(s(0)) -> 0
   fac(s(x)) -> times(fac(p(s(x))), s(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:
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(z0, 0) -> 0
   times(s(z0), z1) -> plus(times(z0, z1), z1)
   p(s(s(z0))) -> s(p(s(z0)))
   p(s(0)) -> 0
   fac(s(z0)) -> times(fac(p(s(z0))), s(z0))
Tuples:
   PLUS(z0, 0) -> c
   PLUS(z0, s(z1)) -> c1(PLUS(z0, z1))
   TIMES(0, z0) -> c2
   TIMES(z0, 0) -> c3
   TIMES(s(z0), z1) -> c4(PLUS(times(z0, z1), z1), TIMES(z0, z1))
   P(s(s(z0))) -> c5(P(s(z0)))
   P(s(0)) -> c6
   FAC(s(z0)) -> c7(TIMES(fac(p(s(z0))), s(z0)), FAC(p(s(z0))), P(s(z0)))
S tuples:
   PLUS(z0, 0) -> c
   PLUS(z0, s(z1)) -> c1(PLUS(z0, z1))
   TIMES(0, z0) -> c2
   TIMES(z0, 0) -> c3
   TIMES(s(z0), z1) -> c4(PLUS(times(z0, z1), z1), TIMES(z0, z1))
   P(s(s(z0))) -> c5(P(s(z0)))
   P(s(0)) -> c6
   FAC(s(z0)) -> c7(TIMES(fac(p(s(z0))), s(z0)), FAC(p(s(z0))), P(s(z0)))
K tuples:none
Defined Rule Symbols:   plus_2, times_2, p_1, fac_1

Defined Pair Symbols:   PLUS_2, TIMES_2, P_1, FAC_1

Compound Symbols:   c, c1_1, c2, c3, c4_2, c5_1, c6, c7_3


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 4 trailing nodes:
   TIMES(0, z0) -> c2
   PLUS(z0, 0) -> c
   P(s(0)) -> c6
   TIMES(z0, 0) -> c3

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(z0, 0) -> 0
   times(s(z0), z1) -> plus(times(z0, z1), z1)
   p(s(s(z0))) -> s(p(s(z0)))
   p(s(0)) -> 0
   fac(s(z0)) -> times(fac(p(s(z0))), s(z0))
Tuples:
   PLUS(z0, s(z1)) -> c1(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c4(PLUS(times(z0, z1), z1), TIMES(z0, z1))
   P(s(s(z0))) -> c5(P(s(z0)))
   FAC(s(z0)) -> c7(TIMES(fac(p(s(z0))), s(z0)), FAC(p(s(z0))), P(s(z0)))
S tuples:
   PLUS(z0, s(z1)) -> c1(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c4(PLUS(times(z0, z1), z1), TIMES(z0, z1))
   P(s(s(z0))) -> c5(P(s(z0)))
   FAC(s(z0)) -> c7(TIMES(fac(p(s(z0))), s(z0)), FAC(p(s(z0))), P(s(z0)))
K tuples:none
Defined Rule Symbols:   plus_2, times_2, p_1, fac_1

Defined Pair Symbols:   PLUS_2, TIMES_2, P_1, FAC_1

Compound Symbols:   c1_1, c4_2, c5_1, c7_3


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

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

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


The TRS R consists of the following rules:

   PLUS(z0, s(z1)) -> c1(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c4(PLUS(times(z0, z1), z1), TIMES(z0, z1))
   P(s(s(z0))) -> c5(P(s(z0)))
   FAC(s(z0)) -> c7(TIMES(fac(p(s(z0))), s(z0)), FAC(p(s(z0))), P(s(z0)))

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

   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(z0, 0) -> 0
   times(s(z0), z1) -> plus(times(z0, z1), z1)
   p(s(s(z0))) -> s(p(s(z0)))
   p(s(0)) -> 0
   fac(s(z0)) -> times(fac(p(s(z0))), s(z0))

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

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

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


The TRS R consists of the following rules:

   PLUS(z0, s(z1)) -> c1(PLUS(z0, z1)) [1]
   TIMES(s(z0), z1) -> c4(PLUS(times(z0, z1), z1), TIMES(z0, z1)) [1]
   P(s(s(z0))) -> c5(P(s(z0))) [1]
   FAC(s(z0)) -> c7(TIMES(fac(p(s(z0))), s(z0)), FAC(p(s(z0))), P(s(z0))) [1]
   plus(z0, 0) -> z0 [0]
   plus(z0, s(z1)) -> s(plus(z0, z1)) [0]
   times(0, z0) -> 0 [0]
   times(z0, 0) -> 0 [0]
   times(s(z0), z1) -> plus(times(z0, z1), z1) [0]
   p(s(s(z0))) -> s(p(s(z0))) [0]
   p(s(0)) -> 0 [0]
   fac(s(z0)) -> times(fac(p(s(z0))), s(z0)) [0]

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

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

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

   PLUS(z0, s(z1)) -> c1(PLUS(z0, z1)) [1]
   TIMES(s(z0), z1) -> c4(PLUS(times(z0, z1), z1), TIMES(z0, z1)) [1]
   P(s(s(z0))) -> c5(P(s(z0))) [1]
   FAC(s(z0)) -> c7(TIMES(fac(p(s(z0))), s(z0)), FAC(p(s(z0))), P(s(z0))) [1]
   plus(z0, 0) -> z0 [0]
   plus(z0, s(z1)) -> s(plus(z0, z1)) [0]
   times(0, z0) -> 0 [0]
   times(z0, 0) -> 0 [0]
   times(s(z0), z1) -> plus(times(z0, z1), z1) [0]
   p(s(s(z0))) -> s(p(s(z0))) [0]
   p(s(0)) -> 0 [0]
   fac(s(z0)) -> times(fac(p(s(z0))), s(z0)) [0]

The TRS has the following type information:
PLUS :: s:0 -> s:0 -> c1
s :: s:0 -> s:0
c1 :: c1 -> c1
TIMES :: s:0 -> s:0 -> c4
c4 :: c1 -> c4 -> c4
times :: s:0 -> s:0 -> s:0
P :: s:0 -> c5
c5 :: c5 -> c5
FAC :: s:0 -> c7
c7 :: c4 -> c7 -> c5 -> c7
fac :: s:0 -> s:0
p :: s:0 -> s:0
plus :: s:0 -> s:0 -> s:0
0 :: s:0

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

(11) 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:

   plus(v0, v1) -> null_plus [0]
   times(v0, v1) -> null_times [0]
   p(v0) -> null_p [0]
   fac(v0) -> null_fac [0]
   PLUS(v0, v1) -> null_PLUS [0]
   TIMES(v0, v1) -> null_TIMES [0]
   P(v0) -> null_P [0]
   FAC(v0) -> null_FAC [0]

And the following fresh constants:    null_plus, null_times, null_p, null_fac, null_PLUS, null_TIMES, null_P, null_FAC

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

(12)
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:

   PLUS(z0, s(z1)) -> c1(PLUS(z0, z1)) [1]
   TIMES(s(z0), z1) -> c4(PLUS(times(z0, z1), z1), TIMES(z0, z1)) [1]
   P(s(s(z0))) -> c5(P(s(z0))) [1]
   FAC(s(z0)) -> c7(TIMES(fac(p(s(z0))), s(z0)), FAC(p(s(z0))), P(s(z0))) [1]
   plus(z0, 0) -> z0 [0]
   plus(z0, s(z1)) -> s(plus(z0, z1)) [0]
   times(0, z0) -> 0 [0]
   times(z0, 0) -> 0 [0]
   times(s(z0), z1) -> plus(times(z0, z1), z1) [0]
   p(s(s(z0))) -> s(p(s(z0))) [0]
   p(s(0)) -> 0 [0]
   fac(s(z0)) -> times(fac(p(s(z0))), s(z0)) [0]
   plus(v0, v1) -> null_plus [0]
   times(v0, v1) -> null_times [0]
   p(v0) -> null_p [0]
   fac(v0) -> null_fac [0]
   PLUS(v0, v1) -> null_PLUS [0]
   TIMES(v0, v1) -> null_TIMES [0]
   P(v0) -> null_P [0]
   FAC(v0) -> null_FAC [0]

The TRS has the following type information:
PLUS :: s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac -> c1:null_PLUS
s :: s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac
c1 :: c1:null_PLUS -> c1:null_PLUS
TIMES :: s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac -> c4:null_TIMES
c4 :: c1:null_PLUS -> c4:null_TIMES -> c4:null_TIMES
times :: s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac
P :: s:0:null_plus:null_times:null_p:null_fac -> c5:null_P
c5 :: c5:null_P -> c5:null_P
FAC :: s:0:null_plus:null_times:null_p:null_fac -> c7:null_FAC
c7 :: c4:null_TIMES -> c7:null_FAC -> c5:null_P -> c7:null_FAC
fac :: s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac
p :: s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac
plus :: s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac -> s:0:null_plus:null_times:null_p:null_fac
0 :: s:0:null_plus:null_times:null_p:null_fac
null_plus :: s:0:null_plus:null_times:null_p:null_fac
null_times :: s:0:null_plus:null_times:null_p:null_fac
null_p :: s:0:null_plus:null_times:null_p:null_fac
null_fac :: s:0:null_plus:null_times:null_p:null_fac
null_PLUS :: c1:null_PLUS
null_TIMES :: c4:null_TIMES
null_P :: c5:null_P
null_FAC :: c7:null_FAC

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

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

   0 => 0
   null_plus => 0
   null_times => 0
   null_p => 0
   null_fac => 0
   null_PLUS => 0
   null_TIMES => 0
   null_P => 0
   null_FAC => 0

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

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

   FAC(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   FAC(z) -{ 1 }-> 1 + TIMES(fac(p(1 + z0)), 1 + z0) + FAC(p(1 + z0)) + P(1 + z0) :|: z = 1 + z0, z0 >= 0
   P(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   P(z) -{ 1 }-> 1 + P(1 + z0) :|: z0 >= 0, z = 1 + (1 + z0)
   PLUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   PLUS(z, z') -{ 1 }-> 1 + PLUS(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   TIMES(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   TIMES(z, z') -{ 1 }-> 1 + PLUS(times(z0, z1), z1) + TIMES(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   fac(z) -{ 0 }-> times(fac(p(1 + z0)), 1 + z0) :|: z = 1 + z0, z0 >= 0
   fac(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   p(z) -{ 0 }-> 0 :|: z = 1 + 0
   p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   p(z) -{ 0 }-> 1 + p(1 + z0) :|: z0 >= 0, z = 1 + (1 + z0)
   plus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + plus(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   times(z, z') -{ 0 }-> plus(times(z0, z1), z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   times(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   times(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   times(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

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

(15) 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,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun2(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun3(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[plus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[times(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[p(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fac(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[fun(V3, V2, Ret1)],[Out = 1 + Ret1,V1 = V3,V2 >= 0,V3 >= 0,V = 1 + V2]).
eq(fun1(V1, V, Out),1,[times(V5, V4, Ret010),fun(Ret010, V4, Ret01),fun1(V5, V4, Ret11)],[Out = 1 + Ret01 + Ret11,V4 >= 0,V1 = 1 + V5,V = V4,V5 >= 0]).
eq(fun2(V1, Out),1,[fun2(1 + V6, Ret12)],[Out = 1 + Ret12,V6 >= 0,V1 = 2 + V6]).
eq(fun3(V1, Out),1,[p(1 + V7, Ret00100),fac(Ret00100, Ret0010),fun1(Ret0010, 1 + V7, Ret001),p(1 + V7, Ret0101),fun3(Ret0101, Ret011),fun2(1 + V7, Ret13)],[Out = 1 + Ret001 + Ret011 + Ret13,V1 = 1 + V7,V7 >= 0]).
eq(plus(V1, V, Out),0,[],[Out = V8,V1 = V8,V8 >= 0,V = 0]).
eq(plus(V1, V, Out),0,[plus(V9, V10, Ret14)],[Out = 1 + Ret14,V1 = V9,V10 >= 0,V9 >= 0,V = 1 + V10]).
eq(times(V1, V, Out),0,[],[Out = 0,V11 >= 0,V1 = 0,V = V11]).
eq(times(V1, V, Out),0,[],[Out = 0,V1 = V12,V12 >= 0,V = 0]).
eq(times(V1, V, Out),0,[times(V14, V13, Ret0),plus(Ret0, V13, Ret)],[Out = Ret,V13 >= 0,V1 = 1 + V14,V = V13,V14 >= 0]).
eq(p(V1, Out),0,[p(1 + V15, Ret15)],[Out = 1 + Ret15,V15 >= 0,V1 = 2 + V15]).
eq(p(V1, Out),0,[],[Out = 0,V1 = 1]).
eq(fac(V1, Out),0,[p(1 + V16, Ret00),fac(Ret00, Ret02),times(Ret02, 1 + V16, Ret2)],[Out = Ret2,V1 = 1 + V16,V16 >= 0]).
eq(plus(V1, V, Out),0,[],[Out = 0,V18 >= 0,V17 >= 0,V1 = V18,V = V17]).
eq(times(V1, V, Out),0,[],[Out = 0,V20 >= 0,V19 >= 0,V1 = V20,V = V19]).
eq(p(V1, Out),0,[],[Out = 0,V21 >= 0,V1 = V21]).
eq(fac(V1, Out),0,[],[Out = 0,V22 >= 0,V1 = V22]).
eq(fun(V1, V, Out),0,[],[Out = 0,V23 >= 0,V24 >= 0,V1 = V23,V = V24]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V25 >= 0,V26 >= 0,V1 = V25,V = V26]).
eq(fun2(V1, Out),0,[],[Out = 0,V27 >= 0,V1 = V27]).
eq(fun3(V1, Out),0,[],[Out = 0,V28 >= 0,V1 = V28]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,Out),[V1],[Out]).
input_output_vars(fun3(V1,Out),[V1],[Out]).
input_output_vars(plus(V1,V,Out),[V1,V],[Out]).
input_output_vars(times(V1,V,Out),[V1,V],[Out]).
input_output_vars(p(V1,Out),[V1],[Out]).
input_output_vars(fac(V1,Out),[V1],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [p/2]
1. recursive  : [plus/3]
2. recursive [non_tail] : [times/3]
3. recursive [non_tail] : [fac/2]
4. recursive  : [fun/3]
5. recursive  : [fun1/3]
6. recursive  : [fun2/2]
7. recursive [non_tail] : [fun3/2]
8. non_recursive  : [start/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into p/2
1. SCC is partially evaluated into plus/3
2. SCC is partially evaluated into times/3
3. SCC is partially evaluated into fac/2
4. SCC is partially evaluated into fun/3
5. SCC is partially evaluated into fun1/3
6. SCC is partially evaluated into fun2/2
7. SCC is partially evaluated into fun3/2
8. SCC is partially evaluated into start/2

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

### Specialization of cost equations p/2 
* CE 24 is refined into CE [27] 
* CE 23 is refined into CE [28] 


### Cost equations --> "Loop" of p/2 
* CEs [28] --> Loop 19 
* CEs [27] --> Loop 20 

### Ranking functions of CR p(V1,Out) 
* RF of phase [19]: [V1-1]

#### Partial ranking functions of CR p(V1,Out) 
* Partial RF of phase [19]:
  - RF of loop [19:1]:
    V1-1


### Specialization of cost equations plus/3 
* CE 19 is refined into CE [29] 
* CE 17 is refined into CE [30] 
* CE 18 is refined into CE [31] 


### Cost equations --> "Loop" of plus/3 
* CEs [31] --> Loop 21 
* CEs [29] --> Loop 22 
* CEs [30] --> Loop 23 

### Ranking functions of CR plus(V1,V,Out) 
* RF of phase [21]: [V]

#### Partial ranking functions of CR plus(V1,V,Out) 
* Partial RF of phase [21]:
  - RF of loop [21:1]:
    V


### Specialization of cost equations times/3 
* CE 20 is refined into CE [32] 
* CE 21 is refined into CE [33] 
* CE 22 is refined into CE [34,35,36,37] 


### Cost equations --> "Loop" of times/3 
* CEs [37] --> Loop 24 
* CEs [36] --> Loop 25 
* CEs [35] --> Loop 26 
* CEs [34] --> Loop 27 
* CEs [32,33] --> Loop 28 

### Ranking functions of CR times(V1,V,Out) 
* RF of phase [24,25,26,27]: [V1]

#### Partial ranking functions of CR times(V1,V,Out) 
* Partial RF of phase [24,25,26,27]:
  - RF of loop [24:1,25:1,26:1,27:1]:
    V1


### Specialization of cost equations fac/2 
* CE 26 is refined into CE [38] 
* CE 25 is refined into CE [39,40,41,42] 


### Cost equations --> "Loop" of fac/2 
* CEs [42] --> Loop 29 
* CEs [40] --> Loop 30 
* CEs [41] --> Loop 31 
* CEs [39] --> Loop 32 
* CEs [38] --> Loop 33 

### Ranking functions of CR fac(V1,Out) 
* RF of phase [29]: [V1-1]
* RF of phase [31]: [V1-1]

#### Partial ranking functions of CR fac(V1,Out) 
* Partial RF of phase [29]:
  - RF of loop [29:1]:
    V1-1
* Partial RF of phase [31]:
  - RF of loop [31:1]:
    V1-1


### Specialization of cost equations fun/3 
* CE 10 is refined into CE [43] 
* CE 9 is refined into CE [44] 


### Cost equations --> "Loop" of fun/3 
* CEs [44] --> Loop 34 
* CEs [43] --> Loop 35 

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

#### Partial ranking functions of CR fun(V1,V,Out) 
* Partial RF of phase [34]:
  - RF of loop [34:1]:
    V


### Specialization of cost equations fun1/3 
* CE 12 is refined into CE [45] 
* CE 11 is refined into CE [46,47,48,49] 


### Cost equations --> "Loop" of fun1/3 
* CEs [47,49] --> Loop 36 
* CEs [46,48] --> Loop 37 
* CEs [45] --> Loop 38 

### Ranking functions of CR fun1(V1,V,Out) 
* RF of phase [36,37]: [V1]

#### Partial ranking functions of CR fun1(V1,V,Out) 
* Partial RF of phase [36,37]:
  - RF of loop [36:1,37:1]:
    V1


### Specialization of cost equations fun2/2 
* CE 14 is refined into CE [50] 
* CE 13 is refined into CE [51] 


### Cost equations --> "Loop" of fun2/2 
* CEs [51] --> Loop 39 
* CEs [50] --> Loop 40 

### Ranking functions of CR fun2(V1,Out) 
* RF of phase [39]: [V1-1]

#### Partial ranking functions of CR fun2(V1,Out) 
* Partial RF of phase [39]:
  - RF of loop [39:1]:
    V1-1


### Specialization of cost equations fun3/2 
* CE 16 is refined into CE [52] 
* CE 15 is refined into CE [53,54,55,56,57,58,59,60] 


### Cost equations --> "Loop" of fun3/2 
* CEs [56,60] --> Loop 41 
* CEs [55,59] --> Loop 42 
* CEs [54,58] --> Loop 43 
* CEs [53,57] --> Loop 44 
* CEs [52] --> Loop 45 

### Ranking functions of CR fun3(V1,Out) 
* RF of phase [41,42]: [V1-1]

#### Partial ranking functions of CR fun3(V1,Out) 
* Partial RF of phase [41,42]:
  - RF of loop [41:1,42:1]:
    V1-1


### Specialization of cost equations start/2 
* CE 1 is refined into CE [61,62] 
* CE 2 is refined into CE [63,64] 
* CE 3 is refined into CE [65,66] 
* CE 4 is refined into CE [67,68,69] 
* CE 5 is refined into CE [70,71,72,73] 
* CE 6 is refined into CE [74,75] 
* CE 7 is refined into CE [76,77] 
* CE 8 is refined into CE [78] 


### Cost equations --> "Loop" of start/2 
* CEs [61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78] --> Loop 46 

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

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


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

#### Cost of chains of p(V1,Out):
* Chain [[19],20]: 0
  with precondition: [Out>=1,V1>=Out+1] 

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


#### Cost of chains of plus(V1,V,Out):
* Chain [[21],23]: 0
  with precondition: [V+V1=Out,V1>=0,V>=1] 

* Chain [[21],22]: 0
  with precondition: [V1>=0,Out>=1,V>=Out] 

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

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


#### Cost of chains of times(V1,V,Out):
* Chain [[24,25,26,27],28]: 0
  with precondition: [V1>=1,V>=0,Out>=0] 

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


#### Cost of chains of fac(V1,Out):
* Chain [[31],33]: 0
  with precondition: [Out=0,V1>=2] 

* Chain [[31],32,33]: 0
  with precondition: [Out=0,V1>=2] 

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

* Chain [32,33]: 0
  with precondition: [Out=0,V1>=1] 


#### Cost of chains of fun(V1,V,Out):
* Chain [[34],35]: 1*it(34)+0
  Such that:it(34) =< Out

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

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


#### Cost of chains of fun1(V1,V,Out):
* Chain [[36,37],38]: 2*it(36)+2*s(5)+0
  Such that:aux(4) =< V
aux(7) =< V1
it(36) =< aux(7)
s(6) =< it(36)*aux(4)
s(5) =< s(6)

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

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


#### Cost of chains of fun2(V1,Out):
* Chain [[39],40]: 1*it(39)+0
  Such that:it(39) =< Out

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

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


#### Cost of chains of fun3(V1,Out):
* Chain [[41,42],45]: 2*it(41)+2*s(11)+0
  Such that:aux(12) =< V1
it(41) =< aux(12)
s(12) =< it(41)*aux(12)
s(11) =< s(12)

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

* Chain [[41,42],44,45]: 2*it(41)+2*s(11)+1
  Such that:aux(13) =< V1
it(41) =< aux(13)
s(12) =< it(41)*aux(13)
s(11) =< s(12)

  with precondition: [V1>=2,Out>=2] 

* Chain [[41,42],43,45]: 4*it(41)+2*s(11)+1
  Such that:aux(15) =< V1
it(41) =< aux(15)
s(12) =< it(41)*aux(15)
s(11) =< s(12)

  with precondition: [V1>=3,Out>=3] 

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

* Chain [44,45]: 1
  with precondition: [Out=1,V1>=1] 

* Chain [43,45]: 2*s(13)+1
  Such that:aux(14) =< V1
s(13) =< aux(14)

  with precondition: [Out>=2,V1>=Out] 


#### Cost of chains of start(V1,V):
* Chain [46]: 1*s(29)+13*s(32)+2*s(34)+6*s(39)+1
  Such that:aux(17) =< V1
aux(18) =< V
s(32) =< aux(17)
s(29) =< aux(18)
s(33) =< s(32)*aux(18)
s(34) =< s(33)
s(38) =< s(32)*aux(17)
s(39) =< s(38)

  with precondition: [V1>=0] 


Closed-form bounds of start(V1,V): 
-------------------------------------
* Chain [46] with precondition: [V1>=0] 
    - Upper bound: 13*V1+1+6*V1*V1+2*V1*nat(V)+nat(V) 
    - Complexity: n^2 

### Maximum cost of start(V1,V): 13*V1+1+6*V1*V1+2*V1*nat(V)+nat(V) 
Asymptotic class: n^2 
* Total analysis performed in 440 ms.


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

(16)
BOUNDS(1, n^2)