WORST_CASE(Omega(n^2),O(n^2))
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^2, n^2).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 1265 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, 3047 ms]
    (12) BOUNDS(1, n^2)
(13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxRelTRS
    (15) SlicingProof [LOWER BOUND(ID), 0 ms]
    (16) CpxRelTRS
    (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) typed CpxTrs
    (19) OrderProof [LOWER BOUND(ID), 0 ms]
    (20) typed CpxTrs
    (21) RewriteLemmaProof [LOWER BOUND(ID), 238 ms]
    (22) BEST
        (23) proven lower bound
            (24) LowerBoundPropagationProof [FINISHED, 0 ms]
            (25) BOUNDS(n^1, INF)
        (26) typed CpxTrs
            (27) RewriteLemmaProof [LOWER BOUND(ID), 11 ms]
            (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 1459 ms]
            (30) BEST
                (31) proven lower bound
                    (32) LowerBoundPropagationProof [FINISHED, 0 ms]
                    (33) BOUNDS(n^2, INF)
                (34) typed CpxTrs
                    (35) RewriteLemmaProof [LOWER BOUND(ID), 63 ms]
                    (36) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

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

The (relative) TRS S consists of the following 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))

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^2, n^2).


The TRS R consists of the following rules:

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

The (relative) TRS S consists of the following 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))

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^2).


The TRS R consists of the following rules:

   NONZERO(0) -> c [1]
   NONZERO(s(z0)) -> c1 [1]
   P(s(0)) -> c2 [1]
   P(s(s(z0))) -> c3(P(s(z0))) [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(s(0)) -> 0 [0]
   p(s(s(z0))) -> s(p(s(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(s(0)) -> c2 [1]
   P(s(s(z0))) -> c3(P(s(z0))) [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(s(0)) -> 0 [0]
   p(s(s(z0))) -> s(p(s(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 -> 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(s(0)) -> c2 [1]
   P(s(s(z0))) -> c3(P(s(z0))) [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(s(0)) -> 0 [0]
   p(s(s(z0))) -> s(p(s(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 -> 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 => 0
   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 }-> 0 :|: z = 1 + 0
   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) + 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 }-> 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)
   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 = 0,V = 1]).
eq(fun1(V, Out),1,[fun1(1 + V2, Ret1)],[Out = 1 + Ret1,V2 >= 0,V = 2 + V2]).
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, Ret11)],[Out = 1 + Ret11,V = V5,V5 >= 0]).
eq(fun4(V, V6, Out),1,[nonZero(V7, Ret010),fun5(Ret010, V7, V8, Ret01),fun(V7, Ret12)],[Out = 1 + Ret01 + Ret12,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, Ret13)],[Out = 1 + Ret012 + Ret13,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, Ret14)],[Out = 1 + Ret013 + Ret14,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 = 1]).
eq(p(V, Out),0,[p(1 + V17, Ret15)],[Out = 1 + Ret15,V17 >= 0,V = 2 + V17]).
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, Ret16),rand(Ret02, Ret16, 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. recursive  : [fun1/2]
2. non_recursive  : [fun2/2]
3. non_recursive  : [fun6/2]
4. 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 24 
* CEs [43] --> Loop 25 
* CEs [44] --> Loop 26 

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

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


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


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

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

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


### 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 29 
* CEs [49] --> Loop 30 

### 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 31 
* CEs [51] --> Loop 32 
* CEs [52] --> Loop 33 

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

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


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


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

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

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


### 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 36 
* CEs [56] --> Loop 37 
* CEs [57] --> Loop 38 

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

### Ranking functions of CR fun4(V,V6,Out) 
* RF of phase [39,40,41,42,43,44,45,46,47,48,49,50]: [V-1]

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


### 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 72 
* CEs [124] --> Loop 73 
* CEs [123] --> Loop 74 
* CEs [122] --> Loop 75 
* CEs [121] --> Loop 76 
* CEs [120] --> Loop 77 
* CEs [115] --> Loop 78 
* CEs [116,117,118,119] --> Loop 79 

### Ranking functions of CR rand(V,V6,Out) 
* RF of phase [72,73,74]: [V-1]

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


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


### Cost equations --> "Loop" of random/2 
* CEs [131] --> Loop 80 
* CEs [130] --> Loop 81 
* CEs [128] --> Loop 82 
* CEs [126,127,129,132] --> 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 [133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153] 
* CE 3 is refined into CE [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] 
* CE 4 is refined into CE [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,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261] 
* CE 1 is refined into CE [262] 
* CE 5 is refined into CE [263] 
* CE 6 is refined into CE [264,265,266] 
* CE 7 is refined into CE [267,268] 
* CE 8 is refined into CE [269,270] 
* CE 9 is refined into CE [271,272,273,274,275,276,277,278] 
* CE 10 is refined into CE [279,280,281,282,283,284,285,286] 
* CE 11 is refined into CE [287,288,289] 
* CE 12 is refined into CE [290,291] 
* CE 13 is refined into CE [292,293,294] 
* CE 14 is refined into CE [295,296,297,298] 
* CE 15 is refined into CE [299,300,301,302,303,304] 


### Cost equations --> "Loop" of start/3 
* CEs [133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,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,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] --> Loop 84 
* CEs [263] --> Loop 85 
* CEs [262,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,299,300,301,302,303,304] --> Loop 86 

### 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 [26]: 1
  with precondition: [V=0,Out=1] 

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

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


#### Cost of chains of fun1(V,Out):
* Chain [[27],28]: 1*it(27)+1
  Such that:it(27) =< Out

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

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


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

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


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

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

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


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

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


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

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

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


#### Cost of chains of fun4(V,V6,Out):
* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],71]: 42*it(39)+1*s(13)+5*s(14)+2
  Such that:aux(9) =< V
