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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 2021 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, 22.1 s]
    (12) BOUNDS(1, n^1)
(13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxRelTRS
    (15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) typed CpxTrs
    (17) OrderProof [LOWER BOUND(ID), 0 ms]
    (18) typed CpxTrs
    (19) RewriteLemmaProof [LOWER BOUND(ID), 357 ms]
    (20) BEST
        (21) proven lower bound
            (22) LowerBoundPropagationProof [FINISHED, 0 ms]
            (23) BOUNDS(n^1, INF)
        (24) typed CpxTrs
            (25) RewriteLemmaProof [LOWER BOUND(ID), 88 ms]
            (26) typed CpxTrs
            (27) RewriteLemmaProof [LOWER BOUND(ID), 56 ms]
            (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 39 ms]
            (30) typed CpxTrs


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

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


The TRS R consists of the following rules:

   GE(z0, 0) -> c
   GE(0, s(z0)) -> c1
   GE(s(z0), s(z1)) -> c2(GE(z0, z1))
   MINUS(z0, 0) -> c3
   MINUS(0, z0) -> c4
   MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
   ID_INC(z0) -> c6
   ID_INC(z0) -> c7
   DIV(z0, z1) -> c8(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z1, s(0)))
   DIV(z0, z1) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z0, z1))
   IF(false, z0, z1, z2) -> c10
   IF(true, false, z0, z1) -> c11
   IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))

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

   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   minus(z0, 0) -> z0
   minus(0, z0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   id_inc(z0) -> z0
   id_inc(z0) -> s(z0)
   div(z0, z1) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1)
   if(false, z0, z1, z2) -> div_by_zero
   if(true, false, z0, z1) -> 0
   if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

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

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

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


The TRS R consists of the following rules:

   GE(z0, 0) -> c
   GE(0, s(z0)) -> c1
   GE(s(z0), s(z1)) -> c2(GE(z0, z1))
   MINUS(z0, 0) -> c3
   MINUS(0, z0) -> c4
   MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
   ID_INC(z0) -> c6
   ID_INC(z0) -> c7
   DIV(z0, z1) -> c8(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z1, s(0)))
   DIV(z0, z1) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z0, z1))
   IF(false, z0, z1, z2) -> c10
   IF(true, false, z0, z1) -> c11
   IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))

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

   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   minus(z0, 0) -> z0
   minus(0, z0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   id_inc(z0) -> z0
   id_inc(z0) -> s(z0)
   div(z0, z1) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1)
   if(false, z0, z1, z2) -> div_by_zero
   if(true, false, z0, z1) -> 0
   if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

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

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

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


The TRS R consists of the following rules:

   GE(z0, 0) -> c [1]
   GE(0, s(z0)) -> c1 [1]
   GE(s(z0), s(z1)) -> c2(GE(z0, z1)) [1]
   MINUS(z0, 0) -> c3 [1]
   MINUS(0, z0) -> c4 [1]
   MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) [1]
   ID_INC(z0) -> c6 [1]
   ID_INC(z0) -> c7 [1]
   DIV(z0, z1) -> c8(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z1, s(0))) [1]
   DIV(z0, z1) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z0, z1)) [1]
   IF(false, z0, z1, z2) -> c10 [1]
   IF(true, false, z0, z1) -> c11 [1]
   IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1)) [1]
   ge(z0, 0) -> true [0]
   ge(0, s(z0)) -> false [0]
   ge(s(z0), s(z1)) -> ge(z0, z1) [0]
   minus(z0, 0) -> z0 [0]
   minus(0, z0) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   div(z0, z1) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1) [0]
   if(false, z0, z1, z2) -> div_by_zero [0]
   if(true, false, z0, z1) -> 0 [0]
   if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), 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:

   GE(z0, 0) -> c [1]
   GE(0, s(z0)) -> c1 [1]
   GE(s(z0), s(z1)) -> c2(GE(z0, z1)) [1]
   MINUS(z0, 0) -> c3 [1]
   MINUS(0, z0) -> c4 [1]
   MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) [1]
   ID_INC(z0) -> c6 [1]
   ID_INC(z0) -> c7 [1]
   DIV(z0, z1) -> c8(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z1, s(0))) [1]
   DIV(z0, z1) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z0, z1)) [1]
   IF(false, z0, z1, z2) -> c10 [1]
   IF(true, false, z0, z1) -> c11 [1]
   IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1)) [1]
   ge(z0, 0) -> true [0]
   ge(0, s(z0)) -> false [0]
   ge(s(z0), s(z1)) -> ge(z0, z1) [0]
   minus(z0, 0) -> z0 [0]
   minus(0, z0) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   div(z0, z1) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1) [0]
   if(false, z0, z1, z2) -> div_by_zero [0]
   if(true, false, z0, z1) -> 0 [0]
   if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1)) [0]

The TRS has the following type information:
GE :: 0:s:div_by_zero -> 0:s:div_by_zero -> c:c1:c2
0 :: 0:s:div_by_zero
c :: c:c1:c2
s :: 0:s:div_by_zero -> 0:s:div_by_zero
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0:s:div_by_zero -> 0:s:div_by_zero -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ID_INC :: 0:s:div_by_zero -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0:s:div_by_zero -> 0:s:div_by_zero -> c8:c9
c8 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
IF :: false:true -> false:true -> 0:s:div_by_zero -> 0:s:div_by_zero -> c10:c11:c12
ge :: 0:s:div_by_zero -> 0:s:div_by_zero -> false:true
c9 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
false :: false:true
c10 :: c10:c11:c12
true :: false:true
c11 :: c10:c11:c12
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5 -> c10:c11:c12
div :: 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero
minus :: 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero
id_inc :: 0:s:div_by_zero -> 0:s:div_by_zero
if :: false:true -> false:true -> 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero
div_by_zero :: 0:s:div_by_zero

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:

   ge(v0, v1) -> null_ge [0]
   minus(v0, v1) -> null_minus [0]
   id_inc(v0) -> null_id_inc [0]
   div(v0, v1) -> null_div [0]
   if(v0, v1, v2, v3) -> null_if [0]
   GE(v0, v1) -> null_GE [0]
   MINUS(v0, v1) -> null_MINUS [0]
   IF(v0, v1, v2, v3) -> null_IF [0]

And the following fresh constants:    null_ge, null_minus, null_id_inc, null_div, null_if, null_GE, null_MINUS, null_IF, const

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

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

   GE(z0, 0) -> c [1]
   GE(0, s(z0)) -> c1 [1]
   GE(s(z0), s(z1)) -> c2(GE(z0, z1)) [1]
   MINUS(z0, 0) -> c3 [1]
   MINUS(0, z0) -> c4 [1]
   MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) [1]
   ID_INC(z0) -> c6 [1]
   ID_INC(z0) -> c7 [1]
   DIV(z0, z1) -> c8(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z1, s(0))) [1]
   DIV(z0, z1) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1), GE(z0, z1)) [1]
   IF(false, z0, z1, z2) -> c10 [1]
   IF(true, false, z0, z1) -> c11 [1]
   IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1)) [1]
   ge(z0, 0) -> true [0]
   ge(0, s(z0)) -> false [0]
   ge(s(z0), s(z1)) -> ge(z0, z1) [0]
   minus(z0, 0) -> z0 [0]
   minus(0, z0) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   id_inc(z0) -> z0 [0]
   id_inc(z0) -> s(z0) [0]
   div(z0, z1) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1) [0]
   if(false, z0, z1, z2) -> div_by_zero [0]
   if(true, false, z0, z1) -> 0 [0]
   if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1)) [0]
   ge(v0, v1) -> null_ge [0]
   minus(v0, v1) -> null_minus [0]
   id_inc(v0) -> null_id_inc [0]
   div(v0, v1) -> null_div [0]
   if(v0, v1, v2, v3) -> null_if [0]
   GE(v0, v1) -> null_GE [0]
   MINUS(v0, v1) -> null_MINUS [0]
   IF(v0, v1, v2, v3) -> null_IF [0]

