WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 610 ms]
(2) CpxRelTRS
(3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxWeightedTrs
    (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CpxTypedWeightedTrs
    (7) CompletionProof [UPPER BOUND(ID), 0 ms]
    (8) CpxTypedWeightedCompleteTrs
    (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (10) CpxRNTS
    (11) CompleteCoflocoProof [FINISHED, 2756 ms]
    (12) BOUNDS(1, n^1)
(13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(14) TRS for Loop Detection
    (15) DecreasingLoopProof [LOWER BOUND(ID), 190 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) TRS for Loop Detection


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

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


The TRS R consists of the following rules:

   NONZERO(0) -> c
   NONZERO(s(z0)) -> c1
   P(0) -> c2
   P(s(z0)) -> c3
   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))

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

   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(0) -> 0
   p(s(z0)) -> 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))

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

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

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


The TRS R consists of the following rules:

   NONZERO(0) -> c
   NONZERO(s(z0)) -> c1
   P(0) -> c2
   P(s(z0)) -> c3
   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))

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

   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(0) -> 0
   p(s(z0)) -> 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))

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

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

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

   NONZERO(0) -> c [1]
   NONZERO(s(z0)) -> c1 [1]
   P(0) -> c2 [1]
   P(s(z0)) -> c3 [1]
   ID_INC(z0) -> c4 [1]
   ID_INC(z0) -> c5 [1]
   RANDOM(z0) -> c6(RAND(z0, 0)) [1]
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0)) [1]
   IF(false, z0, z1) -> c8 [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0)) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1)) [1]
   nonZero(0) -> false [0]
   nonZero(s(z0)) -> true [0]
   p(0) -> 0 [0]
   p(s(z0)) -> z0 [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   random(z0) -> rand(z0, 0) [0]
   rand(z0, z1) -> if(nonZero(z0), z0, z1) [0]
   if(false, z0, z1) -> z1 [0]
   if(true, z0, z1) -> rand(p(z0), id_inc(z1)) [0]

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

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

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

   NONZERO(0) -> c [1]
   NONZERO(s(z0)) -> c1 [1]
   P(0) -> c2 [1]
   P(s(z0)) -> c3 [1]
   ID_INC(z0) -> c4 [1]
   ID_INC(z0) -> c5 [1]
   RANDOM(z0) -> c6(RAND(z0, 0)) [1]
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0)) [1]
   IF(false, z0, z1) -> c8 [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0)) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1)) [1]
   nonZero(0) -> false [0]
   nonZero(s(z0)) -> true [0]
   p(0) -> 0 [0]
   p(s(z0)) -> z0 [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   random(z0) -> rand(z0, 0) [0]
   rand(z0, z1) -> if(nonZero(z0), z0, z1) [0]
   if(false, z0, z1) -> z1 [0]
   if(true, z0, z1) -> rand(p(z0), id_inc(z1)) [0]

The TRS has the following type information:
NONZERO :: 0:s -> c:c1
0 :: 0:s
c :: c:c1
s :: 0:s -> 0:s
c1 :: c:c1
P :: 0:s -> c2:c3
c2 :: c2:c3
c3 :: c2:c3
ID_INC :: 0:s -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
RANDOM :: 0:s -> c6
c6 :: c7 -> c6
RAND :: 0:s -> 0:s -> c7
c7 :: c8:c9:c10 -> c:c1 -> c7
IF :: false:true -> 0:s -> 0:s -> c8:c9:c10
nonZero :: 0:s -> false:true
false :: false:true
c8 :: c8:c9:c10
true :: false:true
c9 :: c7 -> c2:c3 -> c8:c9:c10
p :: 0:s -> 0:s
id_inc :: 0:s -> 0:s
c10 :: c7 -> c4:c5 -> c8:c9:c10
random :: 0:s -> 0:s
rand :: 0:s -> 0:s -> 0:s
if :: false:true -> 0:s -> 0:s -> 0:s

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

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

   nonZero(v0) -> null_nonZero [0]
   p(v0) -> null_p [0]
   id_inc(v0) -> null_id_inc [0]
   random(v0) -> null_random [0]
   rand(v0, v1) -> null_rand [0]
   if(v0, v1, v2) -> null_if [0]
   NONZERO(v0) -> null_NONZERO [0]
   P(v0) -> null_P [0]
   IF(v0, v1, v2) -> null_IF [0]

And the following fresh constants:    null_nonZero, null_p, null_id_inc, null_random, null_rand, null_if, null_NONZERO, null_P, null_IF, const, const1

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

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

   NONZERO(0) -> c [1]
   NONZERO(s(z0)) -> c1 [1]
   P(0) -> c2 [1]
   P(s(z0)) -> c3 [1]
   ID_INC(z0) -> c4 [1]
   ID_INC(z0) -> c5 [1]
   RANDOM(z0) -> c6(RAND(z0, 0)) [1]
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0)) [1]
   IF(false, z0, z1) -> c8 [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0)) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1)) [1]
   nonZero(0) -> false [0]
   nonZero(s(z0)) -> true [0]
   p(0) -> 0 [0]
   p(s(z0)) -> z0 [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   random(z0) -> rand(z0, 0) [0]
   rand(z0, z1) -> if(nonZero(z0), z0, z1) [0]
   if(false, z0, z1) -> z1 [0]
   if(true, z0, z1) -> rand(p(z0), id_inc(z1)) [0]
   nonZero(v0) -> null_nonZero [0]
   p(v0) -> null_p [0]
   id_inc(v0) -> null_id_inc [0]
   random(v0) -> null_random [0]
   rand(v0, v1) -> null_rand [0]
   if(v0, v1, v2) -> null_if [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:
NONZERO :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> c:c1:null_NONZERO
0 :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if
c :: c:c1:null_NONZERO
s :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if
c1 :: c:c1:null_NONZERO
P :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> c2:c3:null_P
c2 :: c2:c3:null_P
c3 :: c2:c3:null_P
ID_INC :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> c4:c5
c4 :: c4:c5
c5 :: c4:c5
RANDOM :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> c6
c6 :: c7 -> c6
RAND :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> c7
c7 :: c8:c9:c10:null_IF -> c:c1:null_NONZERO -> c7
IF :: false:true:null_nonZero -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> c8:c9:c10:null_IF
nonZero :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> false:true:null_nonZero
false :: false:true:null_nonZero
c8 :: c8:c9:c10:null_IF
true :: false:true:null_nonZero
c9 :: c7 -> c2:c3:null_P -> c8:c9:c10:null_IF
p :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if
id_inc :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if
c10 :: c7 -> c4:c5 -> c8:c9:c10:null_IF
random :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if
rand :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if
if :: false:true:null_nonZero -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if -> 0:s:null_p:null_id_inc:null_random:null_rand:null_if
null_nonZero :: false:true:null_nonZero
null_p :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if
null_id_inc :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if
null_random :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if
null_rand :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if
null_if :: 0:s:null_p:null_id_inc:null_random:null_rand:null_if
null_NONZERO :: c:c1:null_NONZERO
null_P :: c2:c3:null_P
null_IF :: c8:c9:c10:null_IF
const :: c6
const1 :: c7

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

(9) 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
   c => 1
   c1 => 2
   c2 => 1
   c3 => 2
   c4 => 0
   c5 => 1
   false => 1
   c8 => 0
   true => 2
   null_nonZero => 0
   null_p => 0
   null_id_inc => 0
   null_random => 0
   null_rand => 0
   null_if => 0
   null_NONZERO => 0
   null_P => 0
   null_IF => 0
   const => 0
   const1 => 0

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

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

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

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V, V6, V10),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V6, V10),0,[fun1(V, Out)],[V >= 0]).
eq(start(V, V6, V10),0,[fun2(V, Out)],[V >= 0]).
eq(start(V, V6, V10),0,[fun3(V, Out)],[V >= 0]).
eq(start(V, V6, V10),0,[fun4(V, V6, Out)],[V >= 0,V6 >= 0]).
eq(start(V, V6, V10),0,[fun5(V, V6, V10, Out)],[V >= 0,V6 >= 0,V10 >= 0]).
eq(start(V, V6, V10),0,[nonZero(V, Out)],[V >= 0]).
eq(start(V, V6, V10),0,[p(V, Out)],[V >= 0]).
eq(start(V, V6, V10),0,[fun6(V, Out)],[V >= 0]).
eq(start(V, V6, V10),0,[random(V, Out)],[V >= 0]).
eq(start(V, V6, V10),0,[rand(V, V6, Out)],[V >= 0,V6 >= 0]).
eq(start(V, V6, V10),0,[if(V, V6, V10, Out)],[V >= 0,V6 >= 0,V10 >= 0]).
eq(fun(V, Out),1,[],[Out = 1,V = 0]).
eq(fun(V, Out),1,[],[Out = 2,V = 1 + V1,V1 >= 0]).
eq(fun1(V, Out),1,[],[Out = 1,V = 0]).
eq(fun1(V, Out),1,[],[Out = 2,V = 1 + V2,V2 >= 0]).
eq(fun2(V, Out),1,[],[Out = 0,V = V3,V3 >= 0]).
eq(fun2(V, Out),1,[],[Out = 1,V = V4,V4 >= 0]).
eq(fun3(V, Out),1,[fun4(V5, 0, Ret1)],[Out = 1 + Ret1,V = V5,V5 >= 0]).
eq(fun4(V, V6, Out),1,[nonZero(V7, Ret010),fun5(Ret010, V7, V8, Ret01),fun(V7, Ret11)],[Out = 1 + Ret01 + Ret11,V = V7,V8 >= 0,V6 = V8,V7 >= 0]).
eq(fun5(V, V6, V10, Out),1,[],[Out = 0,V11 >= 0,V = 1,V9 >= 0,V6 = V9,V10 = V11]).
eq(fun5(V, V6, V10, Out),1,[p(V13, Ret0101),fun6(V12, Ret011),fun4(Ret0101, Ret011, Ret012),fun1(V13, Ret12)],[Out = 1 + Ret012 + Ret12,V = 2,V12 >= 0,V13 >= 0,V6 = V13,V10 = V12]).
eq(fun5(V, V6, V10, Out),1,[p(V15, Ret0102),fun6(V14, Ret0111),fun4(Ret0102, Ret0111, Ret013),fun2(V14, Ret13)],[Out = 1 + Ret013 + Ret13,V = 2,V14 >= 0,V15 >= 0,V6 = V15,V10 = V14]).
eq(nonZero(V, Out),0,[],[Out = 1,V = 0]).
eq(nonZero(V, Out),0,[],[Out = 2,V = 1 + V16,V16 >= 0]).
eq(p(V, Out),0,[],[Out = 0,V = 0]).
eq(p(V, Out),0,[],[Out = V17,V = 1 + V17,V17 >= 0]).
eq(fun6(V, Out),0,[],[Out = V18,V = V18,V18 >= 0]).
eq(fun6(V, Out),0,[],[Out = 1 + V19,V = V19,V19 >= 0]).
eq(random(V, Out),0,[rand(V20, 0, Ret)],[Out = Ret,V = V20,V20 >= 0]).
eq(rand(V, V6, Out),0,[nonZero(V22, Ret0),if(Ret0, V22, V21, Ret2)],[Out = Ret2,V = V22,V21 >= 0,V6 = V21,V22 >= 0]).
eq(if(V, V6, V10, Out),0,[],[Out = V23,V23 >= 0,V = 1,V24 >= 0,V6 = V24,V10 = V23]).
eq(if(V, V6, V10, Out),0,[p(V26, Ret02),fun6(V25, Ret14),rand(Ret02, Ret14, Ret3)],[Out = Ret3,V = 2,V25 >= 0,V26 >= 0,V6 = V26,V10 = V25]).
eq(nonZero(V, Out),0,[],[Out = 0,V27 >= 0,V = V27]).
eq(p(V, Out),0,[],[Out = 0,V28 >= 0,V = V28]).
eq(fun6(V, Out),0,[],[Out = 0,V29 >= 0,V = V29]).
eq(random(V, Out),0,[],[Out = 0,V30 >= 0,V = V30]).
eq(rand(V, V6, Out),0,[],[Out = 0,V31 >= 0,V32 >= 0,V = V31,V6 = V32]).
eq(if(V, V6, V10, Out),0,[],[Out = 0,V33 >= 0,V10 = V35,V34 >= 0,V = V33,V6 = V34,V35 >= 0]).
eq(fun(V, Out),0,[],[Out = 0,V36 >= 0,V = V36]).
eq(fun1(V, Out),0,[],[Out = 0,V37 >= 0,V = V37]).
eq(fun5(V, V6, V10, Out),0,[],[Out = 0,V38 >= 0,V10 = V39,V40 >= 0,V = V38,V6 = V40,V39 >= 0]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,Out),[V],[Out]).
input_output_vars(fun2(V,Out),[V],[Out]).
input_output_vars(fun3(V,Out),[V],[Out]).
input_output_vars(fun4(V,V6,Out),[V,V6],[Out]).
input_output_vars(fun5(V,V6,V10,Out),[V,V6,V10],[Out]).
input_output_vars(nonZero(V,Out),[V],[Out]).
input_output_vars(p(V,Out),[V],[Out]).
input_output_vars(fun6(V,Out),[V],[Out]).
input_output_vars(random(V,Out),[V],[Out]).
input_output_vars(rand(V,V6,Out),[V,V6],[Out]).
input_output_vars(if(V,V6,V10,Out),[V,V6,V10],[Out]).


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