it(39) =< aux(9)
aux(2) =< aux(9)
s(13) =< it(39)*aux(9)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],69]: 42*it(39)+1*s(13)+5*s(14)+2
  Such that:aux(10) =< V
it(39) =< aux(10)
aux(2) =< aux(10)
s(13) =< it(39)*aux(10)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],68,71]: 42*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(11) =< V
it(39) =< aux(11)
aux(2) =< aux(11)
s(13) =< it(39)*aux(11)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],68,70]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(12) =< V
it(39) =< aux(12)
aux(2) =< aux(12)
s(13) =< it(39)*aux(12)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],67,71]: 42*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(13) =< V
it(39) =< aux(13)
aux(2) =< aux(13)
s(13) =< it(39)*aux(13)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],67,70]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(14) =< V
it(39) =< aux(14)
aux(2) =< aux(14)
s(13) =< it(39)*aux(14)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],66,71]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(15) =< V
it(39) =< aux(15)
aux(2) =< aux(15)
s(13) =< it(39)*aux(15)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],66,70]: 42*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(16) =< V
it(39) =< aux(16)
aux(2) =< aux(16)
s(13) =< it(39)*aux(16)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],65,71]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(17) =< V
it(39) =< aux(17)
aux(2) =< aux(17)
s(13) =< it(39)*aux(17)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],65,70]: 42*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(18) =< V
it(39) =< aux(18)
aux(2) =< aux(18)
s(13) =< it(39)*aux(18)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],64,71]: 43*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(19) =< V
it(39) =< aux(19)
aux(2) =< aux(19)
s(13) =< it(39)*aux(19)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],64,70]: 43*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(20) =< V
it(39) =< aux(20)
aux(2) =< aux(20)
s(13) =< it(39)*aux(20)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=7] 

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],63,71]: 43*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(21) =< V
it(39) =< aux(21)
aux(2) =< aux(21)
s(13) =< it(39)*aux(21)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=8] 

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],63,70]: 43*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(22) =< V
it(39) =< aux(22)
aux(2) =< aux(22)
s(13) =< it(39)*aux(22)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=9] 

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],62,71]: 42*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(23) =< V
it(39) =< aux(23)
aux(2) =< aux(23)
s(13) =< it(39)*aux(23)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],62,70]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(24) =< V
it(39) =< aux(24)
aux(2) =< aux(24)
s(13) =< it(39)*aux(24)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],61,71]: 42*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(25) =< V
it(39) =< aux(25)
aux(2) =< aux(25)
s(13) =< it(39)*aux(25)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],61,70]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(26) =< V
it(39) =< aux(26)
aux(2) =< aux(26)
s(13) =< it(39)*aux(26)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],60,71]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(27) =< V
it(39) =< aux(27)
aux(2) =< aux(27)
s(13) =< it(39)*aux(27)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],60,70]: 42*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(28) =< V
it(39) =< aux(28)
aux(2) =< aux(28)
s(13) =< it(39)*aux(28)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],59,71]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(29) =< V
it(39) =< aux(29)
aux(2) =< aux(29)
s(13) =< it(39)*aux(29)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],59,70]: 42*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(30) =< V
it(39) =< aux(30)
aux(2) =< aux(30)
s(13) =< it(39)*aux(30)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],58,71]: 43*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(31) =< V
it(39) =< aux(31)
aux(2) =< aux(31)
s(13) =< it(39)*aux(31)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],58,70]: 43*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(32) =< V
it(39) =< aux(32)
aux(2) =< aux(32)
s(13) =< it(39)*aux(32)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=7] 

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],57,71]: 43*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(33) =< V
it(39) =< aux(33)
aux(2) =< aux(33)
s(13) =< it(39)*aux(33)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=8] 

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],57,70]: 43*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(34) =< V
it(39) =< aux(34)
aux(2) =< aux(34)
s(13) =< it(39)*aux(34)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=9] 

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],56,71]: 42*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(35) =< V
it(39) =< aux(35)
aux(2) =< aux(35)
s(13) =< it(39)*aux(35)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],56,70]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(36) =< V
it(39) =< aux(36)
aux(2) =< aux(36)
s(13) =< it(39)*aux(36)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],55,71]: 42*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(37) =< V
it(39) =< aux(37)
aux(2) =< aux(37)
s(13) =< it(39)*aux(37)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],55,70]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(38) =< V
it(39) =< aux(38)
aux(2) =< aux(38)
s(13) =< it(39)*aux(38)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],54,71]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(39) =< V
it(39) =< aux(39)
aux(2) =< aux(39)
s(13) =< it(39)*aux(39)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],54,70]: 42*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(40) =< V
it(39) =< aux(40)
aux(2) =< aux(40)
s(13) =< it(39)*aux(40)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],53,71]: 42*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(41) =< V
it(39) =< aux(41)
aux(2) =< aux(41)
s(13) =< it(39)*aux(41)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],53,70]: 42*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(42) =< V
it(39) =< aux(42)
aux(2) =< aux(42)
s(13) =< it(39)*aux(42)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],52,71]: 43*it(39)+1*s(13)+5*s(14)+5
  Such that:aux(43) =< V