The TRS has the following type information:
GE :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> c:c1:c2:null_GE
0 :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
c :: c:c1:c2:null_GE
s :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
c1 :: c:c1:c2:null_GE
c2 :: c:c1:c2:null_GE -> c:c1:c2:null_GE
MINUS :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> c3:c4:c5:null_MINUS
c3 :: c3:c4:c5:null_MINUS
c4 :: c3:c4:c5:null_MINUS
c5 :: c3:c4:c5:null_MINUS -> c3:c4:c5:null_MINUS
ID_INC :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> c8:c9
c8 :: c10:c11:c12:null_IF -> c:c1:c2:null_GE -> c8:c9
IF :: false:true:null_ge -> false:true:null_ge -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> c10:c11:c12:null_IF
ge :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> false:true:null_ge
c9 :: c10:c11:c12:null_IF -> c:c1:c2:null_GE -> c8:c9
false :: false:true:null_ge
c10 :: c10:c11:c12:null_IF
true :: false:true:null_ge
c11 :: c10:c11:c12:null_IF
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5:null_MINUS -> c10:c11:c12:null_IF
div :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
minus :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
id_inc :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
if :: false:true:null_ge -> false:true:null_ge -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
div_by_zero :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
null_ge :: false:true:null_ge
null_minus :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
null_id_inc :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
null_div :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
null_if :: 0:s:div_by_zero:null_minus:null_id_inc:null_div:null_if
null_GE :: c:c1:c2:null_GE
null_MINUS :: c3:c4:c5:null_MINUS
null_IF :: c10:c11:c12:null_IF
const :: c8:c9

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 => 0
   c1 => 1
   c3 => 0
   c4 => 1
   c6 => 0
   c7 => 1
   false => 1
   c10 => 0
   true => 2
   c11 => 1
   div_by_zero => 1
   null_ge => 0
   null_minus => 0
   null_id_inc => 0
   null_div => 0
   null_if => 0
   null_GE => 0
   null_MINUS => 0
   null_IF => 0
   const => 0

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

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

   DIV(z, z') -{ 1 }-> 1 + IF(ge(z1, 1 + 0), ge(z0, z1), z0, z1) + GE(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   DIV(z, z') -{ 1 }-> 1 + IF(ge(z1, 1 + 0), ge(z0, z1), z0, z1) + GE(z1, 1 + 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   GE(z, z') -{ 1 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0
   GE(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   GE(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   GE(z, z') -{ 1 }-> 1 + GE(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   ID_INC(z) -{ 1 }-> 1 :|: z = z0, z0 >= 0
   ID_INC(z) -{ 1 }-> 0 :|: z = z0, z0 >= 0
   IF(z, z', z'', z3) -{ 1 }-> 1 :|: z = 2, z1 >= 0, z'' = z0, z3 = z1, z0 >= 0, z' = 1
   IF(z, z', z'', z3) -{ 1 }-> 0 :|: z1 >= 0, z = 1, z0 >= 0, z3 = z2, z' = z0, z2 >= 0, z'' = z1
   IF(z, z', z'', z3) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z3 = v3, v2 >= 0, v3 >= 0
   IF(z, z', z'', z3) -{ 1 }-> 1 + ID_INC(div(minus(z0, z1), z1)) + DIV(minus(z0, z1), z1) + MINUS(z0, z1) :|: z = 2, z1 >= 0, z' = 2, z'' = z0, z3 = z1, z0 >= 0
   MINUS(z, z') -{ 1 }-> 1 :|: z0 >= 0, z = 0, z' = z0
   MINUS(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   MINUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   div(z, z') -{ 0 }-> if(ge(z1, 1 + 0), ge(z0, z1), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   div(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   ge(z, z') -{ 0 }-> ge(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   ge(z, z') -{ 0 }-> 2 :|: z = z0, z0 >= 0, z' = 0
   ge(z, z') -{ 0 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0
   ge(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   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'', z3) -{ 0 }-> id_inc(div(minus(z0, z1), z1)) :|: z = 2, z1 >= 0, z' = 2, z'' = z0, z3 = z1, z0 >= 0
   if(z, z', z'', z3) -{ 0 }-> 1 :|: z1 >= 0, z = 1, z0 >= 0, z3 = z2, z' = z0, z2 >= 0, z'' = z1
   if(z, z', z'', z3) -{ 0 }-> 0 :|: z = 2, z1 >= 0, z'' = z0, z3 = z1, z0 >= 0, z' = 1
   if(z, z', z'', z3) -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z3 = v3, v2 >= 0, v3 >= 0
   minus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

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(V1, V, V17, V20),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V17, V20),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V17, V20),0,[fun2(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V17, V20),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V17, V20),0,[fun4(V1, V, V17, V20, Out)],[V1 >= 0,V >= 0,V17 >= 0,V20 >= 0]).
eq(start(V1, V, V17, V20),0,[ge(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V17, V20),0,[minus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V17, V20),0,[fun5(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V17, V20),0,[div(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V17, V20),0,[if(V1, V, V17, V20, Out)],[V1 >= 0,V >= 0,V17 >= 0,V20 >= 0]).
eq(fun(V1, V, Out),1,[],[Out = 0,V1 = V2,V2 >= 0,V = 0]).
eq(fun(V1, V, Out),1,[],[Out = 1,V3 >= 0,V = 1 + V3,V1 = 0]).
eq(fun(V1, V, Out),1,[fun(V5, V4, Ret1)],[Out = 1 + Ret1,V4 >= 0,V1 = 1 + V5,V5 >= 0,V = 1 + V4]).
eq(fun1(V1, V, Out),1,[],[Out = 0,V1 = V6,V6 >= 0,V = 0]).
eq(fun1(V1, V, Out),1,[],[Out = 1,V7 >= 0,V1 = 0,V = V7]).
eq(fun1(V1, V, Out),1,[fun1(V8, V9, Ret11)],[Out = 1 + Ret11,V9 >= 0,V1 = 1 + V8,V8 >= 0,V = 1 + V9]).
eq(fun2(V1, Out),1,[],[Out = 0,V1 = V10,V10 >= 0]).
eq(fun2(V1, Out),1,[],[Out = 1,V1 = V11,V11 >= 0]).
eq(fun3(V1, V, Out),1,[ge(V12, 1 + 0, Ret010),ge(V13, V12, Ret011),fun4(Ret010, Ret011, V13, V12, Ret01),fun(V12, 1 + 0, Ret12)],[Out = 1 + Ret01 + Ret12,V1 = V13,V12 >= 0,V = V12,V13 >= 0]).
eq(fun3(V1, V, Out),1,[ge(V15, 1 + 0, Ret0101),ge(V14, V15, Ret0111),fun4(Ret0101, Ret0111, V14, V15, Ret012),fun(V14, V15, Ret13)],[Out = 1 + Ret012 + Ret13,V1 = V14,V15 >= 0,V = V15,V14 >= 0]).
eq(fun4(V1, V, V17, V20, Out),1,[],[Out = 0,V16 >= 0,V1 = 1,V18 >= 0,V20 = V19,V = V18,V19 >= 0,V17 = V16]).
eq(fun4(V1, V, V17, V20, Out),1,[],[Out = 1,V1 = 2,V21 >= 0,V17 = V22,V20 = V21,V22 >= 0,V = 1]).
eq(fun4(V1, V, V17, V20, Out),1,[minus(V24, V23, Ret00100),div(Ret00100, V23, Ret0010),fun2(Ret0010, Ret001),minus(V24, V23, Ret0102),fun3(Ret0102, V23, Ret013),fun1(V24, V23, Ret14)],[Out = 1 + Ret001 + Ret013 + Ret14,V1 = 2,V23 >= 0,V = 2,V17 = V24,V20 = V23,V24 >= 0]).
eq(ge(V1, V, Out),0,[],[Out = 2,V1 = V25,V25 >= 0,V = 0]).
eq(ge(V1, V, Out),0,[],[Out = 1,V26 >= 0,V = 1 + V26,V1 = 0]).
eq(ge(V1, V, Out),0,[ge(V28, V27, Ret)],[Out = Ret,V27 >= 0,V1 = 1 + V28,V28 >= 0,V = 1 + V27]).
eq(minus(V1, V, Out),0,[],[Out = V29,V1 = V29,V29 >= 0,V = 0]).
eq(minus(V1, V, Out),0,[],[Out = 0,V30 >= 0,V1 = 0,V = V30]).
eq(minus(V1, V, Out),0,[minus(V32, V31, Ret2)],[Out = Ret2,V31 >= 0,V1 = 1 + V32,V32 >= 0,V = 1 + V31]).
eq(fun5(V1, Out),0,[],[Out = V33,V1 = V33,V33 >= 0]).
eq(fun5(V1, Out),0,[],[Out = 1 + V34,V1 = V34,V34 >= 0]).
eq(div(V1, V, Out),0,[ge(V35, 1 + 0, Ret0),ge(V36, V35, Ret15),if(Ret0, Ret15, V36, V35, Ret3)],[Out = Ret3,V1 = V36,V35 >= 0,V = V35,V36 >= 0]).
eq(if(V1, V, V17, V20, Out),0,[],[Out = 1,V38 >= 0,V1 = 1,V39 >= 0,V20 = V37,V = V39,V37 >= 0,V17 = V38]).
eq(if(V1, V, V17, V20, Out),0,[],[Out = 0,V1 = 2,V40 >= 0,V17 = V41,V20 = V40,V41 >= 0,V = 1]).
eq(if(V1, V, V17, V20, Out),0,[minus(V42, V43, Ret00),div(Ret00, V43, Ret02),fun5(Ret02, Ret4)],[Out = Ret4,V1 = 2,V43 >= 0,V = 2,V17 = V42,V20 = V43,V42 >= 0]).
eq(ge(V1, V, Out),0,[],[Out = 0,V45 >= 0,V44 >= 0,V1 = V45,V = V44]).
eq(minus(V1, V, Out),0,[],[Out = 0,V47 >= 0,V46 >= 0,V1 = V47,V = V46]).
eq(fun5(V1, Out),0,[],[Out = 0,V48 >= 0,V1 = V48]).
eq(div(V1, V, Out),0,[],[Out = 0,V49 >= 0,V50 >= 0,V1 = V49,V = V50]).
eq(if(V1, V, V17, V20, Out),0,[],[Out = 0,V51 >= 0,V17 = V54,V52 >= 0,V1 = V51,V = V52,V20 = V53,V54 >= 0,V53 >= 0]).
eq(fun(V1, V, Out),0,[],[Out = 0,V56 >= 0,V55 >= 0,V1 = V56,V = V55]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V58 >= 0,V57 >= 0,V1 = V58,V = V57]).
eq(fun4(V1, V, V17, V20, Out),0,[],[Out = 0,V59 >= 0,V17 = V61,V60 >= 0,V1 = V59,V = V60,V20 = V62,V61 >= 0,V62 >= 0]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,Out),[V1],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun4(V1,V,V17,V20,Out),[V1,V,V17,V20],[Out]).
input_output_vars(ge(V1,V,Out),[V1,V],[Out]).
input_output_vars(minus(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun5(V1,Out),[V1],[Out]).
input_output_vars(div(V1,V,Out),[V1,V],[Out]).
input_output_vars(if(V1,V,V17,V20,Out),[V1,V,V17,V20],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [ge/3]
1. non_recursive  : [fun5/2]
2. recursive  : [minus/3]
3. recursive [non_tail] : [(div)/3,if/5]
4. recursive  : [fun/3]
5. recursive  : [fun1/3]
6. non_recursive  : [fun2/2]
7. recursive [non_tail] : [fun3/3,fun4/5]
8. non_recursive  : [start/4]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into ge/3
1. SCC is partially evaluated into fun5/2
2. SCC is partially evaluated into minus/3
3. SCC is partially evaluated into (div)/3
4. SCC is partially evaluated into fun/3
5. SCC is partially evaluated into fun1/3
6. SCC is partially evaluated into fun2/2
7. SCC is partially evaluated into fun3/3
8. SCC is partially evaluated into start/4

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

### Specialization of cost equations ge/3 
* CE 45 is refined into CE [46] 
* CE 42 is refined into CE [47] 
* CE 43 is refined into CE [48] 
* CE 44 is refined into CE [49] 


### Cost equations --> "Loop" of ge/3 
* CEs [49] --> Loop 27 
* CEs [46] --> Loop 28 
* CEs [47] --> Loop 29 
* CEs [48] --> Loop 30 

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

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


### Specialization of cost equations fun5/2 
* CE 35 is refined into CE [50] 
* CE 36 is refined into CE [51] 
* CE 37 is refined into CE [52] 


### Cost equations --> "Loop" of fun5/2 
* CEs [50] --> Loop 31 
* CEs [51] --> Loop 32 
* CEs [52] --> Loop 33 

### Ranking functions of CR fun5(V1,Out) 

#### Partial ranking functions of CR fun5(V1,Out) 


### Specialization of cost equations minus/3 
* CE 15 is refined into CE [53] 
* CE 14 is refined into CE [54] 
* CE 16 is refined into CE [55] 


### Cost equations --> "Loop" of minus/3 
* CEs [55] --> Loop 34 
* CEs [53] --> Loop 35 
* CEs [54] --> Loop 36 

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

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


### Specialization of cost equations (div)/3 
* CE 19 is refined into CE [56,57] 
* CE 17 is refined into CE [58,59,60,61,62,63,64,65,66,67,68] 
* CE 20 is refined into CE [69] 
* CE 18 is refined into CE [70,71,72,73,74,75] 


### Cost equations --> "Loop" of (div)/3 
* CEs [75] --> Loop 37 
* CEs [74] --> Loop 38 
* CEs [72] --> Loop 39 
* CEs [71] --> Loop 40 
* CEs [73] --> Loop 41 
* CEs [70] --> Loop 42 
* CEs [56,57] --> Loop 43 
* CEs [58,59,61] --> Loop 44 
* CEs [60,62,63,64,65,66,67,68,69] --> Loop 45 

### Ranking functions of CR div(V1,V,Out) 
* RF of phase [37,38,41]: [V1,V1-V+1]

#### Partial ranking functions of CR div(V1,V,Out) 
* Partial RF of phase [37,38,41]:
  - RF of loop [37:1,38:1,41:1]:
    V1
    V1-V+1


### Specialization of cost equations fun/3 
* CE 38 is refined into CE [76] 
* CE 41 is refined into CE [77] 
* CE 39 is refined into CE [78] 
* CE 40 is refined into CE [79] 


### Cost equations --> "Loop" of fun/3 
* CEs [79] --> Loop 46 
* CEs [76,77] --> Loop 47 
* CEs [78] --> Loop 48 

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

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


### Specialization of cost equations fun1/3 
* CE 31 is refined into CE [80] 
* CE 34 is refined into CE [81] 
* CE 32 is refined into CE [82] 
* CE 33 is refined into CE [83] 


### Cost equations --> "Loop" of fun1/3 
* CEs [83] --> Loop 49 
* CEs [80,81] --> Loop 50 
* CEs [82] --> Loop 51 

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

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


### Specialization of cost equations fun2/2 
* CE 22 is refined into CE [84] 
* CE 21 is refined into CE [85] 


### Cost equations --> "Loop" of fun2/2 
* CEs [84] --> Loop 52 
* CEs [85] --> Loop 53 

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

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


### Specialization of cost equations fun3/3 
* CE 23 is refined into CE [86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110] 
* CE 24 is refined into CE [111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133] 
* CE 27 is refined into CE [134,135,136,137,138] 
* CE 28 is refined into CE [139,140,141,142] 
* CE 29 is refined into CE [143,144] 
* CE 30 is refined into CE [145,146,147,148] 
* CE 25 is refined into CE [149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228] 
* CE 26 is refined into CE [229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308] 


### Cost equations --> "Loop" of fun3/3 
* CEs [252,276,292] --> Loop 54 
* CEs [210,211,284,291] --> Loop 55 
* CEs [172,196,212,228,308] --> Loop 56 
* CEs [204,220,226,227,300,307] --> Loop 57 
* CEs [202,203,218,219,283,299] --> Loop 58 
* CEs [160,168,171,184,192,195,240,248,251,264,272,275,290,306] --> Loop 59 
* CEs [156,159,167,180,183,191,209,225,236,239,247,260,263,271,282,289,298,305] --> Loop 60 
* CEs [155,179,201,217,235,259,281,297] --> Loop 61 
* CEs [246,270,288] --> Loop 62 
* CEs [206,207,280,287] --> Loop 63 
* CEs [208,224,304] --> Loop 64 
* CEs [200,216,222,223,296,303] --> Loop 65 
* CEs [198,199,214,215,279,295] --> Loop 66 
* CEs [242,266,286,302] --> Loop 67 
* CEs [150,153,161,174,177,185,205,221,230,233,241,254,257,265,278,285,294,301] --> Loop 68 
* CEs [149,173,197,213,229,253,277,293] --> Loop 69 
* CEs [151,154,157,162,165,175,178,181,186,189,231,234,237,245,255,258,261,269] --> Loop 70 
* CEs [152,158,163,166,169,176,182,187,190,193,232,238,243,249,256,262,267,273] --> Loop 71 
* CEs [164,170,188,194,244,250,268,274] --> Loop 72 
* CEs [99,110] --> Loop 73 
* CEs [94,97,105,108] --> Loop 74 
* CEs [93,96,104,107] --> Loop 75 
* CEs [137] --> Loop 76 
* CEs [138,142] --> Loop 77 
* CEs [111,113,117,119,145,147] --> Loop 78 
* CEs [86,87,90,112,114,118,143,144,146,148] --> Loop 79 
* CEs [134,140] --> Loop 80 
* CEs [88,91,100,102,116,121,123,125,127,129,131,133,135,136,139,141] --> Loop 81 
* CEs [89,92,95,98,101,103,106,109,115,120,122,124,126,128,130,132] --> Loop 82 

### Ranking functions of CR fun3(V1,V,Out) 
* RF of phase [54,55,56,57,58,59,60,61]: [V1,V1-V+1]

#### Partial ranking functions of CR fun3(V1,V,Out) 
* Partial RF of phase [54,55,56,57,58,59,60,61]:
  - RF of loop [54:1,56:1,59:1,60:1,61:1]:
    V1
    V1-V+1
  - RF of loop [55:1,57:1,58:1]:
    V1-1
    V1-2*V+1


### Specialization of cost equations start/4 
* CE 2 is refined into CE [309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569,570,571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589,590,591,592,593,594,595,596,597,598,599,600,601,602,603,604,605,606,607,608,609,610,611,612,613,614,615,616,617,618,619,620,621,622,623,624,625,626,627,628,629,630,631,632,633,634,635,636,637,638,639,640,641,642,643,644,645,646,647,648,649,650] 
* CE 5 is refined into CE [651,652,653,654,655,656,657,658,659,660,661,662,663,664,665,666,667,668,669,670,671] 
* CE 3 is refined into CE [672] 
* CE 1 is refined into CE [673] 
* CE 4 is refined into CE [674] 
* CE 6 is refined into CE [675,676,677,678] 
* CE 7 is refined into CE [679,680,681,682] 
* CE 8 is refined into CE [683,684] 
* CE 9 is refined into CE [685,686,687,688,689,690,691,692,693,694,695,696,697,698,699,700] 
* CE 10 is refined into CE [701,702,703,704,705] 
* CE 11 is refined into CE [706,707,708] 
* CE 12 is refined into CE [709,710,711] 
* CE 13 is refined into CE [712,713,714,715] 


### Cost equations --> "Loop" of start/4 
* CEs [687,702,706,713] --> Loop 83 
* CEs [359,360,361,363,366,410,411,412,414,417,460,463,466,468,469,470,472,475,502,505,508,510,511,512,514,517] --> Loop 84 
* CEs [378,379,380,381,382,383,429,430,431,432,433,434,487,488,489,490,491,492,529,530,531,532,533,534,563,564,565,566,567,568,593,594,595,596,597,598] --> Loop 85 
* CEs [310,312,314,316,318,320,322,324,326,328,330,332,334,336,338,340,342,344,354,393,395,405,444,446,448,450,452,454,456,458,651,652,653,654,655,656,660,661,662] --> Loop 86 
* CEs [309,311,313,315,317,319,321,323,325,327,329,331,333,335,337,339,341,343,345,346,347,348,349,350,351,352,353,355,356,357,358,362,364,365,367,368,369,370,371,372,373,374,375,376,377,384,385,386,387,388,389,390,391,392,394,396,397,398,399,400,401,402,403,404,406,407,408,409,413,415,416,418,419,420,421,422,423,424,425,426,427,428,435,436,437,438,439,440,441,442,443,445,447,449,451,453,455,457,459,461,462,464,465,467,471,473,474,476,477,478,479,480,481,482,483,484,485,486,493,494,495,496,497,498,499,500,501,503,504,506,507,509,513,515,516,518,519,520,521,522,523,524,525,526,527,528,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,569,570,571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589,590,591,592,599,600,601,602,603,604,605,606,607,608,609,610,611,612,613,614,615,616,617,618,619,620,621,622,623,624,625,626,627,628,629,630,631,632,633,634,635,636,637,638,639,640,641,642,643,644,645,646,647,648,649,650,657,658,659,663,664,665,666,667,668,669,670,671,694,695,696] --> Loop 87 
* CEs [672] --> Loop 88 
* CEs [674] --> Loop 89 
* CEs [673,675,676,677,678,679,680,681,682,683,684,685,686,688,689,690,691,692,693,697,698,699,700,701,703,704,705,707,708,709,710,711,712,714,715] --> Loop 90 

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

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


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

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

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

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

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

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

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


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

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

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


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

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

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

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


#### Cost of chains of div(V1,V,Out):
* Chain [[37,38,41],45]: 0
  with precondition: [V>=1,Out>=0,V1>=V,V1+1>=Out+V] 

* Chain [[37,38,41],42,45]: 0
  with precondition: [V>=1,Out>=0,V1>=2*V,V1+1>=2*V+Out] 

* Chain [[37,38,41],40,45]: 0
  with precondition: [V>=1,Out>=0,V1>=2*V,V1+2>=2*V+Out] 

* Chain [[37,38,41],39,45]: 0
  with precondition: [V>=1,Out>=0,V1>=2*V,V1+1>=2*V+Out] 

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

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

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

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

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

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


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

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

* Chain [[46],47]: 1*it(46)+1
  Such that:it(46) =< Out

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

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

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


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

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

* Chain [[49],50]: 1*it(49)+1
  Such that:it(49) =< Out

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

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

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


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

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


#### Cost of chains of fun3(V1,V,Out):
* Chain [[54,55,56,57,58,59,60,61],82]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+2
  Such that:aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(36) =< V1
aux(23) =< aux(36)
aux(24) =< aux(36)
it(54) =< aux(36)
it(55) =< aux(36)
it(57) =< aux(36)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
s(94) =< aux(36)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< aux(36)
s(92) =< s(94)

  with precondition: [V>=1,Out>=3,V1>=V,5*V1+4>=3*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],81]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+11
  Such that:aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(38) =< V1
aux(23) =< aux(38)
aux(24) =< aux(38)
it(54) =< aux(38)
it(55) =< aux(38)
it(57) =< aux(38)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
s(94) =< aux(38)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< aux(38)
s(92) =< s(94)

  with precondition: [V>=1,Out>=4,V1>=V,5*V1+5>=3*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],80]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+4
  Such that:aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(39) =< V1
aux(23) =< aux(39)
aux(24) =< aux(39)
it(54) =< aux(39)
it(55) =< aux(39)
it(57) =< aux(39)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
s(94) =< aux(39)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< aux(39)
s(92) =< s(94)

  with precondition: [V>=1,Out>=5,V1>=V,5*V1+6>=3*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],77]: 25*it(54)+5*it(55)+10*it(57)+31*s(88)+14*s(89)+18*s(92)+2*s(93)+1*s(121)+3
  Such that:s(121) =< 1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(40) =< V1
s(88) =< aux(40)
aux(23) =< aux(40)
aux(24) =< aux(40)
it(54) =< aux(40)
it(55) =< aux(40)
it(57) =< aux(40)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
s(94) =< aux(40)
s(93) =< aux(24)
s(89) =< aux(23)
s(92) =< s(94)

  with precondition: [V>=2,Out>=5,V1>=V+1,7*V1+5>=3*V+2*Out] 

* Chain [[54,55,56,57,58,59,60,61],76]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+1*s(122)+3
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(41) =< V1+1
s(122) =< aux(41)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(41)
it(55) =< aux(41)
it(54) =< aux(41)
it(57) =< aux(41)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(41)
s(94) =< aux(41)
s(90) =< aux(41)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

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

* Chain [[54,55,56,57,58,59,60,61],75]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+4*s(123)+2
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(43) =< V1+1
s(123) =< aux(43)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(43)
it(55) =< aux(43)
it(54) =< aux(43)
it(57) =< aux(43)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(43)
s(94) =< aux(43)
s(90) =< aux(43)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=2,Out>=5,V1>=V+1,7*V1+5>=3*V+2*Out] 

* Chain [[54,55,56,57,58,59,60,61],74]: 25*it(54)+5*it(55)+10*it(57)+32*s(88)+14*s(89)+18*s(92)+2*s(93)+2*s(127)+2
  Such that:aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(45) =< V
aux(46) =< V1
s(88) =< aux(46)
s(127) =< aux(45)
aux(23) =< aux(46)
aux(24) =< aux(46)
it(54) =< aux(46)
it(55) =< aux(46)
it(57) =< aux(46)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
s(94) =< aux(46)
s(93) =< aux(24)
s(89) =< aux(23)
s(92) =< s(94)

  with precondition: [V>=1,Out>=4,V1>=V+1,5*V1>=3*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],73]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+2*s(131)+2
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(47) =< V
aux(48) =< V1-V
s(131) =< aux(47)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(48)
it(55) =< aux(48)
it(54) =< aux(48)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(48)
s(90) =< aux(48)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(48)

  with precondition: [V>=1,Out>=4,V1>=2*V,5*V1+4>=7*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],72,82]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(133)+4*s(134)+4*s(142)+7
  Such that:aux(49) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(50) =< V
aux(51) =< V+1
aux(52) =< V1-V
s(142) =< aux(49)
s(134) =< aux(50)
s(133) =< aux(51)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(52)
it(55) =< aux(52)
it(54) =< aux(52)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(52)
s(90) =< aux(52)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(52)

  with precondition: [V>=1,V1>=2*V,Out>=V+8,5*V1+8>=6*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],72,81]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(133)+4*s(134)+4*s(142)+16
  Such that:aux(49) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(50) =< V
aux(51) =< V+1
aux(53) =< V1-V
s(142) =< aux(49)
s(134) =< aux(50)
s(133) =< aux(51)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(53)
it(55) =< aux(53)
it(54) =< aux(53)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(53)
s(90) =< aux(53)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(53)

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

* Chain [[54,55,56,57,58,59,60,61],72,80]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(133)+4*s(134)+4*s(142)+9
  Such that:aux(49) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(50) =< V
aux(51) =< V+1
aux(54) =< V1-V
s(142) =< aux(49)
s(134) =< aux(50)
s(133) =< aux(51)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(54)
it(55) =< aux(54)
it(54) =< aux(54)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(54)
s(90) =< aux(54)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(54)

  with precondition: [V>=1,V1>=2*V,Out>=V+10,5*V1+10>=6*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],71,82]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+16*s(149)+8*s(150)+4*s(166)+7
  Such that:aux(57) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(58) =< V
aux(59) =< V+1
aux(60) =< V1-V
s(166) =< aux(57)
s(150) =< aux(58)
s(149) =< aux(59)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(60)
it(55) =< aux(60)
it(54) =< aux(60)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(60)
s(90) =< aux(60)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(60)

  with precondition: [V>=1,Out>=8,V1>=2*V,5*V1+7>=6*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],71,81]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+16*s(149)+8*s(150)+4*s(166)+16
  Such that:aux(57) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(58) =< V
aux(59) =< V+1
aux(61) =< V1-V
s(166) =< aux(57)
s(150) =< aux(58)
s(149) =< aux(59)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(61)
it(55) =< aux(61)
it(54) =< aux(61)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(61)
s(90) =< aux(61)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(61)

  with precondition: [V>=1,Out>=9,V1>=2*V,5*V1+8>=6*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],71,80]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+16*s(149)+8*s(150)+4*s(166)+9
  Such that:aux(57) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(58) =< V
aux(59) =< V+1
aux(62) =< V1-V
s(166) =< aux(57)
s(150) =< aux(58)
s(149) =< aux(59)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(62)
it(55) =< aux(62)
it(54) =< aux(62)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(62)
s(90) =< aux(62)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(62)

  with precondition: [V>=1,Out>=10,V1>=2*V,5*V1+9>=6*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],70,82]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(177)+12*s(178)+2*s(191)+7
  Such that:aux(65) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(66) =< V
aux(67) =< V+1
aux(68) =< V1-V
s(191) =< aux(65)
s(178) =< aux(66)
s(177) =< aux(67)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(68)
it(55) =< aux(68)
it(54) =< aux(68)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(68)
s(90) =< aux(68)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(68)

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

* Chain [[54,55,56,57,58,59,60,61],70,81]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(177)+12*s(178)+2*s(191)+16
  Such that:aux(65) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(66) =< V
aux(67) =< V+1
aux(69) =< V1-V
s(191) =< aux(65)
s(178) =< aux(66)
s(177) =< aux(67)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(69)
it(55) =< aux(69)
it(54) =< aux(69)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(69)
s(90) =< aux(69)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(69)

  with precondition: [V>=1,Out>=8,V1>=2*V,5*V1+7>=6*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],70,80]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(177)+12*s(178)+2*s(191)+9
  Such that:aux(65) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(66) =< V
aux(67) =< V+1
aux(70) =< V1-V
s(191) =< aux(65)
s(178) =< aux(66)
s(177) =< aux(67)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(70)
it(55) =< aux(70)
it(54) =< aux(70)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(70)
s(90) =< aux(70)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(70)

  with precondition: [V>=1,Out>=9,V1>=2*V,5*V1+8>=6*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],69,82]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+7
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(71) =< V1-V
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(71)
it(55) =< aux(71)
it(54) =< aux(71)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(71)
s(90) =< aux(71)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(71)

  with precondition: [V>=1,Out>=5,V1>=2*V,5*V1+6>=8*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],69,81]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+16
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(72) =< V1-V
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(72)
it(55) =< aux(72)
it(54) =< aux(72)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(72)
s(90) =< aux(72)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(72)

  with precondition: [V>=1,Out>=6,V1>=2*V,5*V1+7>=8*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],69,80]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+9
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(73) =< V1-V
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(73)
it(55) =< aux(73)
it(54) =< aux(73)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(73)
s(90) =< aux(73)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(73)

  with precondition: [V>=1,Out>=7,V1>=2*V,5*V1+8>=8*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],68,82]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+6*s(199)+4*s(203)+7
  Such that:aux(74) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(75) =< V
aux(76) =< V1-V
s(203) =< aux(74)
s(199) =< aux(75)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(76)
it(55) =< aux(76)
it(54) =< aux(76)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(76)
s(90) =< aux(76)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(76)

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

* Chain [[54,55,56,57,58,59,60,61],68,81]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+6*s(199)+4*s(203)+16
  Such that:aux(74) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(75) =< V
aux(77) =< V1-V
s(203) =< aux(74)
s(199) =< aux(75)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(77)
it(55) =< aux(77)
it(54) =< aux(77)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(77)
s(90) =< aux(77)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(77)

  with precondition: [V>=1,Out>=7,V1>=2*V,5*V1+7>=7*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],68,80]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+6*s(199)+4*s(203)+9
  Such that:aux(74) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(75) =< V