#### Computed strongly connected components 
0. non_recursive  : [fun/2]
1. non_recursive  : [fun1/2]
2. non_recursive  : [fun2/2]
3. non_recursive  : [fun6/2]
4. non_recursive  : [p/2]
5. non_recursive  : [nonZero/2]
6. recursive [non_tail] : [fun4/3,fun5/4]
7. non_recursive  : [fun3/2]
8. recursive  : [if/4,rand/3]
9. non_recursive  : [random/2]
10. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/2
1. SCC is partially evaluated into fun1/2
2. SCC is partially evaluated into fun2/2
3. SCC is partially evaluated into fun6/2
4. SCC is partially evaluated into p/2
5. SCC is partially evaluated into nonZero/2
6. SCC is partially evaluated into fun4/3
7. SCC is completely evaluated into other SCCs
8. SCC is partially evaluated into rand/3
9. SCC is partially evaluated into random/2
10. SCC is partially evaluated into start/3

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

### Specialization of cost equations fun/2 
* CE 35 is refined into CE [42] 
* CE 36 is refined into CE [43] 
* CE 34 is refined into CE [44] 


### Cost equations --> "Loop" of fun/2 
* CEs [42] --> Loop 25 
* CEs [43] --> Loop 26 
* CEs [44] --> Loop 27 

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

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