it(39) =< aux(43)
aux(2) =< aux(43)
s(13) =< it(39)*aux(43)
s(14) =< it(39)*aux(2)

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

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],52,70]: 43*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(44) =< V
it(39) =< aux(44)
aux(2) =< aux(44)
s(13) =< it(39)*aux(44)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=7] 

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],51,71]: 43*it(39)+1*s(13)+5*s(14)+6
  Such that:aux(45) =< V
it(39) =< aux(45)
aux(2) =< aux(45)
s(13) =< it(39)*aux(45)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=8] 

* Chain [[39,40,41,42,43,44,45,46,47,48,49,50],51,70]: 43*it(39)+1*s(13)+5*s(14)+7
  Such that:aux(46) =< V
it(39) =< aux(46)
aux(2) =< aux(46)
s(13) =< it(39)*aux(46)
s(14) =< it(39)*aux(2)

  with precondition: [V>=3,V6>=0,Out>=9] 

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

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

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

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

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

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

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

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

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

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

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

* Chain [64,71]: 1*s(19)+5
  Such that:s(19) =< V

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

* Chain [64,70]: 1*s(19)+6
  Such that:s(19) =< V

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

* Chain [63,71]: 1*s(20)+6
  Such that:s(20) =< V

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

* Chain [63,70]: 1*s(20)+7
  Such that:s(20) =< V

  with precondition: [V6>=0,Out>=7,V+5>=Out] 

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

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

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

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

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

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

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

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