aux(78) =< V1-V
s(203) =< aux(74)
s(199) =< aux(75)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(78)
it(55) =< aux(78)
it(54) =< aux(78)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(78)
s(90) =< aux(78)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(78)

  with precondition: [V>=1,Out>=8,V1>=2*V,5*V1+8>=7*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],67,82]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+11
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(80) =< V1-V
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(80)
it(55) =< aux(80)
it(54) =< aux(80)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(80)
s(90) =< aux(80)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(80)

  with precondition: [V>=1,Out>=7,V1>=2*V,5*V1+8>=8*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],67,81]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+20
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(81) =< V1-V
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(81)
it(55) =< aux(81)
it(54) =< aux(81)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(81)
s(90) =< aux(81)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(81)

  with precondition: [V>=1,Out>=8,V1>=2*V,5*V1+9>=8*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],67,80]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+13
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(82) =< V1-V
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(82)
it(55) =< aux(82)
it(54) =< aux(82)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(82)
s(90) =< aux(82)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(82)

  with precondition: [V>=1,Out>=9,V1>=2*V,5*V1+10>=8*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],66,82]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+6*s(213)+7
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(83) =< V
aux(84) =< V1-2*V
s(213) =< aux(83)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(84)
it(55) =< aux(84)
it(54) =< aux(84)
it(57) =< aux(84)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(84)
s(94) =< aux(84)
s(90) =< aux(84)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=6,V1>=3*V,5*V1+6>=12*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],66,81]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+6*s(213)+16
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(83) =< V
aux(85) =< V1-2*V
s(213) =< aux(83)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(85)
it(55) =< aux(85)
it(54) =< aux(85)
it(57) =< aux(85)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(85)
s(94) =< aux(85)
s(90) =< aux(85)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=7,V1>=3*V,5*V1+7>=12*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],66,80]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+6*s(213)+9
  Such that:aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(83) =< V