### Specialization of cost equations fun1/2 
* CE 32 is refined into CE [45] 
* CE 33 is refined into CE [46] 
* CE 31 is refined into CE [47] 


### Cost equations --> "Loop" of fun1/2 
* CEs [45] --> Loop 28 
* CEs [46] --> Loop 29 
* CEs [47] --> Loop 30 

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

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


### Specialization of cost equations fun2/2 
* CE 30 is refined into CE [48] 
* CE 29 is refined into CE [49] 


### Cost equations --> "Loop" of fun2/2 
* CEs [48] --> Loop 31 
* CEs [49] --> Loop 32 

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

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


### Specialization of cost equations fun6/2 
* CE 18 is refined into CE [50] 
* CE 19 is refined into CE [51] 
* CE 20 is refined into CE [52] 


### Cost equations --> "Loop" of fun6/2 
* CEs [50] --> Loop 33 
* CEs [51] --> Loop 34 
* CEs [52] --> Loop 35 

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

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


### Specialization of cost equations p/2 
* CE 17 is refined into CE [53] 
* CE 16 is refined into CE [54] 


### Cost equations --> "Loop" of p/2 
* CEs [53] --> Loop 36 
* CEs [54] --> Loop 37 

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

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


### Specialization of cost equations nonZero/2 
* CE 38 is refined into CE [55] 
* CE 39 is refined into CE [56] 
* CE 37 is refined into CE [57] 