* Chain [58,71]: 1*s(21)+5
  Such that:s(21) =< V

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

* Chain [58,70]: 1*s(21)+6
  Such that:s(21) =< V

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

* Chain [57,71]: 1*s(22)+6
  Such that:s(22) =< V

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

* Chain [57,70]: 1*s(22)+7
  Such that:s(22) =< V

  with precondition: [V6>=0,Out>=7,V+5>=Out] 

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

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

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

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

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

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

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

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

* Chain [52,71]: 1*s(23)+5
  Such that:s(23) =< V

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

* Chain [52,70]: 1*s(23)+6
  Such that:s(23) =< V

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

* Chain [51,71]: 1*s(24)+6
  Such that:s(24) =< V

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

* Chain [51,70]: 1*s(24)+7
  Such that:s(24) =< V

  with precondition: [V6>=0,Out>=7,V+5>=Out] 


#### Cost of chains of rand(V,V6,Out):
* Chain [[72,73,74],79]: 0
  with precondition: [Out=0,V>=2,V6>=0] 

* Chain [[72,73,74],77,79]: 0
  with precondition: [Out=0,V>=2,V6>=0] 

* Chain [[72,73,74],77,78]: 0
  with precondition: [Out=0,V>=2,V6>=0] 

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

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

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

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

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

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

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

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

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

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

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

* Chain [75,78]: 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: [Out=1,V>=1] 

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

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


#### Cost of chains of start(V,V6,V10):
* Chain [86]: 3241*s(227)+76*s(231)+380*s(232)+8
  Such that:aux(50) =< V
s(227) =< aux(50)
s(230) =< aux(50)
s(231) =< s(227)*aux(50)
s(232) =< s(227)*s(230)

  with precondition: [V>=0] 

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

* Chain [84]: 19467*s(239)+456*s(241)+2280*s(242)+9
  Such that:aux(54) =< V6
s(239) =< aux(54)
s(240) =< aux(54)
s(241) =< s(239)*aux(54)
s(242) =< s(239)*s(240)

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


Closed-form bounds of start(V,V6,V10): 
-------------------------------------
* Chain [86] with precondition: [V>=0] 
    - Upper bound: 3241*V+8+456*V*V 
    - Complexity: n^2 
* Chain [85] with precondition: [V=1,V6>=0,V10>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [84] with precondition: [V=2,V6>=0,V10>=0] 
    - Upper bound: 19467*V6+9+2736*V6*V6 
    - Complexity: n^2 

### Maximum cost of start(V,V6,V10): max([3241*V+7+456*V*V,nat(V6)*19467+8+nat(V6)*2736*nat(V6)])+1 
Asymptotic class: n^2 
* Total analysis performed in 2881 ms.


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

(12)
BOUNDS(1, n^2)

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

(13) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

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

The (relative) TRS S consists of the following 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))

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

(15) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
ID_INC/0

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

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


The TRS R consists of the following rules:

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

The (relative) TRS S consists of the following 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))

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

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

(18)
Obligation:
Innermost TRS:
Rules:
NONZERO(0') -> c
NONZERO(s(z0)) -> c1
P(s(0')) -> c2
P(s(s(z0))) -> c3(P(s(z0)))
ID_INC -> c4
ID_INC -> 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)
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))