aux(86) =< V1-2*V
s(213) =< aux(83)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(86)
it(55) =< aux(86)
it(54) =< aux(86)
it(57) =< aux(86)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(86)
s(94) =< aux(86)
s(90) =< aux(86)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=8,V1>=3*V,5*V1+8>=12*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],65,82]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(219)+1*s(226)+7
  Such that:s(226) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(89) =< V
aux(90) =< V1-2*V
s(219) =< aux(89)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(90)
it(55) =< aux(90)
it(54) =< aux(90)
it(57) =< aux(90)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(90)
s(94) =< aux(90)
s(90) =< aux(90)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=7,V1>=3*V,5*V1+6>=11*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],65,81]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(219)+1*s(226)+16
  Such that:s(226) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(89) =< V
aux(91) =< V1-2*V
s(219) =< aux(89)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(91)
it(55) =< aux(91)
it(54) =< aux(91)
it(57) =< aux(91)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(91)
s(94) =< aux(91)
s(90) =< aux(91)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=8,V1>=3*V,5*V1+7>=11*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],65,80]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+8*s(219)+1*s(226)+9
  Such that:s(226) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(89) =< V
aux(92) =< V1-2*V
s(219) =< aux(89)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(92)
it(55) =< aux(92)
it(54) =< aux(92)
it(57) =< aux(92)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(92)
s(94) =< aux(92)
s(90) =< aux(92)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=9,V1>=3*V,5*V1+8>=11*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],64,82]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+5*s(228)+1*s(233)+7
  Such that:s(233) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(95) =< V
aux(96) =< V1-2*V
s(228) =< aux(95)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(96)
it(55) =< aux(96)
it(54) =< aux(96)
it(57) =< aux(96)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(96)
s(94) =< aux(96)
s(90) =< aux(96)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=8,V1>=3*V,5*V1+7>=11*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],64,81]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+5*s(228)+1*s(233)+16
  Such that:s(233) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(95) =< V