### Cost equations --> "Loop" of nonZero/2 
* CEs [55] --> Loop 38 
* CEs [56] --> Loop 39 
* CEs [57] --> Loop 40 

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

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


### Specialization of cost equations fun4/3 
* CE 25 is refined into CE [58,59,60,61,62,63,64] 
* CE 28 is refined into CE [65,66] 
* CE 26 is refined into CE [67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90] 
* CE 27 is refined into CE [91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114] 


### Cost equations --> "Loop" of fun4/3 
* CEs [114] --> Loop 41 
* CEs [90] --> Loop 42 
* CEs [88,112,113] --> Loop 43 
* CEs [89] --> Loop 44 
* CEs [87,111] --> Loop 45 
* CEs [110] --> Loop 46 
* CEs [86] --> Loop 47 
* CEs [84,108,109] --> Loop 48 
* CEs [85] --> Loop 49 
* CEs [83,107] --> Loop 50 
* CEs [106] --> Loop 51 
* CEs [82] --> Loop 52 
* CEs [80,104,105] --> Loop 53 
* CEs [81] --> Loop 54 
* CEs [79,103] --> Loop 55 
* CEs [102] --> Loop 56 
* CEs [78] --> Loop 57 
* CEs [76,100,101] --> Loop 58 
* CEs [77] --> Loop 59 
* CEs [75,99] --> Loop 60 
* CEs [98] --> Loop 61 
* CEs [74] --> Loop 62 
* CEs [72,96,97] --> Loop 63 
* CEs [73] --> Loop 64 
* CEs [71,95] --> Loop 65 
* CEs [94] --> Loop 66 
* CEs [70] --> Loop 67 
* CEs [68,92,93] --> Loop 68 
* CEs [69] --> Loop 69 
* CEs [67,91] --> Loop 70 
* CEs [62,64] --> Loop 71 
* CEs [58,60,65] --> Loop 72 
* CEs [59,61,63,66] --> Loop 73 

