WORST_CASE(?,O(n^1))
proof of input_ht8PgXrps9.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
(4) CdtProblem
(5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CdtProblem
(9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CpxRelTRS
(11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CpxWeightedTrs
(13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxTypedWeightedTrs
(15) CompletionProof [UPPER BOUND(ID), 0 ms]
(16) CpxTypedWeightedCompleteTrs
(17) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
(18) CpxTypedWeightedCompleteTrs
(19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(20) CpxRNTS
(21) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
(22) CpxRNTS
(23) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
(24) CpxRNTS
(25) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(26) CpxRNTS
(27) IntTrsBoundProof [UPPER BOUND(ID), 117 ms]
(28) CpxRNTS
(29) IntTrsBoundProof [UPPER BOUND(ID), 12 ms]
(30) CpxRNTS
(31) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(32) CpxRNTS
(33) IntTrsBoundProof [UPPER BOUND(ID), 177 ms]
(34) CpxRNTS
(35) IntTrsBoundProof [UPPER BOUND(ID), 4 ms]
(36) CpxRNTS
(37) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(38) CpxRNTS
(39) IntTrsBoundProof [UPPER BOUND(ID), 921 ms]
(40) CpxRNTS
(41) IntTrsBoundProof [UPPER BOUND(ID), 583 ms]
(42) CpxRNTS
(43) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(44) CpxRNTS
(45) IntTrsBoundProof [UPPER BOUND(ID), 137 ms]
(46) CpxRNTS
(47) IntTrsBoundProof [UPPER BOUND(ID), 53 ms]
(48) CpxRNTS
(49) FinalProof [FINISHED, 0 ms]
(50) BOUNDS(1, n^1)


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

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


The TRS R consists of the following rules:

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

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   nonZero(0) -> false
   nonZero(s(z0)) -> true
   p(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))
Tuples:
   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))
S tuples:
   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))
K tuples:none
Defined Rule Symbols:   nonZero_1, p_1, id_inc_1, random_1, rand_2, if_3

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

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


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

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

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))
Tuples:
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1))
S tuples:
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1), NONZERO(z0))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)), P(z0))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)), ID_INC(z1))
K tuples:none
Defined Rule Symbols:   nonZero_1, p_1, id_inc_1, random_1, rand_2, if_3

Defined Pair Symbols:   RAND_2, IF_3

Compound Symbols:   c7_2, c9_2, c10_2


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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

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))
Tuples:
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)))
S tuples:
   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)))
   IF(true, z0, z1) -> c10(RAND(p(z0), id_inc(z1)))
K tuples:none
Defined Rule Symbols:   nonZero_1, p_1, id_inc_1, random_1, rand_2, if_3

Defined Pair Symbols:   RAND_2, IF_3

Compound Symbols:   c7_1, c9_1, c10_1


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

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

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

(8)
Obligation:
Complexity Dependency Tuples Problem

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

Defined Pair Symbols:   RAND_2, IF_3

Compound Symbols:   c7_1, c9_1, c10_1


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

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

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


The TRS R consists of the following rules:

   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1))
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1)))
   IF(true, z0, z1) -> c10(RAND(p(z0), 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)

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

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

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


The TRS R consists of the following rules:

   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1)) [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1))) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), 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]

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

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

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

   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1)) [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1))) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), 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]

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

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

(15) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

   RAND_2
   IF_3

(c) The following functions are completely defined:

   nonZero_1
   p_1
   id_inc_1

Due to the following rules being added:

   nonZero(v0) -> null_nonZero [0]
   p(v0) -> 0 [0]
   id_inc(v0) -> 0 [0]

And the following fresh constants:    null_nonZero, const, const1

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