aux(97) =< V1-2*V
s(228) =< aux(95)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(97)
it(55) =< aux(97)
it(54) =< aux(97)
it(57) =< aux(97)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(97)
s(94) =< aux(97)
s(90) =< aux(97)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=9,V1>=3*V,5*V1+8>=11*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],64,80]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+5*s(228)+1*s(233)+9
  Such that:s(233) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(95) =< V
aux(98) =< V1-2*V
s(228) =< aux(95)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(98)
it(55) =< aux(98)
it(54) =< aux(98)
it(57) =< aux(98)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(98)
s(94) =< aux(98)
s(90) =< aux(98)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=10,V1>=3*V,5*V1+9>=11*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],63,82]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+4*s(234)+1*s(237)+7
  Such that:s(237) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(99) =< V
aux(100) =< V1-2*V
s(234) =< aux(99)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(100)
it(55) =< aux(100)
it(54) =< aux(100)
it(57) =< aux(100)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(100)
s(94) =< aux(100)
s(90) =< aux(100)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=7,V1>=3*V,5*V1+7>=12*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],63,81]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+4*s(234)+1*s(237)+16
  Such that:s(237) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(99) =< V
aux(101) =< V1-2*V
s(234) =< aux(99)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(101)
it(55) =< aux(101)
it(54) =< aux(101)
it(57) =< aux(101)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(101)
s(94) =< aux(101)
s(90) =< aux(101)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=8,V1>=3*V,5*V1+8>=12*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],63,80]: 25*it(54)+5*it(55)+10*it(57)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+4*s(234)+1*s(237)+9
  Such that:s(237) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(32) =< V1-V
aux(33) =< V1-V+1
aux(99) =< V
aux(102) =< V1-2*V
s(234) =< aux(99)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
it(57) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
it(57) =< aux(30)
aux(24) =< aux(102)
it(55) =< aux(102)
it(54) =< aux(102)
it(57) =< aux(102)
it(57) =< aux(32)
s(94) =< aux(32)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
it(57) =< aux(33)
aux(23) =< aux(102)
s(94) =< aux(102)
s(90) =< aux(102)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< s(94)

  with precondition: [V>=1,Out>=9,V1>=3*V,5*V1+9>=12*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],62,82]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+3*s(239)+3*s(240)+7
  Such that:aux(103) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(104) =< V
aux(105) =< V1-V
s(240) =< aux(103)
s(239) =< aux(104)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(105)
it(55) =< aux(105)
it(54) =< aux(105)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(105)
s(90) =< aux(105)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(105)

  with precondition: [V>=1,Out>=8,V1>=2*V,5*V1+8>=7*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],62,81]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+3*s(239)+3*s(240)+16
  Such that:aux(103) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(104) =< V
aux(106) =< V1-V
s(240) =< aux(103)
s(239) =< aux(104)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(106)
it(55) =< aux(106)
it(54) =< aux(106)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(106)
s(90) =< aux(106)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(106)

  with precondition: [V>=1,Out>=9,V1>=2*V,5*V1+9>=7*V+Out] 

* Chain [[54,55,56,57,58,59,60,61],62,80]: 25*it(54)+15*it(55)+30*s(88)+14*s(89)+18*s(92)+2*s(93)+3*s(239)+3*s(240)+9
  Such that:aux(103) =< 1
aux(29) =< V1
aux(30) =< V1-2*V+1
aux(33) =< V1-V+1
aux(104) =< V
aux(107) =< V1-V
s(240) =< aux(103)
s(239) =< aux(104)
aux(23) =< aux(29)
aux(24) =< aux(29)
it(54) =< aux(29)
it(55) =< aux(29)
s(90) =< aux(29)
aux(24) =< aux(30)
it(55) =< aux(30)
aux(24) =< aux(107)
it(55) =< aux(107)
it(54) =< aux(107)
aux(23) =< aux(33)
aux(24) =< aux(33)
it(54) =< aux(33)
it(55) =< aux(33)
aux(23) =< aux(107)
s(90) =< aux(107)
s(93) =< aux(24)
s(89) =< aux(23)
s(88) =< s(90)
s(92) =< aux(107)

  with precondition: [V>=1,Out>=10,V1>=2*V,5*V1+10>=7*V+Out] 

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

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

* Chain [80]: 4
  with precondition: [V1=0,Out=3,V>=1] 

* Chain [79]: 3
  with precondition: [V=0,Out=1,V1>=0] 

* Chain [78]: 3
  with precondition: [V=0,Out=2,V1>=0] 

* Chain [77]: 1*s(120)+1*s(121)+3
  Such that:s(121) =< 1
s(120) =< V1

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

* Chain [76]: 1*s(122)+3
  Such that:s(122) =< V1+1

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

* Chain [75]: 4*s(123)+2
  Such that:aux(42) =< V1+1
s(123) =< aux(42)

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

* Chain [74]: 2*s(127)+2*s(128)+2
  Such that:aux(44) =< V1
aux(45) =< V
s(128) =< aux(44)
s(127) =< aux(45)

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

* Chain [73]: 2*s(131)+2
  Such that:aux(47) =< V
s(131) =< aux(47)

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

* Chain [72,82]: 8*s(133)+4*s(134)+4*s(142)+7
  Such that:aux(49) =< 1
aux(50) =< V1
aux(51) =< V1+1
s(142) =< aux(49)
s(134) =< aux(50)
s(133) =< aux(51)

  with precondition: [V1=V,Out>=V1+6,2*V1+5>=Out] 

* Chain [72,81]: 8*s(133)+4*s(134)+4*s(142)+16
  Such that:aux(49) =< 1
aux(50) =< V1
aux(51) =< V1+1
s(142) =< aux(49)
s(134) =< aux(50)
s(133) =< aux(51)

  with precondition: [V1=V,Out>=V1+7,2*V1+6>=Out] 

* Chain [72,80]: 8*s(133)+4*s(134)+4*s(142)+9
  Such that:aux(49) =< 1
aux(50) =< V1
aux(51) =< V1+1
s(142) =< aux(49)
s(134) =< aux(50)
s(133) =< aux(51)

  with precondition: [V1=V,Out>=V1+8,2*V1+7>=Out] 

* Chain [71,82]: 16*s(149)+8*s(150)+4*s(166)+7
  Such that:aux(57) =< 1
aux(58) =< V
aux(59) =< V+1
s(166) =< aux(57)
s(150) =< aux(58)
s(149) =< aux(59)

  with precondition: [Out>=6,V1>=V,2*V+4>=Out] 

* Chain [71,81]: 16*s(149)+8*s(150)+4*s(166)+16
  Such that:aux(57) =< 1
aux(58) =< V
aux(59) =< V+1
s(166) =< aux(57)
s(150) =< aux(58)
s(149) =< aux(59)

  with precondition: [Out>=7,V1>=V,2*V+5>=Out] 

* Chain [71,80]: 16*s(149)+8*s(150)+4*s(166)+9
  Such that:aux(57) =< 1
aux(58) =< V
aux(59) =< V+1
s(166) =< aux(57)
s(150) =< aux(58)
s(149) =< aux(59)

  with precondition: [Out>=8,V1>=V,2*V+6>=Out] 

* Chain [70,82]: 8*s(177)+12*s(178)+2*s(191)+7
  Such that:aux(65) =< 1
aux(66) =< V
aux(67) =< V+1
s(191) =< aux(65)
s(178) =< aux(66)
s(177) =< aux(67)

  with precondition: [Out>=5,V1>=V,2*V+3>=Out] 

* Chain [70,81]: 8*s(177)+12*s(178)+2*s(191)+16
  Such that:aux(65) =< 1
aux(66) =< V
aux(67) =< V+1
s(191) =< aux(65)
s(178) =< aux(66)
s(177) =< aux(67)

  with precondition: [Out>=6,V1>=V,2*V+4>=Out] 

* Chain [70,80]: 8*s(177)+12*s(178)+2*s(191)+9
  Such that:aux(65) =< 1
aux(66) =< V
aux(67) =< V+1
s(191) =< aux(65)
s(178) =< aux(66)
s(177) =< aux(67)

  with precondition: [Out>=7,V1>=V,2*V+5>=Out] 

* Chain [69,82]: 7
  with precondition: [Out=3,V>=1,V1>=V] 

* Chain [69,81]: 16
  with precondition: [Out=4,V>=1,V1>=V] 

* Chain [69,80]: 9
  with precondition: [Out=5,V>=1,V1>=V] 

* Chain [68,82]: 6*s(199)+4*s(203)+7
  Such that:aux(74) =< 1
aux(75) =< V
s(203) =< aux(74)
s(199) =< aux(75)

  with precondition: [Out>=4,V1>=V,V+3>=Out] 

* Chain [68,81]: 6*s(199)+4*s(203)+16
  Such that:aux(74) =< 1
aux(75) =< V
s(203) =< aux(74)
s(199) =< aux(75)

  with precondition: [Out>=5,V1>=V,V+4>=Out] 

* Chain [68,80]: 6*s(199)+4*s(203)+9
  Such that:aux(74) =< 1
aux(75) =< V
s(203) =< aux(74)
s(199) =< aux(75)

  with precondition: [Out>=6,V1>=V,V+5>=Out] 

* Chain [67,82]: 11
  with precondition: [Out=5,V>=1,V1>=V] 

* Chain [67,81]: 20
  with precondition: [Out=6,V>=1,V1>=V] 

* Chain [67,80]: 13
  with precondition: [Out=7,V>=1,V1>=V] 

* Chain [66,82]: 6*s(213)+7
  Such that:aux(83) =< V
s(213) =< aux(83)

  with precondition: [Out>=4,V1>=2*V,V+3>=Out] 

* Chain [66,81]: 6*s(213)+16
  Such that:aux(83) =< V
s(213) =< aux(83)

  with precondition: [Out>=5,V1>=2*V,V+4>=Out] 

* Chain [66,80]: 6*s(213)+9
  Such that:aux(83) =< V
s(213) =< aux(83)

  with precondition: [Out>=6,V1>=2*V,V+5>=Out] 

* Chain [65,82]: 8*s(219)+1*s(226)+7
  Such that:s(226) =< 1
aux(89) =< V
s(219) =< aux(89)

  with precondition: [Out>=5,V1>=2*V,2*V+3>=Out] 

* Chain [65,81]: 8*s(219)+1*s(226)+16
  Such that:s(226) =< 1
aux(89) =< V
s(219) =< aux(89)

  with precondition: [Out>=6,V1>=2*V,2*V+4>=Out] 

* Chain [65,80]: 8*s(219)+1*s(226)+9
  Such that:s(226) =< 1
aux(89) =< V
s(219) =< aux(89)

  with precondition: [Out>=7,V1>=2*V,2*V+5>=Out] 

* Chain [64,82]: 5*s(228)+1*s(233)+7
  Such that:s(233) =< 1
aux(95) =< V
s(228) =< aux(95)

  with precondition: [Out>=6,V1>=2*V,2*V+4>=Out] 

* Chain [64,81]: 5*s(228)+1*s(233)+16
  Such that:s(233) =< 1