### Ranking functions of CR fun4(V,V6,Out) 
* RF of phase [41,42,43,44,45,46,47,48,49,50,51,52,53,54,55]: [V]

#### Partial ranking functions of CR fun4(V,V6,Out) 
* Partial RF of phase [41,42,43,44,45,46,47,48,49,50,51,52,53,54,55]:
  - RF of loop [41:1,42:1,43:1,44:1,45:1,46:1,47:1,48:1,49:1,50:1,51:1,52:1,53:1,54:1,55:1]:
    V


### Specialization of cost equations rand/3 
* CE 23 is refined into CE [115] 
* CE 21 is refined into CE [116,117,118] 
* CE 24 is refined into CE [119] 
* CE 22 is refined into CE [120,121,122,123,124,125] 


### Cost equations --> "Loop" of rand/3 
* CEs [125] --> Loop 74 
* CEs [124] --> Loop 75 
* CEs [123] --> Loop 76 
* CEs [122] --> Loop 77 
* CEs [121] --> Loop 78 
* CEs [120] --> Loop 79 
* CEs [115] --> Loop 80 
* CEs [116,117,118,119] --> Loop 81 

### Ranking functions of CR rand(V,V6,Out) 
* RF of phase [74,75,76]: [V]

#### Partial ranking functions of CR rand(V,V6,Out) 
* Partial RF of phase [74,75,76]:
  - RF of loop [74:1,75:1,76:1]:
    V


### Specialization of cost equations random/2 
* CE 40 is refined into CE [126,127,128,129] 
* CE 41 is refined into CE [130] 


### Cost equations --> "Loop" of random/2 
* CEs [128] --> Loop 82 
* CEs [126,127,129,130] --> Loop 83 

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

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


### Specialization of cost equations start/3 
* CE 2 is refined into CE [131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148] 
* CE 3 is refined into CE [149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220] 
* CE 4 is refined into CE [221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298] 
* CE 1 is refined into CE [299] 
* CE 5 is refined into CE [300] 
* CE 6 is refined into CE [301,302,303] 
* CE 7 is refined into CE [304,305,306] 
* CE 8 is refined into CE [307,308] 
* CE 9 is refined into CE [309,310,311,312,313,314,315,316,317,318] 
* CE 10 is refined into CE [319,320,321,322,323,324,325,326,327,328] 
* CE 11 is refined into CE [329,330,331] 
* CE 12 is refined into CE [332,333] 
* CE 13 is refined into CE [334,335,336] 
* CE 14 is refined into CE [337,338] 
* CE 15 is refined into CE [339,340,341,342] 


### Cost equations --> "Loop" of start/3 
* CEs [137,141,145,161,162,181,182,201,202,239,240,259,260,279,280] --> Loop 84 
* CEs [131,132,133,134,135,136,138,139,140,142,143,144,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298] --> Loop 85 
* CEs [300] --> Loop 86 
* CEs [299,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342] --> Loop 87 

### Ranking functions of CR start(V,V6,V10) 

#### Partial ranking functions of CR start(V,V6,V10) 


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

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

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

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


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

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

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


#### Cost of chains of fun2(V,Out):
* Chain [32]: 1
  with precondition: [Out=0,V>=0] 

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


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

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

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


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

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


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

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

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


#### Cost of chains of fun4(V,V6,Out):
* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],73]: 54*it(41)+2
  Such that:aux(3) =< V
it(41) =< aux(3)

  with precondition: [V>=1,V6>=0,Out>=3,6*V+1>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],72]: 54*it(41)+3
  Such that:aux(4) =< V