Types:
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 -> c2:c3
ID_INC :: 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
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c33_11 :: c2:c3
hole_c4:c54_11 :: c4:c5
hole_c65_11 :: c6
hole_c76_11 :: c7
hole_c8:c9:c107_11 :: c8:c9:c10
hole_false:true8_11 :: false:true
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c310_11 :: Nat -> c2:c3

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

(19) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
P, RAND, p, rand

They will be analysed ascendingly in the following order:
P < RAND
p < RAND
p < rand

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

(20)
Obligation:
Innermost TRS:
Rules:
NONZERO(0') -> c
NONZERO(s(z0)) -> c1
P(s(0')) -> c2
P(s(s(z0))) -> c3(P(s(z0)))
ID_INC -> c4
ID_INC -> 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)
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))

Types:
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 -> c2:c3
ID_INC :: 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
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c33_11 :: c2:c3
hole_c4:c54_11 :: c4:c5
hole_c65_11 :: c6
hole_c76_11 :: c7
hole_c8:c9:c107_11 :: c8:c9:c10
hole_false:true8_11 :: false:true
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c310_11 :: Nat -> c2:c3


Generator Equations:
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c310_11(0) <=> c2
gen_c2:c310_11(+(x, 1)) <=> c3(gen_c2:c310_11(x))


The following defined symbols remain to be analysed:
P, RAND, p, rand