(16)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   RAND(z0, z1) -> c7(IF(nonZero(z0), z0, z1)) [1]
   IF(true, z0, z1) -> c9(RAND(p(z0), id_inc(z1))) [1]
   IF(true, z0, z1) -> c10(RAND(p(z0), 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]
   nonZero(v0) -> null_nonZero [0]
   p(v0) -> 0 [0]
   id_inc(v0) -> 0 [0]

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

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

(17) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(18)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   RAND(0, z1) -> c7(IF(false, 0, z1)) [1]
   RAND(s(z0'), z1) -> c7(IF(true, s(z0'), z1)) [1]
   RAND(z0, z1) -> c7(IF(null_nonZero, z0, z1)) [1]
   IF(true, 0, z1) -> c9(RAND(0, z1)) [1]
   IF(true, 0, z1) -> c9(RAND(0, s(z1))) [1]
   IF(true, 0, z1) -> c9(RAND(0, 0)) [1]
   IF(true, s(z0''), z1) -> c9(RAND(z0'', z1)) [1]
   IF(true, s(z0''), z1) -> c9(RAND(z0'', s(z1))) [1]
   IF(true, s(z0''), z1) -> c9(RAND(z0'', 0)) [1]
   IF(true, z0, z1) -> c9(RAND(0, z1)) [1]
   IF(true, z0, z1) -> c9(RAND(0, s(z1))) [1]
   IF(true, z0, z1) -> c9(RAND(0, 0)) [1]
   IF(true, 0, z1) -> c10(RAND(0, z1)) [1]
   IF(true, 0, z1) -> c10(RAND(0, s(z1))) [1]
   IF(true, 0, z1) -> c10(RAND(0, 0)) [1]
   IF(true, s(z01), z1) -> c10(RAND(z01, z1)) [1]
   IF(true, s(z01), z1) -> c10(RAND(z01, s(z1))) [1]
   IF(true, s(z01), z1) -> c10(RAND(z01, 0)) [1]
   IF(true, z0, z1) -> c10(RAND(0, z1)) [1]
   IF(true, z0, z1) -> c10(RAND(0, s(z1))) [1]
   IF(true, z0, z1) -> c10(RAND(0, 0)) [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]
   nonZero(v0) -> null_nonZero [0]
   p(v0) -> 0 [0]
   id_inc(v0) -> 0 [0]

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

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

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

   true => 2
   0 => 0
   false => 1
   null_nonZero => 0
   const => 0
   const1 => 0

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

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(z0'', z1) :|: z = 2, z1 >= 0, z' = 1 + z0'', z0'' >= 0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z0'', 0) :|: z = 2, z1 >= 0, z' = 1 + z0'', z0'' >= 0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z0'', 1 + z1) :|: z = 2, z1 >= 0, z' = 1 + z0'', z0'' >= 0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z01, z1) :|: z = 2, z1 >= 0, z01 >= 0, z' = 1 + z01, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z01, 0) :|: z = 2, z1 >= 0, z01 >= 0, z' = 1 + z01, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z01, 1 + z1) :|: z = 2, z1 >= 0, z01 >= 0, z' = 1 + z01, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z1) :|: z = 2, z1 >= 0, z' = 0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z1 >= 0, z' = 0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z1) :|: z = 2, z1 >= 0, z' = 0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + z0', z1) :|: z1 >= 0, z0' >= 0, z' = z1, z = 1 + z0'
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z1) :|: z1 >= 0, z' = z1, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   id_inc(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0
   id_inc(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   id_inc(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0
   nonZero(z) -{ 0 }-> 2 :|: z = 1 + z0, z0 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   p(z) -{ 0 }-> z0 :|: z = 1 + z0, z0 >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0


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

(21) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0


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

(23) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { nonZero }
   { id_inc }
   { RAND, IF }
   { p }

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

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {nonZero}, {id_inc}, {RAND,IF}, {p}

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

(25) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {nonZero}, {id_inc}, {RAND,IF}, {p}

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

(27) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: nonZero
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 2

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

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {nonZero}, {id_inc}, {RAND,IF}, {p}
Previous analysis results are:
  nonZero: runtime: ?, size: O(1) [2]

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

(29) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: nonZero
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {id_inc}, {RAND,IF}, {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]

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

(31) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {id_inc}, {RAND,IF}, {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]

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

(33) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: id_inc
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z

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

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {id_inc}, {RAND,IF}, {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]
  id_inc: runtime: ?, size: O(n^1) [1 + z]

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

(35) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: id_inc
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {RAND,IF}, {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]
  id_inc: runtime: O(1) [0], size: O(n^1) [1 + z]

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

(37) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {RAND,IF}, {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]
  id_inc: runtime: O(1) [0], size: O(n^1) [1 + z]

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

(39) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: RAND
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

Computed SIZE bound using CoFloCo for: IF
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

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

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {RAND,IF}, {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]
  id_inc: runtime: O(1) [0], size: O(n^1) [1 + z]
  RAND: runtime: ?, size: O(1) [0]
  IF: runtime: ?, size: O(1) [1]

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

(41) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: RAND
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 5 + 2*z

Computed RUNTIME bound using CoFloCo for: IF
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 6 + 2*z'

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

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

   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 0) :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(0, 1 + z'') :|: z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 0) :|: z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + RAND(z' - 1, 1 + z'') :|: z = 2, z'' >= 0, z' - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(2, 1 + (z - 1), z') :|: z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 1 }-> 1 + IF(1, 0, z') :|: z' >= 0, z = 0
   RAND(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]
  id_inc: runtime: O(1) [0], size: O(n^1) [1 + z]
  RAND: runtime: O(n^1) [5 + 2*z], size: O(1) [0]
  IF: runtime: O(n^1) [6 + 2*z'], size: O(1) [1]

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

(43) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   IF(z, z', z'') -{ 6 }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 6 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 6 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s5 :|: s5 >= 0, s5 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s6 :|: s6 >= 0, s6 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s7 :|: s7 >= 0, s7 <= 0, z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s8 :|: s8 >= 0, s8 <= 0, z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s9 :|: s9 >= 0, s9 <= 0, z = 2, z'' >= 0, z' >= 0
   RAND(z, z') -{ 7 }-> 1 + s :|: s >= 0, s <= 1, z' >= 0, z = 0
   RAND(z, z') -{ 7 + 2*z }-> 1 + s' :|: s' >= 0, s' <= 1, z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 7 + 2*z }-> 1 + s'' :|: s'' >= 0, s'' <= 1, z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]
  id_inc: runtime: O(1) [0], size: O(n^1) [1 + z]
  RAND: runtime: O(n^1) [5 + 2*z], size: O(1) [0]
  IF: runtime: O(n^1) [6 + 2*z'], size: O(1) [1]

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

(45) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: p
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

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

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

   IF(z, z', z'') -{ 6 }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 6 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 6 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s5 :|: s5 >= 0, s5 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s6 :|: s6 >= 0, s6 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s7 :|: s7 >= 0, s7 <= 0, z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s8 :|: s8 >= 0, s8 <= 0, z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s9 :|: s9 >= 0, s9 <= 0, z = 2, z'' >= 0, z' >= 0
   RAND(z, z') -{ 7 }-> 1 + s :|: s >= 0, s <= 1, z' >= 0, z = 0
   RAND(z, z') -{ 7 + 2*z }-> 1 + s' :|: s' >= 0, s' <= 1, z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 7 + 2*z }-> 1 + s'' :|: s'' >= 0, s'' <= 1, z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: {p}
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]
  id_inc: runtime: O(1) [0], size: O(n^1) [1 + z]
  RAND: runtime: O(n^1) [5 + 2*z], size: O(1) [0]
  IF: runtime: O(n^1) [6 + 2*z'], size: O(1) [1]
  p: runtime: ?, size: O(n^1) [z]

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

(47) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: p
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

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

   IF(z, z', z'') -{ 6 }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 6 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 6 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z = 2, z'' >= 0, z' = 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s5 :|: s5 >= 0, s5 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 4 + 2*z' }-> 1 + s6 :|: s6 >= 0, s6 <= 0, z = 2, z'' >= 0, z' - 1 >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s7 :|: s7 >= 0, s7 <= 0, z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s8 :|: s8 >= 0, s8 <= 0, z = 2, z'' >= 0, z' >= 0
   IF(z, z', z'') -{ 6 }-> 1 + s9 :|: s9 >= 0, s9 <= 0, z = 2, z'' >= 0, z' >= 0
   RAND(z, z') -{ 7 }-> 1 + s :|: s >= 0, s <= 1, z' >= 0, z = 0
   RAND(z, z') -{ 7 + 2*z }-> 1 + s' :|: s' >= 0, s' <= 1, z' >= 0, z - 1 >= 0
   RAND(z, z') -{ 7 + 2*z }-> 1 + s'' :|: s'' >= 0, s'' <= 1, z' >= 0, z >= 0
   id_inc(z) -{ 0 }-> z :|: z >= 0
   id_inc(z) -{ 0 }-> 0 :|: z >= 0
   id_inc(z) -{ 0 }-> 1 + z :|: z >= 0
   nonZero(z) -{ 0 }-> 2 :|: z - 1 >= 0
   nonZero(z) -{ 0 }-> 1 :|: z = 0
   nonZero(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> 0 :|: z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  nonZero: runtime: O(1) [0], size: O(1) [2]
  id_inc: runtime: O(1) [0], size: O(n^1) [1 + z]
  RAND: runtime: O(n^1) [5 + 2*z], size: O(1) [0]
  IF: runtime: O(n^1) [6 + 2*z'], size: O(1) [1]
  p: runtime: O(1) [0], size: O(n^1) [z]

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

(49) FinalProof (FINISHED)
Computed overall runtime complexity
----------------------------------------

(50)
BOUNDS(1, n^1)