it(41) =< aux(4)

  with precondition: [V>=1,V6>=0,Out>=2*V+2,6*V+2>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],71]: 54*it(41)+2
  Such that:aux(5) =< V
it(41) =< aux(5)

  with precondition: [V>=2,V6>=0,Out>=5,6*V>=Out+3] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],70,73]: 54*it(41)+5
  Such that:aux(6) =< V
it(41) =< aux(6)

  with precondition: [V>=2,V6>=0,Out>=5,6*V>=Out+3] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],70,72]: 54*it(41)+6
  Such that:aux(7) =< V
it(41) =< aux(7)

  with precondition: [V>=2,V6>=0,Out>=6,6*V>=Out+2] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],69,73]: 54*it(41)+5
  Such that:aux(8) =< V
it(41) =< aux(8)

  with precondition: [V>=2,V6>=0,Out>=6,6*V>=Out+2] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],69,72]: 54*it(41)+6
  Such that:aux(9) =< V
it(41) =< aux(9)

  with precondition: [V>=2,V6>=0,Out>=7,6*V>=Out+1] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],68,73]: 54*it(41)+6
  Such that:aux(10) =< V
it(41) =< aux(10)

  with precondition: [V>=2,V6>=0,Out>=7,6*V>=Out+1] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],68,72]: 54*it(41)+7
  Such that:aux(11) =< V
it(41) =< aux(11)

  with precondition: [V>=2,V6>=0,Out>=8,6*V>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],67,73]: 54*it(41)+6
  Such that:aux(12) =< V
it(41) =< aux(12)

  with precondition: [V>=2,V6>=0,Out>=8,6*V>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],67,72]: 54*it(41)+7
  Such that:aux(13) =< V
it(41) =< aux(13)

  with precondition: [V>=2,V6>=0,Out>=9,6*V+1>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],66,73]: 54*it(41)+6
  Such that:aux(14) =< V
it(41) =< aux(14)

  with precondition: [V>=2,V6>=0,Out>=9,6*V+1>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],66,72]: 54*it(41)+7
  Such that:aux(15) =< V
it(41) =< aux(15)

  with precondition: [V>=2,V6>=0,Out>=10,6*V+2>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],65,73]: 54*it(41)+5
  Such that:aux(16) =< V
it(41) =< aux(16)

  with precondition: [V>=2,V6>=0,Out>=5,6*V>=Out+3] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],65,72]: 54*it(41)+6
  Such that:aux(17) =< V
it(41) =< aux(17)

  with precondition: [V>=2,V6>=0,Out>=6,6*V>=Out+2] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],64,73]: 54*it(41)+5
  Such that:aux(18) =< V
it(41) =< aux(18)

  with precondition: [V>=2,V6>=0,Out>=6,6*V>=Out+2] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],64,72]: 54*it(41)+6
  Such that:aux(19) =< V
it(41) =< aux(19)

  with precondition: [V>=2,V6>=0,Out>=7,6*V>=Out+1] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],63,73]: 54*it(41)+6
  Such that:aux(20) =< V
it(41) =< aux(20)

  with precondition: [V>=2,V6>=0,Out>=7,6*V>=Out+1] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],63,72]: 54*it(41)+7
  Such that:aux(21) =< V
it(41) =< aux(21)

  with precondition: [V>=2,V6>=0,Out>=8,6*V>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],62,73]: 54*it(41)+6
  Such that:aux(22) =< V
it(41) =< aux(22)

  with precondition: [V>=2,V6>=0,Out>=8,6*V>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],62,72]: 54*it(41)+7
  Such that:aux(23) =< V
it(41) =< aux(23)

  with precondition: [V>=2,V6>=0,Out>=9,6*V+1>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],61,73]: 54*it(41)+6
  Such that:aux(24) =< V
it(41) =< aux(24)

  with precondition: [V>=2,V6>=0,Out>=9,6*V+1>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],61,72]: 54*it(41)+7
  Such that:aux(25) =< V
it(41) =< aux(25)

  with precondition: [V>=2,V6>=0,Out>=10,6*V+2>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],60,73]: 54*it(41)+5
  Such that:aux(26) =< V
it(41) =< aux(26)

  with precondition: [V>=2,V6>=0,Out>=5,6*V>=Out+3] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],60,72]: 54*it(41)+6
  Such that:aux(27) =< V
it(41) =< aux(27)

  with precondition: [V>=2,V6>=0,Out>=6,6*V>=Out+2] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],59,73]: 54*it(41)+5
  Such that:aux(28) =< V