aux(95) =< V
s(228) =< aux(95)

  with precondition: [Out>=7,V1>=2*V,2*V+5>=Out] 

* Chain [64,80]: 5*s(228)+1*s(233)+9
  Such that:s(233) =< 1
aux(95) =< V
s(228) =< aux(95)

  with precondition: [Out>=8,V1>=2*V,2*V+6>=Out] 

* Chain [63,82]: 4*s(234)+1*s(237)+7
  Such that:s(237) =< 1
aux(99) =< V
s(234) =< aux(99)

  with precondition: [Out>=5,V1>=2*V,V+4>=Out] 

* Chain [63,81]: 4*s(234)+1*s(237)+16
  Such that:s(237) =< 1
aux(99) =< V
s(234) =< aux(99)

  with precondition: [Out>=6,V1>=2*V,V+5>=Out] 

* Chain [63,80]: 4*s(234)+1*s(237)+9
  Such that:s(237) =< 1
aux(99) =< V
s(234) =< aux(99)

  with precondition: [Out>=7,V1>=2*V,V+6>=Out] 

* Chain [62,82]: 3*s(239)+3*s(240)+7
  Such that:aux(103) =< 1
aux(104) =< V
s(240) =< aux(103)
s(239) =< aux(104)

  with precondition: [Out>=6,V1>=V,V+5>=Out] 

* Chain [62,81]: 3*s(239)+3*s(240)+16
  Such that:aux(103) =< 1
aux(104) =< V
s(240) =< aux(103)
s(239) =< aux(104)

  with precondition: [Out>=7,V1>=V,V+6>=Out] 

* Chain [62,80]: 3*s(239)+3*s(240)+9
  Such that:aux(103) =< 1
aux(104) =< V
s(240) =< aux(103)
s(239) =< aux(104)

  with precondition: [Out>=8,V1>=V,V+7>=Out] 


#### Cost of chains of start(V1,V,V17,V20):
* Chain [90]: 12*s(1027)+334*s(1028)+110*s(1040)+168*s(1042)+550*s(1045)+380*s(1046)+44*s(1048)+308*s(1049)+750*s(1050)+396*s(1051)+300*s(1054)+60*s(1055)+120*s(1056)+24*s(1059)+168*s(1060)+360*s(1061)+216*s(1062)+156*s(1063)+125*s(1066)+25*s(1067)+10*s(1068)+70*s(1069)+50*s(1073)+10*s(1074)+20*s(1075)+4*s(1078)+28*s(1079)+60*s(1080)+36*s(1081)+20
  Such that:s(1034) =< V1-2*V
aux(132) =< 1
aux(133) =< V1
aux(134) =< V1+1
aux(135) =< V1-2*V+1
aux(136) =< V1-V
aux(137) =< V1-V+1
aux(138) =< V
aux(139) =< V+1
s(1040) =< aux(132)
s(1063) =< aux(133)
s(1027) =< aux(134)
s(1028) =< aux(138)
s(1042) =< aux(139)
s(1043) =< aux(133)
s(1044) =< aux(133)
s(1045) =< aux(133)
s(1046) =< aux(133)
s(1047) =< aux(133)
s(1044) =< aux(135)
s(1046) =< aux(135)
s(1044) =< aux(136)
s(1046) =< aux(136)
s(1045) =< aux(136)
s(1043) =< aux(137)
s(1044) =< aux(137)
s(1045) =< aux(137)
s(1046) =< aux(137)
s(1043) =< aux(136)
s(1047) =< aux(136)
s(1048) =< s(1044)
s(1049) =< s(1043)
s(1050) =< s(1047)
s(1051) =< aux(136)
s(1052) =< aux(133)
s(1053) =< aux(133)
s(1054) =< aux(133)
s(1055) =< aux(133)
s(1056) =< aux(133)
s(1057) =< aux(133)
s(1053) =< aux(135)
s(1055) =< aux(135)
s(1056) =< aux(135)
s(1053) =< s(1034)
s(1055) =< s(1034)
s(1054) =< s(1034)
s(1056) =< s(1034)
s(1056) =< aux(136)
s(1058) =< aux(136)
s(1052) =< aux(137)
s(1053) =< aux(137)
s(1054) =< aux(137)
s(1055) =< aux(137)
s(1056) =< aux(137)
s(1052) =< s(1034)
s(1058) =< s(1034)
s(1057) =< s(1034)
s(1059) =< s(1053)
s(1060) =< s(1052)
s(1061) =< s(1057)
s(1062) =< s(1058)
s(1064) =< aux(133)
s(1065) =< aux(133)
s(1066) =< aux(133)
s(1067) =< aux(133)
s(1065) =< aux(135)
s(1067) =< aux(135)
s(1064) =< aux(137)
s(1065) =< aux(137)
s(1066) =< aux(137)
s(1067) =< aux(137)
s(1068) =< s(1065)
s(1069) =< s(1064)
s(1071) =< aux(133)
s(1072) =< aux(133)
s(1073) =< aux(133)
s(1074) =< aux(133)
s(1075) =< aux(133)
s(1076) =< aux(133)
s(1072) =< aux(135)
s(1074) =< aux(135)
s(1075) =< aux(135)
s(1072) =< aux(134)
s(1074) =< aux(134)
s(1073) =< aux(134)
s(1075) =< aux(134)
s(1075) =< aux(136)
s(1077) =< aux(136)
s(1071) =< aux(137)
s(1072) =< aux(137)
s(1073) =< aux(137)
s(1074) =< aux(137)
s(1075) =< aux(137)
s(1071) =< aux(134)
s(1077) =< aux(134)
s(1076) =< aux(134)
s(1078) =< s(1072)
s(1079) =< s(1071)
s(1080) =< s(1076)
s(1081) =< s(1077)

  with precondition: [V1>=0] 

* Chain [89]: 1
  with precondition: [V1=1,V>=0,V17>=0,V20>=0] 

* Chain [88]: 1
  with precondition: [V1=2,V=1,V17>=0,V20>=0] 

* Chain [87]: 6*s(1162)+5416*s(1163)+1764*s(1179)+2688*s(1181)+8800*s(1184)+6080*s(1185)+704*s(1187)+4928*s(1188)+12000*s(1189)+6336*s(1190)+4800*s(1193)+960*s(1194)+1920*s(1195)+384*s(1198)+2688*s(1199)+5760*s(1200)+3456*s(1201)+2488*s(1202)+2000*s(1205)+400*s(1206)+160*s(1207)+1120*s(1208)+120*s(1209)+800*s(1212)+160*s(1213)+320*s(1214)+64*s(1217)+448*s(1218)+960*s(1219)+576*s(1220)+12*s(3332)+24*s(3333)+23
  Such that:aux(180) =< 1
aux(181) =< V
aux(182) =< V+1
aux(183) =< V17+1
aux(184) =< V17-3*V20
aux(185) =< V17-3*V20+1
aux(186) =< V17-2*V20
aux(187) =< V17-2*V20+1
aux(188) =< V17-V20
aux(189) =< V17-V20+1
aux(190) =< V20
aux(191) =< V20+1
s(1179) =< aux(180)
s(1162) =< aux(183)
s(1202) =< aux(188)
s(1209) =< aux(189)
s(1163) =< aux(190)
s(1181) =< aux(191)
s(1182) =< aux(188)
s(1183) =< aux(188)
s(1184) =< aux(188)
s(1185) =< aux(188)
s(1186) =< aux(188)
s(1183) =< aux(185)
s(1185) =< aux(185)
s(1183) =< aux(186)
s(1185) =< aux(186)
s(1184) =< aux(186)
s(1182) =< aux(187)
s(1183) =< aux(187)
s(1184) =< aux(187)
s(1185) =< aux(187)
s(1182) =< aux(186)
s(1186) =< aux(186)
s(1187) =< s(1183)
s(1188) =< s(1182)
s(1189) =< s(1186)
s(1190) =< aux(186)
s(1191) =< aux(188)
s(1192) =< aux(188)
s(1193) =< aux(188)
s(1194) =< aux(188)
s(1195) =< aux(188)
s(1196) =< aux(188)
s(1192) =< aux(185)
s(1194) =< aux(185)
s(1195) =< aux(185)
s(1192) =< aux(184)
s(1194) =< aux(184)
s(1193) =< aux(184)
s(1195) =< aux(184)
s(1195) =< aux(186)
s(1197) =< aux(186)
s(1191) =< aux(187)
s(1192) =< aux(187)
s(1193) =< aux(187)
s(1194) =< aux(187)
s(1195) =< aux(187)
s(1191) =< aux(184)
s(1197) =< aux(184)
s(1196) =< aux(184)
s(1198) =< s(1192)
s(1199) =< s(1191)
s(1200) =< s(1196)
s(1201) =< s(1197)
s(1203) =< aux(188)
s(1204) =< aux(188)
s(1205) =< aux(188)
s(1206) =< aux(188)
s(1204) =< aux(185)
s(1206) =< aux(185)
s(1203) =< aux(187)
s(1204) =< aux(187)
s(1205) =< aux(187)
s(1206) =< aux(187)
s(1207) =< s(1204)
s(1208) =< s(1203)
s(1210) =< aux(188)
s(1211) =< aux(188)
s(1212) =< aux(188)
s(1213) =< aux(188)
s(1214) =< aux(188)
s(1215) =< aux(188)
s(1211) =< aux(185)
s(1213) =< aux(185)
s(1214) =< aux(185)
s(1211) =< aux(189)
s(1213) =< aux(189)
s(1212) =< aux(189)
s(1214) =< aux(189)
s(1214) =< aux(186)
s(1216) =< aux(186)
s(1210) =< aux(187)
s(1211) =< aux(187)
s(1212) =< aux(187)
s(1213) =< aux(187)
s(1214) =< aux(187)
s(1210) =< aux(189)
s(1216) =< aux(189)
s(1215) =< aux(189)
s(1217) =< s(1211)
s(1218) =< s(1210)
s(1219) =< s(1215)
s(1220) =< s(1216)
s(3332) =< aux(181)
s(3333) =< aux(182)

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

* Chain [86]: 6
  with precondition: [V1=2,V=2,V20=0,V17>=0] 

* Chain [85]: 144*s(3349)+162*s(3350)+288*s(3351)+19
  Such that:aux(210) =< 1
aux(211) =< V20
aux(212) =< V20+1
s(3349) =< aux(210)
s(3350) =< aux(211)
s(3351) =< aux(212)

  with precondition: [V1=2,V=2,V17=2*V20,V17>=2] 

* Chain [84]: 18*s(3580)+4*s(3581)+14
  Such that:aux(213) =< V20
aux(214) =< V20+1
s(3581) =< aux(213)
s(3580) =< aux(214)

  with precondition: [V1=2,V=2,V17=V20,V17>=1] 

* Chain [83]: 3
  with precondition: [V=0,V1>=0] 