They will be analysed ascendingly in the following order:
P < RAND
p < RAND
p < rand

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
P(gen_0':s9_11(+(1, n12_11))) -> gen_c2:c310_11(n12_11), rt in Omega(1 + n12_11)

Induction Base:
P(gen_0':s9_11(+(1, 0))) ->_R^Omega(1)
c2

Induction Step:
P(gen_0':s9_11(+(1, +(n12_11, 1)))) ->_R^Omega(1)
c3(P(s(gen_0':s9_11(n12_11)))) ->_IH
c3(gen_c2:c310_11(c13_11))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(22)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
NONZERO(0') -> c
NONZERO(s(z0)) -> c1
P(s(0')) -> c2
P(s(s(z0))) -> c3(P(s(z0)))
ID_INC -> c4
ID_INC -> 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)
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))

Types:
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 -> c2:c3
ID_INC :: 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
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c33_11 :: c2:c3
hole_c4:c54_11 :: c4:c5
hole_c65_11 :: c6
hole_c76_11 :: c7
hole_c8:c9:c107_11 :: c8:c9:c10
hole_false:true8_11 :: false:true
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c310_11 :: Nat -> c2:c3


Generator Equations:
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c310_11(0) <=> c2
gen_c2:c310_11(+(x, 1)) <=> c3(gen_c2:c310_11(x))


The following defined symbols remain to be analysed:
P, RAND, p, rand

They will be analysed ascendingly in the following order:
P < RAND
p < RAND
p < rand

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

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

(25)
BOUNDS(n^1, INF)

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

(26)
Obligation:
Innermost TRS:
Rules:
NONZERO(0') -> c
NONZERO(s(z0)) -> c1
P(s(0')) -> c2
P(s(s(z0))) -> c3(P(s(z0)))
ID_INC -> c4
ID_INC -> 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)
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))

Types:
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 -> c2:c3
ID_INC :: 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
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c33_11 :: c2:c3
hole_c4:c54_11 :: c4:c5
hole_c65_11 :: c6
hole_c76_11 :: c7
hole_c8:c9:c107_11 :: c8:c9:c10
hole_false:true8_11 :: false:true
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c310_11 :: Nat -> c2:c3


Lemmas:
P(gen_0':s9_11(+(1, n12_11))) -> gen_c2:c310_11(n12_11), rt in Omega(1 + n12_11)


Generator Equations:
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c310_11(0) <=> c2
gen_c2:c310_11(+(x, 1)) <=> c3(gen_c2:c310_11(x))


The following defined symbols remain to be analysed:
p, RAND, rand

They will be analysed ascendingly in the following order:
p < RAND
p < rand

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
p(gen_0':s9_11(+(1, n315_11))) -> gen_0':s9_11(n315_11), rt in Omega(0)

Induction Base:
p(gen_0':s9_11(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
p(gen_0':s9_11(+(1, +(n315_11, 1)))) ->_R^Omega(0)
s(p(s(gen_0':s9_11(n315_11)))) ->_IH
s(gen_0':s9_11(c316_11))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
NONZERO(0') -> c
NONZERO(s(z0)) -> c1
P(s(0')) -> c2
P(s(s(z0))) -> c3(P(s(z0)))
ID_INC -> c4
ID_INC -> 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)
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))

Types:
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 -> c2:c3
ID_INC :: 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
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c33_11 :: c2:c3
hole_c4:c54_11 :: c4:c5
hole_c65_11 :: c6
hole_c76_11 :: c7
hole_c8:c9:c107_11 :: c8:c9:c10
hole_false:true8_11 :: false:true
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c310_11 :: Nat -> c2:c3


Lemmas:
P(gen_0':s9_11(+(1, n12_11))) -> gen_c2:c310_11(n12_11), rt in Omega(1 + n12_11)
p(gen_0':s9_11(+(1, n315_11))) -> gen_0':s9_11(n315_11), rt in Omega(0)


Generator Equations:
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c310_11(0) <=> c2
gen_c2:c310_11(+(x, 1)) <=> c3(gen_c2:c310_11(x))


The following defined symbols remain to be analysed:
RAND, rand
----------------------------------------

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
RAND(gen_0':s9_11(n594_11), gen_0':s9_11(b)) -> *11_11, rt in Omega(n594_11 + n594_11^2)

Induction Base:
RAND(gen_0':s9_11(0), gen_0':s9_11(b))

Induction Step:
RAND(gen_0':s9_11(+(n594_11, 1)), gen_0':s9_11(b)) ->_R^Omega(1)
c7(IF(nonZero(gen_0':s9_11(+(n594_11, 1))), gen_0':s9_11(+(n594_11, 1)), gen_0':s9_11(b)), NONZERO(gen_0':s9_11(+(n594_11, 1)))) ->_R^Omega(0)
c7(IF(true, gen_0':s9_11(+(1, n594_11)), gen_0':s9_11(b)), NONZERO(gen_0':s9_11(+(1, n594_11)))) ->_R^Omega(1)
c7(c9(RAND(p(gen_0':s9_11(+(1, n594_11))), id_inc(gen_0':s9_11(b))), P(gen_0':s9_11(+(1, n594_11)))), NONZERO(gen_0':s9_11(+(1, n594_11)))) ->_L^Omega(0)
c7(c9(RAND(gen_0':s9_11(n594_11), id_inc(gen_0':s9_11(b))), P(gen_0':s9_11(+(1, n594_11)))), NONZERO(gen_0':s9_11(+(1, n594_11)))) ->_R^Omega(0)
c7(c9(RAND(gen_0':s9_11(n594_11), gen_0':s9_11(b)), P(gen_0':s9_11(+(1, n594_11)))), NONZERO(gen_0':s9_11(+(1, n594_11)))) ->_IH
c7(c9(*11_11, P(gen_0':s9_11(+(1, n594_11)))), NONZERO(gen_0':s9_11(+(1, n594_11)))) ->_L^Omega(1 + n594_11)
c7(c9(*11_11, gen_c2:c310_11(n594_11)), NONZERO(gen_0':s9_11(+(1, n594_11)))) ->_R^Omega(1)
c7(c9(*11_11, gen_c2:c310_11(n594_11)), c1)

We have rt in Omega(n^2) and sz in O(n). Thus, we have irc_R in Omega(n^2).
----------------------------------------

(30)
Complex Obligation (BEST)

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

(31)
Obligation:
Proved the lower bound n^2 for the following obligation:

Innermost TRS:
Rules:
NONZERO(0') -> c
NONZERO(s(z0)) -> c1
P(s(0')) -> c2
P(s(s(z0))) -> c3(P(s(z0)))
ID_INC -> c4
ID_INC -> 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)
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))

Types:
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 -> c2:c3
ID_INC :: 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
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c33_11 :: c2:c3
hole_c4:c54_11 :: c4:c5
hole_c65_11 :: c6
hole_c76_11 :: c7
hole_c8:c9:c107_11 :: c8:c9:c10
hole_false:true8_11 :: false:true
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c310_11 :: Nat -> c2:c3


Lemmas:
P(gen_0':s9_11(+(1, n12_11))) -> gen_c2:c310_11(n12_11), rt in Omega(1 + n12_11)
p(gen_0':s9_11(+(1, n315_11))) -> gen_0':s9_11(n315_11), rt in Omega(0)


Generator Equations:
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c310_11(0) <=> c2
gen_c2:c310_11(+(x, 1)) <=> c3(gen_c2:c310_11(x))


The following defined symbols remain to be analysed:
RAND, rand
----------------------------------------

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

(33)
BOUNDS(n^2, INF)

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

(34)
Obligation:
Innermost TRS:
Rules:
NONZERO(0') -> c
NONZERO(s(z0)) -> c1
P(s(0')) -> c2
P(s(s(z0))) -> c3(P(s(z0)))
ID_INC -> c4
ID_INC -> 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)
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))

Types:
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 -> c2:c3
ID_INC :: 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
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c33_11 :: c2:c3
hole_c4:c54_11 :: c4:c5
hole_c65_11 :: c6
hole_c76_11 :: c7
hole_c8:c9:c107_11 :: c8:c9:c10
hole_false:true8_11 :: false:true
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c310_11 :: Nat -> c2:c3


Lemmas:
P(gen_0':s9_11(+(1, n12_11))) -> gen_c2:c310_11(n12_11), rt in Omega(1 + n12_11)
p(gen_0':s9_11(+(1, n315_11))) -> gen_0':s9_11(n315_11), rt in Omega(0)
RAND(gen_0':s9_11(n594_11), gen_0':s9_11(b)) -> *11_11, rt in Omega(n594_11 + n594_11^2)


Generator Equations:
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c310_11(0) <=> c2
gen_c2:c310_11(+(x, 1)) <=> c3(gen_c2:c310_11(x))


The following defined symbols remain to be analysed:
rand
----------------------------------------

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
rand(gen_0':s9_11(n7461_11), gen_0':s9_11(b)) -> gen_0':s9_11(b), rt in Omega(0)

Induction Base:
rand(gen_0':s9_11(0), gen_0':s9_11(b)) ->_R^Omega(0)
if(nonZero(gen_0':s9_11(0)), gen_0':s9_11(0), gen_0':s9_11(b)) ->_R^Omega(0)
if(false, gen_0':s9_11(0), gen_0':s9_11(b)) ->_R^Omega(0)
gen_0':s9_11(b)

Induction Step:
rand(gen_0':s9_11(+(n7461_11, 1)), gen_0':s9_11(b)) ->_R^Omega(0)
if(nonZero(gen_0':s9_11(+(n7461_11, 1))), gen_0':s9_11(+(n7461_11, 1)), gen_0':s9_11(b)) ->_R^Omega(0)
if(true, gen_0':s9_11(+(1, n7461_11)), gen_0':s9_11(b)) ->_R^Omega(0)
rand(p(gen_0':s9_11(+(1, n7461_11))), id_inc(gen_0':s9_11(b))) ->_L^Omega(0)
rand(gen_0':s9_11(n7461_11), id_inc(gen_0':s9_11(b))) ->_R^Omega(0)
rand(gen_0':s9_11(n7461_11), gen_0':s9_11(b)) ->_IH
gen_0':s9_11(b)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(36)
BOUNDS(1, INF)