it(41) =< aux(28)

  with precondition: [V>=2,V6>=0,Out>=6,6*V>=Out+2] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],59,72]: 54*it(41)+6
  Such that:aux(29) =< V
it(41) =< aux(29)

  with precondition: [V>=2,V6>=0,Out>=7,6*V>=Out+1] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],58,73]: 54*it(41)+6
  Such that:aux(30) =< V
it(41) =< aux(30)

  with precondition: [V>=2,V6>=0,Out>=7,6*V>=Out+1] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],58,72]: 54*it(41)+7
  Such that:aux(31) =< V
it(41) =< aux(31)

  with precondition: [V>=2,V6>=0,Out>=8,6*V>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],57,73]: 54*it(41)+6
  Such that:aux(32) =< V
it(41) =< aux(32)

  with precondition: [V>=2,V6>=0,Out>=8,6*V>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],57,72]: 54*it(41)+7
  Such that:aux(33) =< V
it(41) =< aux(33)

  with precondition: [V>=2,V6>=0,Out>=9,6*V+1>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],56,73]: 54*it(41)+6
  Such that:aux(34) =< V
it(41) =< aux(34)

  with precondition: [V>=2,V6>=0,Out>=9,6*V+1>=Out] 

* Chain [[41,42,43,44,45,46,47,48,49,50,51,52,53,54,55],56,72]: 54*it(41)+7
  Such that:aux(35) =< V
it(41) =< aux(35)

  with precondition: [V>=2,V6>=0,Out>=10,6*V+2>=Out] 

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

* Chain [72]: 3
  with precondition: [V=0,Out=2,V6>=0] 

* Chain [71]: 2
  with precondition: [Out=3,V>=1,V6>=0] 

* Chain [70,73]: 5
  with precondition: [Out=3,V>=1,V6>=0] 

* Chain [70,72]: 6
  with precondition: [Out=4,V>=1,V6>=0] 

* Chain [69,73]: 5
  with precondition: [Out=4,V>=1,V6>=0] 

* Chain [69,72]: 6
  with precondition: [Out=5,V>=1,V6>=0] 

* Chain [68,73]: 6
  with precondition: [Out=5,V>=1,V6>=0] 

* Chain [68,72]: 7
  with precondition: [Out=6,V>=1,V6>=0] 

* Chain [67,73]: 6
  with precondition: [Out=6,V>=1,V6>=0] 

* Chain [67,72]: 7
  with precondition: [Out=7,V>=1,V6>=0] 

* Chain [66,73]: 6
  with precondition: [Out=7,V>=1,V6>=0] 

* Chain [66,72]: 7
  with precondition: [Out=8,V>=1,V6>=0] 

* Chain [65,73]: 5
  with precondition: [Out=3,V>=1,V6>=0] 

* Chain [65,72]: 6
  with precondition: [Out=4,V>=1,V6>=0] 

* Chain [64,73]: 5
  with precondition: [Out=4,V>=1,V6>=0] 

* Chain [64,72]: 6
  with precondition: [Out=5,V>=1,V6>=0] 

* Chain [63,73]: 6
  with precondition: [Out=5,V>=1,V6>=0] 

* Chain [63,72]: 7
  with precondition: [Out=6,V>=1,V6>=0] 

* Chain [62,73]: 6
  with precondition: [Out=6,V>=1,V6>=0] 

* Chain [62,72]: 7
  with precondition: [Out=7,V>=1,V6>=0] 

* Chain [61,73]: 6
  with precondition: [Out=7,V>=1,V6>=0] 

* Chain [61,72]: 7
  with precondition: [Out=8,V>=1,V6>=0] 

* Chain [60,73]: 5
  with precondition: [Out=3,V>=1,V6>=0] 

* Chain [60,72]: 6
  with precondition: [Out=4,V>=1,V6>=0] 

* Chain [59,73]: 5
  with precondition: [Out=4,V>=1,V6>=0] 

* Chain [59,72]: 6
  with precondition: [Out=5,V>=1,V6>=0] 

* Chain [58,73]: 6
  with precondition: [Out=5,V>=1,V6>=0] 

* Chain [58,72]: 7
  with precondition: [Out=6,V>=1,V6>=0] 

* Chain [57,73]: 6
  with precondition: [Out=6,V>=1,V6>=0] 

* Chain [57,72]: 7
  with precondition: [Out=7,V>=1,V6>=0] 

