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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
(4) CdtProblem
(5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CdtProblem
(9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CpxRelTRS
(11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CpxWeightedTrs
(13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxTypedWeightedTrs
(15) CompletionProof [UPPER BOUND(ID), 0 ms]
(16) CpxTypedWeightedCompleteTrs
(17) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(18) CpxRNTS
(19) CompleteCoflocoProof [FINISHED, 597 ms]
(20) 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:

   nonZero(0) -> false
   nonZero(s(x)) -> true
   p(s(0)) -> 0
   p(s(s(x))) -> s(p(s(x)))
   id_inc(x) -> x
   id_inc(x) -> s(x)
   random(x) -> rand(x, 0)
   rand(x, y) -> if(nonZero(x), x, y)
   if(false, x, y) -> y
   if(true, x, y) -> rand(p(x), id_inc(y))

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:
   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   id_inc(z0) -> z0
   id_inc(z0) -> s(z0)
   random(z0) -> rand(z0, 0)
   rand(z0, z1) -> if(nonZero(z0), z0, z1)
   if(false, z0, z1) -> z1
   if(true, z0, z1) -> rand(p(z0), id_inc(z1))
Tuples:
   NONZERO(0) -> c
   NONZERO(s(z0)) -> c1
   P(s(0)) -> c2
   P(s(s(z0))) -> c3(P(s(z0)))
   ID_INC(z0) -> c4
   ID_INC(z0) -> c5
   RANDOM(z0) -> c6(RAND(z0, 0))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0))
   IF(false, z0, z1) -> c8
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1))
S tuples:
   NONZERO(0) -> c
   NONZERO(s(z0)) -> c1
   P(s(0)) -> c2
   P(s(s(z0))) -> c3(P(s(z0)))
   ID_INC(z0) -> c4
   ID_INC(z0) -> c5
   RANDOM(z0) -> c6(RAND(z0, 0))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0))
   IF(false, z0, z1) -> c8
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1))
K tuples:none
Defined Rule Symbols:   nonZero_1, p_1, id_inc_1, random_1, rand_2, if_3

Defined Pair Symbols:   NONZERO_1, P_1, ID_INC_1, RANDOM_1, RAND_2, IF_3

Compound Symbols:   c, c1, c2, c3_1, c4, c5, c6_1, c7_2, c8, c9_2, c10_2


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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   RANDOM(z0) -> c6(RAND(z0, 0))
Removed 6 trailing nodes:
   IF(false, z0, z1) -> c8
   P(s(0)) -> c2
   ID_INC(z0) -> c5
   NONZERO(0) -> c
   ID_INC(z0) -> c4
   NONZERO(s(z0)) -> c1

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   id_inc(z0) -> z0
   id_inc(z0) -> s(z0)
   random(z0) -> rand(z0, 0)
   rand(z0, z1) -> if(nonZero(z0), z0, z1)
   if(false, z0, z1) -> z1
   if(true, z0, z1) -> rand(p(z0), id_inc(z1))
Tuples:
   P(s(s(z0))) -> c3(P(s(z0)))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1))
S tuples:
   P(s(s(z0))) -> c3(P(s(z0)))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1))
K tuples:none
Defined Rule Symbols:   nonZero_1, p_1, id_inc_1, random_1, rand_2, if_3

Defined Pair Symbols:   P_1, RAND_2, IF_3

Compound Symbols:   c3_1, c7_2, c9_2, c10_2


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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   id_inc(z0) -> z0
   id_inc(z0) -> s(z0)
   random(z0) -> rand(z0, 0)
   rand(z0, z1) -> if(nonZero(z0), z0, z1)
   if(false, z0, z1) -> z1
   if(true, z0, z1) -> rand(p(z0), id_inc(z1))
Tuples:
   P(s(s(z0))) -> c3(P(s(z0)))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)))
S tuples:
   P(s(s(z0))) -> c3(P(s(z0)))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)))
K tuples:none
Defined Rule Symbols:   nonZero_1, p_1, id_inc_1, random_1, rand_2, if_3

Defined Pair Symbols:   P_1, IF_3, RAND_2