Closed-form bounds of start(V1,V,V17,V20): 
-------------------------------------
* Chain [90] with precondition: [V1>=0] 
    - Upper bound: 3622*V1+130+nat(V)*334+(12*V1+12)+nat(V+1)*168+nat(V1-V)*648 
    - Complexity: n 
* Chain [89] with precondition: [V1=1,V>=0,V17>=0,V20>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [88] with precondition: [V1=2,V=1,V17>=0,V20>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [87] with precondition: [V1=V,V1>=1] 
    - Upper bound: 12*V+1787+nat(V20)*5416+(24*V+24)+nat(V17+1)*6+nat(V20+1)*2688+nat(V17-V20+1)*120+nat(V17-V20)*57944+nat(V17-2*V20)*10368 
    - Complexity: n 
* Chain [86] with precondition: [V1=2,V=2,V20=0,V17>=0] 
    - Upper bound: 6 
    - Complexity: constant 
* Chain [85] with precondition: [V1=2,V=2,V17=2*V20,V17>=2] 
    - Upper bound: 450*V20+451 
    - Complexity: n 
* Chain [84] with precondition: [V1=2,V=2,V17=V20,V17>=1] 
    - Upper bound: 22*V20+32 
    - Complexity: n 
* Chain [83] with precondition: [V=0,V1>=0] 
    - Upper bound: 3 
    - Complexity: constant 

### Maximum cost of start(V1,V,V17,V20): max([max([5,3622*V1+129+nat(V)*334+(12*V1+12)+nat(V+1)*168+nat(V1-V)*648]),nat(V)*12+1624+nat(V20)*5254+nat(V+1)*24+nat(V17+1)*6+nat(V20+1)*2400+nat(V17-V20+1)*120+nat(V17-V20)*57944+nat(V17-2*V20)*10368+(nat(V20)*158+149+nat(V20+1)*270)+(nat(V20)*4+13+nat(V20+1)*18)])+1 
Asymptotic class: n 
* Total analysis performed in 18899 ms.


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

(12)
BOUNDS(1, n^1)

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

(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^1, INF).


The TRS R consists of the following rules:

   GE(z0, 0') -> c
   GE(0', s(z0)) -> c1
   GE(s(z0), s(z1)) -> c2(GE(z0, z1))
   MINUS(z0, 0') -> c3
   MINUS(0', z0) -> c4
   MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
   ID_INC(z0) -> c6
   ID_INC(z0) -> c7
   DIV(z0, z1) -> c8(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z1, s(0')))
   DIV(z0, z1) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z0, z1))
   IF(false, z0, z1, z2) -> c10
   IF(true, false, z0, z1) -> c11
   IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))

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

   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   minus(z0, 0') -> z0
   minus(0', z0) -> 0'
   minus(s(z0), s(z1)) -> minus(z0, z1)
   id_inc(z0) -> z0
   id_inc(z0) -> s(z0)
   div(z0, z1) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1)
   if(false, z0, z1, z2) -> div_by_zero
   if(true, false, z0, z1) -> 0'
   if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

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

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

(16)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
MINUS(z0, 0') -> c3
MINUS(0', z0) -> c4
MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
ID_INC(z0) -> c6
ID_INC(z0) -> c7
DIV(z0, z1) -> c8(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z1, s(0')))
DIV(z0, z1) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z0, z1))
IF(false, z0, z1, z2) -> c10
IF(true, false, z0, z1) -> c11
IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
id_inc(z0) -> z0
id_inc(z0) -> s(z0)
div(z0, z1) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1)
if(false, z0, z1, z2) -> div_by_zero
if(true, false, z0, z1) -> 0'
if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

Types:
GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2
0' :: 0':s:div_by_zero
c :: c:c1:c2
s :: 0':s:div_by_zero -> 0':s:div_by_zero
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ID_INC :: 0':s:div_by_zero -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8:c9
c8 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> c10:c11:c12
ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true
c9 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
false :: false:true
c10 :: c10:c11:c12
true :: false:true
c11 :: c10:c11:c12
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5 -> c10:c11:c12
div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero
if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
div_by_zero :: 0':s:div_by_zero
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s:div_by_zero2_13 :: 0':s:div_by_zero
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c95_13 :: c8:c9
hole_c10:c11:c126_13 :: c10:c11:c12
hole_false:true7_13 :: false:true
gen_c:c1:c28_13 :: Nat -> c:c1:c2
gen_0':s:div_by_zero9_13 :: Nat -> 0':s:div_by_zero
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5

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

(17) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
GE, MINUS, DIV, ge, div, minus

They will be analysed ascendingly in the following order:
GE < DIV
MINUS < DIV
ge < DIV
div < DIV
minus < DIV
ge < div
minus < div

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

(18)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
MINUS(z0, 0') -> c3
MINUS(0', z0) -> c4
MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
ID_INC(z0) -> c6
ID_INC(z0) -> c7
DIV(z0, z1) -> c8(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z1, s(0')))
DIV(z0, z1) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z0, z1))
IF(false, z0, z1, z2) -> c10
IF(true, false, z0, z1) -> c11
IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
id_inc(z0) -> z0
id_inc(z0) -> s(z0)
div(z0, z1) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1)
if(false, z0, z1, z2) -> div_by_zero
if(true, false, z0, z1) -> 0'
if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

Types:
GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2
0' :: 0':s:div_by_zero
c :: c:c1:c2
s :: 0':s:div_by_zero -> 0':s:div_by_zero
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ID_INC :: 0':s:div_by_zero -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8:c9
c8 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> c10:c11:c12
ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true
c9 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
false :: false:true
c10 :: c10:c11:c12
true :: false:true
c11 :: c10:c11:c12
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5 -> c10:c11:c12
div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero
if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
div_by_zero :: 0':s:div_by_zero
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s:div_by_zero2_13 :: 0':s:div_by_zero
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c95_13 :: c8:c9
hole_c10:c11:c126_13 :: c10:c11:c12
hole_false:true7_13 :: false:true
gen_c:c1:c28_13 :: Nat -> c:c1:c2
gen_0':s:div_by_zero9_13 :: Nat -> 0':s:div_by_zero
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5


Generator Equations:
gen_c:c1:c28_13(0) <=> c
gen_c:c1:c28_13(+(x, 1)) <=> c2(gen_c:c1:c28_13(x))
gen_0':s:div_by_zero9_13(0) <=> 0'
gen_0':s:div_by_zero9_13(+(x, 1)) <=> s(gen_0':s:div_by_zero9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))


The following defined symbols remain to be analysed:
GE, MINUS, DIV, ge, div, minus

They will be analysed ascendingly in the following order:
GE < DIV
MINUS < DIV
ge < DIV
div < DIV
minus < DIV
ge < div
minus < div

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s:div_by_zero9_13(n12_13), gen_0':s:div_by_zero9_13(n12_13)) -> gen_c:c1:c28_13(n12_13), rt in Omega(1 + n12_13)

Induction Base:
GE(gen_0':s:div_by_zero9_13(0), gen_0':s:div_by_zero9_13(0)) ->_R^Omega(1)
c

Induction Step:
GE(gen_0':s:div_by_zero9_13(+(n12_13, 1)), gen_0':s:div_by_zero9_13(+(n12_13, 1))) ->_R^Omega(1)
c2(GE(gen_0':s:div_by_zero9_13(n12_13), gen_0':s:div_by_zero9_13(n12_13))) ->_IH
c2(gen_c:c1:c28_13(c13_13))

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

(20)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
MINUS(z0, 0') -> c3
MINUS(0', z0) -> c4
MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
ID_INC(z0) -> c6
ID_INC(z0) -> c7
DIV(z0, z1) -> c8(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z1, s(0')))
DIV(z0, z1) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z0, z1))
IF(false, z0, z1, z2) -> c10
IF(true, false, z0, z1) -> c11
IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
id_inc(z0) -> z0
id_inc(z0) -> s(z0)
div(z0, z1) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1)
if(false, z0, z1, z2) -> div_by_zero
if(true, false, z0, z1) -> 0'
if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

Types:
GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2
0' :: 0':s:div_by_zero
c :: c:c1:c2
s :: 0':s:div_by_zero -> 0':s:div_by_zero
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ID_INC :: 0':s:div_by_zero -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8:c9
c8 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> c10:c11:c12
ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true
c9 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
false :: false:true
c10 :: c10:c11:c12
true :: false:true
c11 :: c10:c11:c12
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5 -> c10:c11:c12
div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero
if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
div_by_zero :: 0':s:div_by_zero
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s:div_by_zero2_13 :: 0':s:div_by_zero
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c95_13 :: c8:c9
hole_c10:c11:c126_13 :: c10:c11:c12
hole_false:true7_13 :: false:true
gen_c:c1:c28_13 :: Nat -> c:c1:c2
gen_0':s:div_by_zero9_13 :: Nat -> 0':s:div_by_zero
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5


Generator Equations:
gen_c:c1:c28_13(0) <=> c
gen_c:c1:c28_13(+(x, 1)) <=> c2(gen_c:c1:c28_13(x))
gen_0':s:div_by_zero9_13(0) <=> 0'
gen_0':s:div_by_zero9_13(+(x, 1)) <=> s(gen_0':s:div_by_zero9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))


The following defined symbols remain to be analysed:
GE, MINUS, DIV, ge, div, minus

They will be analysed ascendingly in the following order:
GE < DIV
MINUS < DIV
ge < DIV
div < DIV
minus < DIV
ge < div
minus < div

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

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

(23)
BOUNDS(n^1, INF)

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

(24)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
MINUS(z0, 0') -> c3
MINUS(0', z0) -> c4
MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
ID_INC(z0) -> c6
ID_INC(z0) -> c7
DIV(z0, z1) -> c8(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z1, s(0')))
DIV(z0, z1) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z0, z1))
IF(false, z0, z1, z2) -> c10
IF(true, false, z0, z1) -> c11
IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
id_inc(z0) -> z0
id_inc(z0) -> s(z0)
div(z0, z1) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1)
if(false, z0, z1, z2) -> div_by_zero
if(true, false, z0, z1) -> 0'
if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

Types:
GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2
0' :: 0':s:div_by_zero
c :: c:c1:c2
s :: 0':s:div_by_zero -> 0':s:div_by_zero
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ID_INC :: 0':s:div_by_zero -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8:c9
c8 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> c10:c11:c12
ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true
c9 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
false :: false:true
c10 :: c10:c11:c12
true :: false:true
c11 :: c10:c11:c12
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5 -> c10:c11:c12
div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero
if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
div_by_zero :: 0':s:div_by_zero
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s:div_by_zero2_13 :: 0':s:div_by_zero
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c95_13 :: c8:c9
hole_c10:c11:c126_13 :: c10:c11:c12
hole_false:true7_13 :: false:true
gen_c:c1:c28_13 :: Nat -> c:c1:c2
gen_0':s:div_by_zero9_13 :: Nat -> 0':s:div_by_zero
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5


Lemmas:
GE(gen_0':s:div_by_zero9_13(n12_13), gen_0':s:div_by_zero9_13(n12_13)) -> gen_c:c1:c28_13(n12_13), rt in Omega(1 + n12_13)


Generator Equations:
gen_c:c1:c28_13(0) <=> c
gen_c:c1:c28_13(+(x, 1)) <=> c2(gen_c:c1:c28_13(x))
gen_0':s:div_by_zero9_13(0) <=> 0'
gen_0':s:div_by_zero9_13(+(x, 1)) <=> s(gen_0':s:div_by_zero9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))


The following defined symbols remain to be analysed:
MINUS, DIV, ge, div, minus

They will be analysed ascendingly in the following order:
MINUS < DIV
ge < DIV
div < DIV
minus < DIV
ge < div
minus < div

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINUS(gen_0':s:div_by_zero9_13(n636_13), gen_0':s:div_by_zero9_13(n636_13)) -> gen_c3:c4:c510_13(n636_13), rt in Omega(1 + n636_13)

Induction Base:
MINUS(gen_0':s:div_by_zero9_13(0), gen_0':s:div_by_zero9_13(0)) ->_R^Omega(1)
c3

Induction Step:
MINUS(gen_0':s:div_by_zero9_13(+(n636_13, 1)), gen_0':s:div_by_zero9_13(+(n636_13, 1))) ->_R^Omega(1)
c5(MINUS(gen_0':s:div_by_zero9_13(n636_13), gen_0':s:div_by_zero9_13(n636_13))) ->_IH
c5(gen_c3:c4:c510_13(c637_13))

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

(26)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
MINUS(z0, 0') -> c3
MINUS(0', z0) -> c4
MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
ID_INC(z0) -> c6
ID_INC(z0) -> c7
DIV(z0, z1) -> c8(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z1, s(0')))
DIV(z0, z1) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z0, z1))
IF(false, z0, z1, z2) -> c10
IF(true, false, z0, z1) -> c11
IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
id_inc(z0) -> z0
id_inc(z0) -> s(z0)
div(z0, z1) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1)
if(false, z0, z1, z2) -> div_by_zero
if(true, false, z0, z1) -> 0'
if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

Types:
GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2
0' :: 0':s:div_by_zero
c :: c:c1:c2
s :: 0':s:div_by_zero -> 0':s:div_by_zero
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ID_INC :: 0':s:div_by_zero -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8:c9
c8 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> c10:c11:c12
ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true
c9 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
false :: false:true
c10 :: c10:c11:c12
true :: false:true
c11 :: c10:c11:c12
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5 -> c10:c11:c12
div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero
if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
div_by_zero :: 0':s:div_by_zero
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s:div_by_zero2_13 :: 0':s:div_by_zero
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c95_13 :: c8:c9
hole_c10:c11:c126_13 :: c10:c11:c12
hole_false:true7_13 :: false:true
gen_c:c1:c28_13 :: Nat -> c:c1:c2
gen_0':s:div_by_zero9_13 :: Nat -> 0':s:div_by_zero
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5


Lemmas:
GE(gen_0':s:div_by_zero9_13(n12_13), gen_0':s:div_by_zero9_13(n12_13)) -> gen_c:c1:c28_13(n12_13), rt in Omega(1 + n12_13)
MINUS(gen_0':s:div_by_zero9_13(n636_13), gen_0':s:div_by_zero9_13(n636_13)) -> gen_c3:c4:c510_13(n636_13), rt in Omega(1 + n636_13)


Generator Equations:
gen_c:c1:c28_13(0) <=> c
gen_c:c1:c28_13(+(x, 1)) <=> c2(gen_c:c1:c28_13(x))
gen_0':s:div_by_zero9_13(0) <=> 0'
gen_0':s:div_by_zero9_13(+(x, 1)) <=> s(gen_0':s:div_by_zero9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))


The following defined symbols remain to be analysed:
ge, DIV, div, minus

They will be analysed ascendingly in the following order:
ge < DIV
div < DIV
minus < DIV
ge < div
minus < div

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s:div_by_zero9_13(n1182_13), gen_0':s:div_by_zero9_13(n1182_13)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s:div_by_zero9_13(0), gen_0':s:div_by_zero9_13(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s:div_by_zero9_13(+(n1182_13, 1)), gen_0':s:div_by_zero9_13(+(n1182_13, 1))) ->_R^Omega(0)
ge(gen_0':s:div_by_zero9_13(n1182_13), gen_0':s:div_by_zero9_13(n1182_13)) ->_IH
true

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:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
MINUS(z0, 0') -> c3
MINUS(0', z0) -> c4
MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
ID_INC(z0) -> c6
ID_INC(z0) -> c7
DIV(z0, z1) -> c8(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z1, s(0')))
DIV(z0, z1) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z0, z1))
IF(false, z0, z1, z2) -> c10
IF(true, false, z0, z1) -> c11
IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
id_inc(z0) -> z0
id_inc(z0) -> s(z0)
div(z0, z1) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1)
if(false, z0, z1, z2) -> div_by_zero
if(true, false, z0, z1) -> 0'
if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

Types:
GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2
0' :: 0':s:div_by_zero
c :: c:c1:c2
s :: 0':s:div_by_zero -> 0':s:div_by_zero
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ID_INC :: 0':s:div_by_zero -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8:c9
c8 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> c10:c11:c12
ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true
c9 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
false :: false:true
c10 :: c10:c11:c12
true :: false:true
c11 :: c10:c11:c12
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5 -> c10:c11:c12
div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero
if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
div_by_zero :: 0':s:div_by_zero
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s:div_by_zero2_13 :: 0':s:div_by_zero
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c95_13 :: c8:c9
hole_c10:c11:c126_13 :: c10:c11:c12
hole_false:true7_13 :: false:true
gen_c:c1:c28_13 :: Nat -> c:c1:c2
gen_0':s:div_by_zero9_13 :: Nat -> 0':s:div_by_zero
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5


Lemmas:
GE(gen_0':s:div_by_zero9_13(n12_13), gen_0':s:div_by_zero9_13(n12_13)) -> gen_c:c1:c28_13(n12_13), rt in Omega(1 + n12_13)
MINUS(gen_0':s:div_by_zero9_13(n636_13), gen_0':s:div_by_zero9_13(n636_13)) -> gen_c3:c4:c510_13(n636_13), rt in Omega(1 + n636_13)
ge(gen_0':s:div_by_zero9_13(n1182_13), gen_0':s:div_by_zero9_13(n1182_13)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c28_13(0) <=> c
gen_c:c1:c28_13(+(x, 1)) <=> c2(gen_c:c1:c28_13(x))
gen_0':s:div_by_zero9_13(0) <=> 0'
gen_0':s:div_by_zero9_13(+(x, 1)) <=> s(gen_0':s:div_by_zero9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))


The following defined symbols remain to be analysed:
minus, DIV, div

They will be analysed ascendingly in the following order:
div < DIV
minus < DIV
minus < div

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minus(gen_0':s:div_by_zero9_13(n1592_13), gen_0':s:div_by_zero9_13(n1592_13)) -> gen_0':s:div_by_zero9_13(0), rt in Omega(0)

Induction Base:
minus(gen_0':s:div_by_zero9_13(0), gen_0':s:div_by_zero9_13(0)) ->_R^Omega(0)
gen_0':s:div_by_zero9_13(0)

Induction Step:
minus(gen_0':s:div_by_zero9_13(+(n1592_13, 1)), gen_0':s:div_by_zero9_13(+(n1592_13, 1))) ->_R^Omega(0)
minus(gen_0':s:div_by_zero9_13(n1592_13), gen_0':s:div_by_zero9_13(n1592_13)) ->_IH
gen_0':s:div_by_zero9_13(0)

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

(30)
Obligation:
Innermost TRS:
Rules:
GE(z0, 0') -> c
GE(0', s(z0)) -> c1
GE(s(z0), s(z1)) -> c2(GE(z0, z1))
MINUS(z0, 0') -> c3
MINUS(0', z0) -> c4
MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1))
ID_INC(z0) -> c6
ID_INC(z0) -> c7
DIV(z0, z1) -> c8(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z1, s(0')))
DIV(z0, z1) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1), GE(z0, z1))
IF(false, z0, z1, z2) -> c10
IF(true, false, z0, z1) -> c11
IF(true, true, z0, z1) -> c12(ID_INC(div(minus(z0, z1), z1)), DIV(minus(z0, z1), z1), MINUS(z0, z1))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
id_inc(z0) -> z0
id_inc(z0) -> s(z0)
div(z0, z1) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1)
if(false, z0, z1, z2) -> div_by_zero
if(true, false, z0, z1) -> 0'
if(true, true, z0, z1) -> id_inc(div(minus(z0, z1), z1))

Types:
GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2
0' :: 0':s:div_by_zero
c :: c:c1:c2
s :: 0':s:div_by_zero -> 0':s:div_by_zero
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ID_INC :: 0':s:div_by_zero -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8:c9
c8 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> c10:c11:c12
ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true
c9 :: c10:c11:c12 -> c:c1:c2 -> c8:c9
false :: false:true
c10 :: c10:c11:c12
true :: false:true
c11 :: c10:c11:c12
c12 :: c6:c7 -> c8:c9 -> c3:c4:c5 -> c10:c11:c12
div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero
if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero
div_by_zero :: 0':s:div_by_zero
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s:div_by_zero2_13 :: 0':s:div_by_zero
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c95_13 :: c8:c9
hole_c10:c11:c126_13 :: c10:c11:c12
hole_false:true7_13 :: false:true
gen_c:c1:c28_13 :: Nat -> c:c1:c2
gen_0':s:div_by_zero9_13 :: Nat -> 0':s:div_by_zero
gen_c3:c4:c510_13 :: Nat -> c3:c4:c5


Lemmas:
GE(gen_0':s:div_by_zero9_13(n12_13), gen_0':s:div_by_zero9_13(n12_13)) -> gen_c:c1:c28_13(n12_13), rt in Omega(1 + n12_13)
MINUS(gen_0':s:div_by_zero9_13(n636_13), gen_0':s:div_by_zero9_13(n636_13)) -> gen_c3:c4:c510_13(n636_13), rt in Omega(1 + n636_13)
ge(gen_0':s:div_by_zero9_13(n1182_13), gen_0':s:div_by_zero9_13(n1182_13)) -> true, rt in Omega(0)
minus(gen_0':s:div_by_zero9_13(n1592_13), gen_0':s:div_by_zero9_13(n1592_13)) -> gen_0':s:div_by_zero9_13(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c28_13(0) <=> c
gen_c:c1:c28_13(+(x, 1)) <=> c2(gen_c:c1:c28_13(x))
gen_0':s:div_by_zero9_13(0) <=> 0'
gen_0':s:div_by_zero9_13(+(x, 1)) <=> s(gen_0':s:div_by_zero9_13(x))
gen_c3:c4:c510_13(0) <=> c3
gen_c3:c4:c510_13(+(x, 1)) <=> c5(gen_c3:c4:c510_13(x))


The following defined symbols remain to be analysed:
div, DIV

They will be analysed ascendingly in the following order:
div < DIV