* Chain [56,73]: 6
  with precondition: [Out=7,V>=1,V6>=0] 

* Chain [56,72]: 7
  with precondition: [Out=8,V>=1,V6>=0] 


#### Cost of chains of rand(V,V6,Out):
* Chain [[74,75,76],81]: 0
  with precondition: [Out=0,V>=1,V6>=0] 

* Chain [[74,75,76],80]: 0
  with precondition: [V>=1,V6>=0,Out>=0,V+V6>=Out] 

* Chain [[74,75,76],79,81]: 0
  with precondition: [Out=0,V>=2,V6>=0] 

* Chain [[74,75,76],79,80]: 0
  with precondition: [Out=0,V>=2,V6>=0] 

* Chain [[74,75,76],78,81]: 0
  with precondition: [Out=0,V>=2,V6>=0] 

* Chain [[74,75,76],78,80]: 0
  with precondition: [V>=2,V6>=0,Out>=1,V+V6>=Out] 

* Chain [[74,75,76],77,81]: 0
  with precondition: [Out=0,V>=2,V6>=0] 

* Chain [[74,75,76],77,80]: 0
  with precondition: [V>=2,V6>=0,Out>=0,V+V6>=Out+1] 

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

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

* Chain [79,81]: 0
  with precondition: [Out=0,V>=1,V6>=0] 

* Chain [79,80]: 0
  with precondition: [Out=0,V>=1,V6>=0] 

* Chain [78,81]: 0
  with precondition: [Out=0,V>=1,V6>=0] 

* Chain [78,80]: 0
  with precondition: [Out=V6+1,V>=1,Out>=1] 

* Chain [77,81]: 0
  with precondition: [Out=0,V>=1,V6>=0] 

* Chain [77,80]: 0
  with precondition: [V6=Out,V>=1,V6>=0] 


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

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


#### Cost of chains of start(V,V6,V10):
* Chain [87]: 3564*s(66)+8
  Such that:aux(40) =< V
s(66) =< aux(40)

  with precondition: [V>=0] 

* Chain [86]: 1
  with precondition: [V=1,V6>=0,V10>=0] 

* Chain [85]: 21384*s(78)+9
  Such that:aux(41) =< V6
s(78) =< aux(41)

  with precondition: [V=2,V6>=0,V10>=0] 

* Chain [84]: 5
  with precondition: [V=2,V6=1,V10>=0] 


Closed-form bounds of start(V,V6,V10): 
-------------------------------------
* Chain [87] with precondition: [V>=0] 
    - Upper bound: 3564*V+8 
    - Complexity: n 
* Chain [86] with precondition: [V=1,V6>=0,V10>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [85] with precondition: [V=2,V6>=0,V10>=0] 
    - Upper bound: 21384*V6+9 
    - Complexity: n 
* Chain [84] with precondition: [V=2,V6=1,V10>=0] 
    - Upper bound: 5 
    - Complexity: constant 

### Maximum cost of start(V,V6,V10): max([3564*V+7,nat(V6)*21384+8])+1 
Asymptotic class: n 
* Total analysis performed in 2645 ms.


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

(12)
BOUNDS(1, n^1)

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

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

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

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


The TRS R consists of the following rules:

   NONZERO(0) -> c
   NONZERO(s(z0)) -> c1
   P(0) -> c2
   P(s(z0)) -> c3
   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))

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

   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(0) -> 0
   p(s(z0)) -> 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))

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

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

The rewrite sequence

RAND(s(z01_2), z1) ->^+ c7(c9(RAND(z01_2, id_inc(z1)), P(s(z01_2))), NONZERO(s(z01_2)))

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

The pumping substitution is [z01_2 / s(z01_2)].

The result substitution is [z1 / id_inc(z1)].




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

(16)
Complex Obligation (BEST)

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

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

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


The TRS R consists of the following rules:

   NONZERO(0) -> c
   NONZERO(s(z0)) -> c1
   P(0) -> c2
   P(s(z0)) -> c3
   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))

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

   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(0) -> 0
   p(s(z0)) -> 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))

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

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

(19)
BOUNDS(n^1, INF)

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

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

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


The TRS R consists of the following rules:

   NONZERO(0) -> c
   NONZERO(s(z0)) -> c1
   P(0) -> c2
   P(s(z0)) -> c3
   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))

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

   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(0) -> 0
   p(s(z0)) -> 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))

Rewrite Strategy: INNERMOST