Compound Symbols:   c3_1, c9_2, c7_1, c10_1


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   random(z0) -> rand(z0, 0)
   rand(z0, z1) -> if(nonZero(z0), z0, z1)
   if(false, z0, z1) -> z1
   if(true, z0, z1) -> rand(p(z0), id_inc(z1))

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   id_inc(z0) -> z0
   id_inc(z0) -> s(z0)
   nonZero(0) -> false
   nonZero(s(z0)) -> true
Tuples:
   P(s(s(z0))) -> c3(P(s(z0)))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)))
S tuples:
   P(s(s(z0))) -> c3(P(s(z0)))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)))
K tuples:none
Defined Rule Symbols:   p_1, id_inc_1, nonZero_1

Defined Pair Symbols:   P_1, IF_3, RAND_2

Compound Symbols:   c3_1, c9_2, c7_1, c10_1


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

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

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

   P(s(s(z0))) -> c3(P(s(z0)))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)))

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

   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   id_inc(z0) -> z0
   id_inc(z0) -> s(z0)
   nonZero(0) -> false
   nonZero(s(z0)) -> true

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

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

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

   P(s(s(z0))) -> c3(P(s(z0))) [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0)) [1]
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1)) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1))) [1]
   p(s(0)) -> 0 [0]
   p(s(s(z0))) -> s(p(s(z0))) [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   nonZero(0) -> false [0]
   nonZero(s(z0)) -> true [0]

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

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

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

   P(s(s(z0))) -> c3(P(s(z0))) [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0)) [1]
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1)) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1))) [1]
   p(s(0)) -> 0 [0]
   p(s(s(z0))) -> s(p(s(z0))) [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   nonZero(0) -> false [0]
   nonZero(s(z0)) -> true [0]

The TRS has the following type information:
P :: s:0 -> c3
s :: s:0 -> s:0
c3 :: c3 -> c3
IF :: true:false -> s:0 -> s:0 -> c9:c10
true :: true:false
c9 :: c7 -> c3 -> c9:c10
RAND :: s:0 -> s:0 -> c7
p :: s:0 -> s:0
id_inc :: s:0 -> s:0
c7 :: c9:c10 -> c7
nonZero :: s:0 -> true:false
c10 :: c7 -> c9:c10
0 :: s:0
false :: true:false

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

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

   p(v0) -> null_p [0]
   id_inc(v0) -> null_id_inc [0]
   nonZero(v0) -> null_nonZero [0]
   P(v0) -> null_P [0]
   IF(v0, v1, v2) -> null_IF [0]

And the following fresh constants:    null_p, null_id_inc, null_nonZero, null_P, null_IF, const

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

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

   P(s(s(z0))) -> c3(P(s(z0))) [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0)) [1]
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1)) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1))) [1]
   p(s(0)) -> 0 [0]
   p(s(s(z0))) -> s(p(s(z0))) [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   nonZero(0) -> false [0]
   nonZero(s(z0)) -> true [0]
   p(v0) -> null_p [0]
   id_inc(v0) -> null_id_inc [0]
   nonZero(v0) -> null_nonZero [0]
   P(v0) -> null_P [0]
   IF(v0, v1, v2) -> null_IF [0]

The TRS has the following type information:
P :: s:0:null_p:null_id_inc -> c3:null_P
s :: s:0:null_p:null_id_inc -> s:0:null_p:null_id_inc
c3 :: c3:null_P -> c3:null_P
IF :: true:false:null_nonZero -> s:0:null_p:null_id_inc -> s:0:null_p:null_id_inc -> c9:c10:null_IF
true :: true:false:null_nonZero
c9 :: c7 -> c3:null_P -> c9:c10:null_IF
RAND :: s:0:null_p:null_id_inc -> s:0:null_p:null_id_inc -> c7
p :: s:0:null_p:null_id_inc -> s:0:null_p:null_id_inc
id_inc :: s:0:null_p:null_id_inc -> s:0:null_p:null_id_inc
c7 :: c9:c10:null_IF -> c7
nonZero :: s:0:null_p:null_id_inc -> true:false:null_nonZero
c10 :: c7 -> c9:c10:null_IF
0 :: s:0:null_p:null_id_inc
false :: true:false:null_nonZero
null_p :: s:0:null_p:null_id_inc
null_id_inc :: s:0:null_p:null_id_inc
null_nonZero :: true:false:null_nonZero
null_P :: c3:null_P
null_IF :: c9:c10:null_IF
const :: c7

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

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

   true => 2
   0 => 0
   false => 1
   null_p => 0
   null_id_inc => 0
   null_nonZero => 0
   null_P => 0
   null_IF => 0
   const => 0

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

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

   IF(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(p(z0), id_inc(z1)) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(p(z0), id_inc(z1)) + P(z0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   P(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   P(z) -{ 1 }-> 1 + P(1 + z0) :|: z0 >= 0, z = 1 + (1 + z0)
   RAND(z, z') -{ 1 }-> 1 + IF(nonZero(z0), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   id_inc(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0
   id_inc(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   id_inc(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0
   nonZero(z) -{ 0 }-> 2 :|: z = 1 + z0, z0 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(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)

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V, V2, V3),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V2, V3),0,[fun1(V, V2, V3, Out)],[V >= 0,V2 >= 0,V3 >= 0]).
eq(start(V, V2, V3),0,[fun2(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2, V3),0,[p(V, Out)],[V >= 0]).
eq(start(V, V2, V3),0,[fun3(V, Out)],[V >= 0]).
eq(start(V, V2, V3),0,[nonZero(V, Out)],[V >= 0]).
eq(fun(V, Out),1,[fun(1 + V1, Ret1)],[Out = 1 + Ret1,V1 >= 0,V = 2 + V1]).
eq(fun1(V, V2, V3, Out),1,[p(V5, Ret010),fun3(V4, Ret011),fun2(Ret010, Ret011, Ret01),fun(V5, Ret11)],[Out = 1 + Ret01 + Ret11,V = 2,V4 >= 0,V5 >= 0,V2 = V5,V3 = V4]).
eq(fun2(V, V2, Out),1,[nonZero(V7, Ret10),fun1(Ret10, V7, V6, Ret12)],[Out = 1 + Ret12,V = V7,V6 >= 0,V2 = V6,V7 >= 0]).
eq(fun1(V, V2, V3, Out),1,[p(V8, Ret101),fun3(V9, Ret111),fun2(Ret101, Ret111, Ret13)],[Out = 1 + Ret13,V = 2,V9 >= 0,V8 >= 0,V2 = V8,V3 = V9]).
eq(p(V, Out),0,[],[Out = 0,V = 1]).
eq(p(V, Out),0,[p(1 + V10, Ret14)],[Out = 1 + Ret14,V10 >= 0,V = 2 + V10]).
eq(fun3(V, Out),0,[],[Out = V11,V = V11,V11 >= 0]).
eq(fun3(V, Out),0,[],[Out = 1 + V12,V = V12,V12 >= 0]).
eq(nonZero(V, Out),0,[],[Out = 1,V = 0]).
eq(nonZero(V, Out),0,[],[Out = 2,V = 1 + V13,V13 >= 0]).
eq(p(V, Out),0,[],[Out = 0,V14 >= 0,V = V14]).
eq(fun3(V, Out),0,[],[Out = 0,V15 >= 0,V = V15]).
eq(nonZero(V, Out),0,[],[Out = 0,V16 >= 0,V = V16]).
eq(fun(V, Out),0,[],[Out = 0,V17 >= 0,V = V17]).
eq(fun1(V, V2, V3, Out),0,[],[Out = 0,V18 >= 0,V3 = V20,V19 >= 0,V = V18,V2 = V19,V20 >= 0]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,V2,V3,Out),[V,V2,V3],[Out]).
input_output_vars(fun2(V,V2,Out),[V,V2],[Out]).
input_output_vars(p(V,Out),[V],[Out]).
input_output_vars(fun3(V,Out),[V],[Out]).
input_output_vars(nonZero(V,Out),[V],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [fun/2]
1. non_recursive  : [nonZero/2]
2. non_recursive  : [fun3/2]
3. recursive  : [p/2]
4. recursive [non_tail] : [fun1/4,fun2/3]
5. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/2
1. SCC is partially evaluated into nonZero/2
2. SCC is partially evaluated into fun3/2
3. SCC is partially evaluated into p/2
4. SCC is partially evaluated into fun2/3
5. SCC is partially evaluated into start/3

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

### Specialization of cost equations fun/2 
* CE 18 is refined into CE [22] 
* CE 17 is refined into CE [23] 


### Cost equations --> "Loop" of fun/2 
* CEs [23] --> Loop 14 
* CEs [22] --> Loop 15 

### Ranking functions of CR fun(V,Out) 
* RF of phase [14]: [V-1]

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


### Specialization of cost equations nonZero/2 
* CE 20 is refined into CE [24] 
* CE 21 is refined into CE [25] 
* CE 19 is refined into CE [26] 


### Cost equations --> "Loop" of nonZero/2 
* CEs [24] --> Loop 16 
* CEs [25] --> Loop 17 
* CEs [26] --> Loop 18 

### Ranking functions of CR nonZero(V,Out) 

#### Partial ranking functions of CR nonZero(V,Out) 


### Specialization of cost equations fun3/2 
* CE 11 is refined into CE [27] 
* CE 12 is refined into CE [28] 
* CE 13 is refined into CE [29] 


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

### Ranking functions of CR fun3(V,Out) 

#### Partial ranking functions of CR fun3(V,Out) 


### Specialization of cost equations p/2 
* CE 9 is refined into CE [30] 
* CE 10 is refined into CE [31] 


### Cost equations --> "Loop" of p/2 
* CEs [31] --> Loop 22 
* CEs [30] --> Loop 23 

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

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


### Specialization of cost equations fun2/3 
* CE 15 is refined into CE [32,33,34,35,36,37] 
* CE 16 is refined into CE [38,39,40,41,42,43,44,45,46,47,48,49] 
* CE 14 is refined into CE [50,51,52] 


### Cost equations --> "Loop" of fun2/3 
* CEs [50,51,52] --> Loop 24 
* CEs [49] --> Loop 25 
* CEs [37,48] --> Loop 26 
* CEs [47] --> Loop 27 
* CEs [36,46] --> Loop 28 
* CEs [45] --> Loop 29 
* CEs [35,44] --> Loop 30 
* CEs [43] --> Loop 31 
* CEs [34,42] --> Loop 32 
* CEs [41] --> Loop 33 
* CEs [33,40] --> Loop 34 
* CEs [39] --> Loop 35 
* CEs [32,38] --> Loop 36 

### Ranking functions of CR fun2(V,V2,Out) 
* RF of phase [25,26,27,28,29,30]: [V-1]

#### Partial ranking functions of CR fun2(V,V2,Out) 
* Partial RF of phase [25,26,27,28,29,30]:
  - RF of loop [25:1,26:1,27:1,28:1,29:1,30:1]:
    V-1


### Specialization of cost equations start/3 
* CE 1 is refined into CE [53] 
* CE 2 is refined into CE [54,55,56,57,58,59,60,61,62,63,64,65] 
* CE 3 is refined into CE [66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89] 
* CE 4 is refined into CE [90,91] 
* CE 5 is refined into CE [92,93,94] 
* CE 6 is refined into CE [95,96] 
* CE 7 is refined into CE [97,98,99] 
* CE 8 is refined into CE [100,101,102] 


### Cost equations --> "Loop" of start/3 
* CEs [54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89] --> Loop 37 
* CEs [53,90,91,92,93,94,95,96,97,98,99,100,101,102] --> Loop 38 

### Ranking functions of CR start(V,V2,V3) 

#### Partial ranking functions of CR start(V,V2,V3) 


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

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

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

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


#### Cost of chains of nonZero(V,Out):
* Chain [18]: 0
  with precondition: [V=0,Out=1] 

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

* Chain [16]: 0
  with precondition: [Out=2,V>=1] 


#### Cost of chains of fun3(V,Out):
* Chain [21]: 0
  with precondition: [Out=0,V>=0] 

* Chain [20]: 0
  with precondition: [V+1=Out,V>=0] 

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


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

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


#### Cost of chains of fun2(V,V2,Out):
* Chain [[25,26,27,28,29,30],36,24]: 12*it(25)+1*s(7)+2*s(8)+3
  Such that:aux(6) =< V
it(25) =< aux(6)
aux(2) =< aux(6)
s(7) =< it(25)*aux(6)
s(8) =< it(25)*aux(2)

  with precondition: [V>=2,V2>=0,Out>=5] 

* Chain [[25,26,27,28,29,30],35,24]: 13*it(25)+1*s(7)+2*s(8)+3
  Such that:aux(7) =< V
it(25) =< aux(7)
aux(2) =< aux(7)
s(7) =< it(25)*aux(7)
s(8) =< it(25)*aux(2)

  with precondition: [V>=3,V2>=0,Out>=6] 

* Chain [[25,26,27,28,29,30],34,24]: 12*it(25)+1*s(7)+2*s(8)+3
  Such that:aux(8) =< V
it(25) =< aux(8)
aux(2) =< aux(8)
s(7) =< it(25)*aux(8)
s(8) =< it(25)*aux(2)

  with precondition: [V>=2,V2>=0,Out>=5] 

* Chain [[25,26,27,28,29,30],33,24]: 13*it(25)+1*s(7)+2*s(8)+3
  Such that:aux(9) =< V
it(25) =< aux(9)
aux(2) =< aux(9)
s(7) =< it(25)*aux(9)
s(8) =< it(25)*aux(2)

  with precondition: [V>=3,V2>=0,Out>=6] 

* Chain [[25,26,27,28,29,30],32,24]: 12*it(25)+1*s(7)+2*s(8)+3
  Such that:aux(10) =< V
it(25) =< aux(10)
aux(2) =< aux(10)
s(7) =< it(25)*aux(10)
s(8) =< it(25)*aux(2)

  with precondition: [V>=2,V2>=0,Out>=5] 

* Chain [[25,26,27,28,29,30],31,24]: 13*it(25)+1*s(7)+2*s(8)+3
  Such that:aux(11) =< V
it(25) =< aux(11)
aux(2) =< aux(11)
s(7) =< it(25)*aux(11)
s(8) =< it(25)*aux(2)

  with precondition: [V>=3,V2>=0,Out>=6] 

* Chain [[25,26,27,28,29,30],24]: 12*it(25)+1*s(7)+2*s(8)+1
  Such that:aux(12) =< V
it(25) =< aux(12)
aux(2) =< aux(12)
s(7) =< it(25)*aux(12)
s(8) =< it(25)*aux(2)

  with precondition: [V>=2,V2>=0,Out>=3] 

* Chain [36,24]: 3
  with precondition: [Out=3,V>=1,V2>=0] 

* Chain [35,24]: 1*s(10)+3
  Such that:s(10) =< V

  with precondition: [V2>=0,Out>=4,V+2>=Out] 

* Chain [34,24]: 3
  with precondition: [Out=3,V>=1,V2>=0] 

* Chain [33,24]: 1*s(11)+3
  Such that:s(11) =< V

  with precondition: [V2>=0,Out>=4,V+2>=Out] 

* Chain [32,24]: 3
  with precondition: [Out=3,V>=1,V2>=0] 

* Chain [31,24]: 1*s(12)+3
  Such that:s(12) =< V

  with precondition: [V2>=0,Out>=4,V+2>=Out] 

* Chain [24]: 1
  with precondition: [Out=1,V>=0,V2>=0] 


#### Cost of chains of start(V,V2,V3):
* Chain [38]: 91*s(51)+7*s(55)+14*s(56)+3
  Such that:aux(14) =< V
s(51) =< aux(14)
s(54) =< aux(14)
s(55) =< s(51)*aux(14)
s(56) =< s(51)*s(54)

  with precondition: [V>=0] 

* Chain [37]: 822*s(58)+63*s(60)+126*s(61)+4
  Such that:aux(18) =< V2
s(58) =< aux(18)
s(59) =< aux(18)
s(60) =< s(58)*aux(18)
s(61) =< s(58)*s(59)

  with precondition: [V=2,V2>=0,V3>=0] 


Closed-form bounds of start(V,V2,V3): 
-------------------------------------
* Chain [38] with precondition: [V>=0] 
    - Upper bound: 91*V+3+21*V*V 
    - Complexity: n^2 
* Chain [37] with precondition: [V=2,V2>=0,V3>=0] 
    - Upper bound: 822*V2+4+189*V2*V2 
    - Complexity: n^2 

### Maximum cost of start(V,V2,V3): max([21*V*V+91*V,nat(V2)*822+1+nat(V2)*189*nat(V2)])+3 
Asymptotic class: n^2 
* Total analysis performed in 618 ms.


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

(20)
BOUNDS(1, n^2)