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), 398 ms]
(2) CpxRelTRS
(3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxWeightedTrs
    (5) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CpxWeightedTrs
    (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxTypedWeightedTrs
    (9) CompletionProof [UPPER BOUND(ID), 0 ms]
    (10) CpxTypedWeightedCompleteTrs
    (11) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (12) CpxRNTS
    (13) CompleteCoflocoProof [FINISHED, 3434 ms]
    (14) BOUNDS(1, n^1)
(15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(16) TRS for Loop Detection
    (17) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
    (18) BEST
        (19) proven lower bound
            (20) LowerBoundPropagationProof [FINISHED, 0 ms]
            (21) BOUNDS(n^1, INF)
        (22) TRS for Loop Detection


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

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(0, s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   LT(z0, 0) -> c3
   LT(0, s(z0)) -> c4
   LT(s(z0), s(z1)) -> c5(LT(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   DIV(z0, 0) -> c8
   DIV(0, z0) -> c9
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), LT(z0, z1))
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), DIV(-(z0, z1), s(z1)), -'(z0, z1))

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

   -(z0, 0) -> z0
   -(0, s(z0)) -> 0
   -(s(z0), s(z1)) -> -(z0, z1)
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   div(z0, 0) -> 0
   div(0, z0) -> 0
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(-(z0, z1), s(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:

   -'(z0, 0) -> c
   -'(0, s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   LT(z0, 0) -> c3
   LT(0, s(z0)) -> c4
   LT(s(z0), s(z1)) -> c5(LT(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   DIV(z0, 0) -> c8
   DIV(0, z0) -> c9
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), LT(z0, z1))
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), DIV(-(z0, z1), s(z1)), -'(z0, z1))

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

   -(z0, 0) -> z0
   -(0, s(z0)) -> 0
   -(s(z0), s(z1)) -> -(z0, z1)
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   div(z0, 0) -> 0
   div(0, z0) -> 0
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(-(z0, z1), s(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:

   -'(z0, 0) -> c [1]
   -'(0, s(z0)) -> c1 [1]
   -'(s(z0), s(z1)) -> c2(-'(z0, z1)) [1]
   LT(z0, 0) -> c3 [1]
   LT(0, s(z0)) -> c4 [1]
   LT(s(z0), s(z1)) -> c5(LT(z0, z1)) [1]
   IF(true, z0, z1) -> c6 [1]
   IF(false, z0, z1) -> c7 [1]
   DIV(z0, 0) -> c8 [1]
   DIV(0, z0) -> c9 [1]
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), LT(z0, z1)) [1]
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), DIV(-(z0, z1), s(z1)), -'(z0, z1)) [1]
   -(z0, 0) -> z0 [0]
   -(0, s(z0)) -> 0 [0]
   -(s(z0), s(z1)) -> -(z0, z1) [0]
   lt(z0, 0) -> false [0]
   lt(0, s(z0)) -> true [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   div(z0, 0) -> 0 [0]
   div(0, z0) -> 0 [0]
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))) [0]

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

(5) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID))
Renamed defined symbols to avoid conflicts with arithmetic symbols:

- => minus

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

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

   -'(z0, 0) -> c [1]
   -'(0, s(z0)) -> c1 [1]
   -'(s(z0), s(z1)) -> c2(-'(z0, z1)) [1]
   LT(z0, 0) -> c3 [1]
   LT(0, s(z0)) -> c4 [1]
   LT(s(z0), s(z1)) -> c5(LT(z0, z1)) [1]
   IF(true, z0, z1) -> c6 [1]
   IF(false, z0, z1) -> c7 [1]
   DIV(z0, 0) -> c8 [1]
   DIV(0, z0) -> c9 [1]
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))), LT(z0, z1)) [1]
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))), DIV(minus(z0, z1), s(z1)), -'(z0, z1)) [1]
   minus(z0, 0) -> z0 [0]
   minus(0, s(z0)) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   lt(z0, 0) -> false [0]
   lt(0, s(z0)) -> true [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   div(z0, 0) -> 0 [0]
   div(0, z0) -> 0 [0]
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))) [0]

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

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

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

   -'(z0, 0) -> c [1]
   -'(0, s(z0)) -> c1 [1]
   -'(s(z0), s(z1)) -> c2(-'(z0, z1)) [1]
   LT(z0, 0) -> c3 [1]
   LT(0, s(z0)) -> c4 [1]
   LT(s(z0), s(z1)) -> c5(LT(z0, z1)) [1]
   IF(true, z0, z1) -> c6 [1]
   IF(false, z0, z1) -> c7 [1]
   DIV(z0, 0) -> c8 [1]
   DIV(0, z0) -> c9 [1]
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))), LT(z0, z1)) [1]
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))), DIV(minus(z0, z1), s(z1)), -'(z0, z1)) [1]
   minus(z0, 0) -> z0 [0]
   minus(0, s(z0)) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   lt(z0, 0) -> false [0]
   lt(0, s(z0)) -> true [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   div(z0, 0) -> 0 [0]
   div(0, z0) -> 0 [0]
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))) [0]

The TRS has the following type information:
-' :: 0:s -> 0:s -> c:c1:c2
0 :: 0:s
c :: c:c1:c2
s :: 0:s -> 0:s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LT :: 0:s -> 0:s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
IF :: true:false -> 0:s -> 0:s -> c6:c7
true :: true:false
c6 :: c6:c7
false :: true:false
c7 :: c6:c7
DIV :: 0:s -> 0:s -> c8:c9:c10:c11
c8 :: c8:c9:c10:c11
c9 :: c8:c9:c10:c11
c10 :: c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11
lt :: 0:s -> 0:s -> true:false
div :: 0:s -> 0:s -> 0:s
minus :: 0:s -> 0:s -> 0:s
c11 :: c6:c7 -> c8:c9:c10:c11 -> c:c1:c2 -> c8:c9:c10:c11
if :: true:false -> 0:s -> 0:s -> 0:s

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

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

   minus(v0, v1) -> null_minus [0]
   lt(v0, v1) -> null_lt [0]
   if(v0, v1, v2) -> null_if [0]
   div(v0, v1) -> null_div [0]
   -'(v0, v1) -> null_-' [0]
   LT(v0, v1) -> null_LT [0]
   IF(v0, v1, v2) -> null_IF [0]
   DIV(v0, v1) -> null_DIV [0]

And the following fresh constants:    null_minus, null_lt, null_if, null_div, null_-', null_LT, null_IF, null_DIV

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

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

   -'(z0, 0) -> c [1]
   -'(0, s(z0)) -> c1 [1]
   -'(s(z0), s(z1)) -> c2(-'(z0, z1)) [1]
   LT(z0, 0) -> c3 [1]
   LT(0, s(z0)) -> c4 [1]
   LT(s(z0), s(z1)) -> c5(LT(z0, z1)) [1]
   IF(true, z0, z1) -> c6 [1]
   IF(false, z0, z1) -> c7 [1]
   DIV(z0, 0) -> c8 [1]
   DIV(0, z0) -> c9 [1]
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))), LT(z0, z1)) [1]
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))), DIV(minus(z0, z1), s(z1)), -'(z0, z1)) [1]
   minus(z0, 0) -> z0 [0]
   minus(0, s(z0)) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   lt(z0, 0) -> false [0]
   lt(0, s(z0)) -> true [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   if(true, z0, z1) -> z0 [0]
   if(false, z0, z1) -> z1 [0]
   div(z0, 0) -> 0 [0]
   div(0, z0) -> 0 [0]
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(minus(z0, z1), s(z1)))) [0]
   minus(v0, v1) -> null_minus [0]
   lt(v0, v1) -> null_lt [0]
   if(v0, v1, v2) -> null_if [0]
   div(v0, v1) -> null_div [0]
   -'(v0, v1) -> null_-' [0]
   LT(v0, v1) -> null_LT [0]
   IF(v0, v1, v2) -> null_IF [0]
   DIV(v0, v1) -> null_DIV [0]

The TRS has the following type information:
-' :: 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div -> c:c1:c2:null_-'
0 :: 0:s:null_minus:null_if:null_div
c :: c:c1:c2:null_-'
s :: 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div
c1 :: c:c1:c2:null_-'
c2 :: c:c1:c2:null_-' -> c:c1:c2:null_-'
LT :: 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div -> c3:c4:c5:null_LT
c3 :: c3:c4:c5:null_LT
c4 :: c3:c4:c5:null_LT
c5 :: c3:c4:c5:null_LT -> c3:c4:c5:null_LT
IF :: true:false:null_lt -> 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div -> c6:c7:null_IF
true :: true:false:null_lt
c6 :: c6:c7:null_IF
false :: true:false:null_lt
c7 :: c6:c7:null_IF
DIV :: 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div -> c8:c9:c10:c11:null_DIV
c8 :: c8:c9:c10:c11:null_DIV
c9 :: c8:c9:c10:c11:null_DIV
c10 :: c6:c7:null_IF -> c3:c4:c5:null_LT -> c8:c9:c10:c11:null_DIV
lt :: 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div -> true:false:null_lt
div :: 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div
minus :: 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div
c11 :: c6:c7:null_IF -> c8:c9:c10:c11:null_DIV -> c:c1:c2:null_-' -> c8:c9:c10:c11:null_DIV
if :: true:false:null_lt -> 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div -> 0:s:null_minus:null_if:null_div
null_minus :: 0:s:null_minus:null_if:null_div
null_lt :: true:false:null_lt
null_if :: 0:s:null_minus:null_if:null_div
null_div :: 0:s:null_minus:null_if:null_div
null_-' :: c:c1:c2:null_-'
null_LT :: c3:c4:c5:null_LT
null_IF :: c6:c7:null_IF
null_DIV :: c8:c9:c10:c11:null_DIV

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

(11) 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
   true => 2
   c6 => 1
   false => 1
   c7 => 2
   c8 => 0
   c9 => 1
   null_minus => 0
   null_lt => 0
   null_if => 0
   null_div => 0
   null_-' => 0
   null_LT => 0
   null_IF => 0
   null_DIV => 0

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

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

   -'(z, z') -{ 1 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0
   -'(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   -'(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   -'(z, z') -{ 1 }-> 1 + -'(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   DIV(z, z') -{ 1 }-> 1 :|: z0 >= 0, z = 0, z' = z0
   DIV(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   DIV(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   DIV(z, z') -{ 1 }-> 1 + IF(lt(z0, z1), 0, 1 + div(minus(z0, z1), 1 + z1)) + LT(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   DIV(z, z') -{ 1 }-> 1 + IF(lt(z0, z1), 0, 1 + div(minus(z0, z1), 1 + z1)) + DIV(minus(z0, z1), 1 + z1) + -'(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   IF(z, z', z'') -{ 1 }-> 2 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   LT(z, z') -{ 1 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0
   LT(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   LT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LT(z, z') -{ 1 }-> 1 + LT(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   div(z, z') -{ 0 }-> if(lt(z0, z1), 0, 1 + div(minus(z0, z1), 1 + z1)) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   div(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   div(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   div(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   if(z, z', z'') -{ 0 }-> z0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> z1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   lt(z, z') -{ 0 }-> lt(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   lt(z, z') -{ 0 }-> 2 :|: z0 >= 0, z' = 1 + z0, z = 0
   lt(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 0
   lt(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   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' = 1 + z0, z = 0
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V1, V, V11),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V11),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V11),0,[fun2(V1, V, V11, Out)],[V1 >= 0,V >= 0,V11 >= 0]).
eq(start(V1, V, V11),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V11),0,[minus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V11),0,[lt(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V11),0,[if(V1, V, V11, Out)],[V1 >= 0,V >= 0,V11 >= 0]).
eq(start(V1, V, V11),0,[div(V1, V, Out)],[V1 >= 0,V >= 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,V = 1 + V7,V1 = 0]).
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, V, V11, Out),1,[],[Out = 1,V1 = 2,V12 >= 0,V10 >= 0,V = V10,V11 = V12]).
eq(fun2(V1, V, V11, Out),1,[],[Out = 2,V13 >= 0,V1 = 1,V14 >= 0,V = V14,V11 = V13]).
eq(fun3(V1, V, Out),1,[],[Out = 0,V1 = V15,V15 >= 0,V = 0]).
eq(fun3(V1, V, Out),1,[],[Out = 1,V16 >= 0,V1 = 0,V = V16]).
eq(fun3(V1, V, Out),1,[lt(V18, V17, Ret010),minus(V18, V17, Ret01210),div(Ret01210, 1 + V17, Ret0121),fun2(Ret010, 0, 1 + Ret0121, Ret01),fun1(V18, V17, Ret12)],[Out = 1 + Ret01 + Ret12,V17 >= 0,V1 = 1 + V18,V18 >= 0,V = 1 + V17]).
eq(fun3(V1, V, Out),1,[lt(V20, V19, Ret0010),minus(V20, V19, Ret001210),div(Ret001210, 1 + V19, Ret00121),fun2(Ret0010, 0, 1 + Ret00121, Ret001),minus(V20, V19, Ret0101),fun3(Ret0101, 1 + V19, Ret011),fun(V20, V19, Ret13)],[Out = 1 + Ret001 + Ret011 + Ret13,V19 >= 0,V1 = 1 + V20,V20 >= 0,V = 1 + V19]).
eq(minus(V1, V, Out),0,[],[Out = V21,V1 = V21,V21 >= 0,V = 0]).
eq(minus(V1, V, Out),0,[],[Out = 0,V22 >= 0,V = 1 + V22,V1 = 0]).
eq(minus(V1, V, Out),0,[minus(V24, V23, Ret)],[Out = Ret,V23 >= 0,V1 = 1 + V24,V24 >= 0,V = 1 + V23]).
eq(lt(V1, V, Out),0,[],[Out = 1,V1 = V25,V25 >= 0,V = 0]).
eq(lt(V1, V, Out),0,[],[Out = 2,V26 >= 0,V = 1 + V26,V1 = 0]).
eq(lt(V1, V, Out),0,[lt(V28, V27, Ret2)],[Out = Ret2,V27 >= 0,V1 = 1 + V28,V28 >= 0,V = 1 + V27]).
eq(if(V1, V, V11, Out),0,[],[Out = V30,V1 = 2,V29 >= 0,V30 >= 0,V = V30,V11 = V29]).
eq(if(V1, V, V11, Out),0,[],[Out = V32,V32 >= 0,V1 = 1,V31 >= 0,V = V31,V11 = V32]).
eq(div(V1, V, Out),0,[],[Out = 0,V1 = V33,V33 >= 0,V = 0]).
eq(div(V1, V, Out),0,[],[Out = 0,V34 >= 0,V1 = 0,V = V34]).
eq(div(V1, V, Out),0,[lt(V35, V36, Ret0),minus(V35, V36, Ret210),div(Ret210, 1 + V36, Ret21),if(Ret0, 0, 1 + Ret21, Ret3)],[Out = Ret3,V36 >= 0,V1 = 1 + V35,V35 >= 0,V = 1 + V36]).
eq(minus(V1, V, Out),0,[],[Out = 0,V38 >= 0,V37 >= 0,V1 = V38,V = V37]).
eq(lt(V1, V, Out),0,[],[Out = 0,V40 >= 0,V39 >= 0,V1 = V40,V = V39]).
eq(if(V1, V, V11, Out),0,[],[Out = 0,V42 >= 0,V11 = V43,V41 >= 0,V1 = V42,V = V41,V43 >= 0]).
eq(div(V1, V, Out),0,[],[Out = 0,V44 >= 0,V45 >= 0,V1 = V44,V = V45]).
eq(fun(V1, V, Out),0,[],[Out = 0,V47 >= 0,V46 >= 0,V1 = V47,V = V46]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V49 >= 0,V48 >= 0,V1 = V49,V = V48]).
eq(fun2(V1, V, V11, Out),0,[],[Out = 0,V51 >= 0,V11 = V52,V50 >= 0,V1 = V51,V = V50,V52 >= 0]).
eq(fun3(V1, V, Out),0,[],[Out = 0,V53 >= 0,V54 >= 0,V1 = V53,V = V54]).
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,V,V11,Out),[V1,V,V11],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(minus(V1,V,Out),[V1,V],[Out]).
input_output_vars(lt(V1,V,Out),[V1,V],[Out]).
input_output_vars(if(V1,V,V11,Out),[V1,V,V11],[Out]).
input_output_vars(div(V1,V,Out),[V1,V],[Out]).


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

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

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into if/4
1. SCC is partially evaluated into lt/3
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/4
7. SCC is partially evaluated into fun3/3
8. SCC is partially evaluated into start/3

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

### Specialization of cost equations if/4 
* CE 34 is refined into CE [38] 
* CE 32 is refined into CE [39] 
* CE 33 is refined into CE [40] 


### Cost equations --> "Loop" of if/4 
* CEs [38] --> Loop 27 
* CEs [39] --> Loop 28 
* CEs [40] --> Loop 29 

### Ranking functions of CR if(V1,V,V11,Out) 

#### Partial ranking functions of CR if(V1,V,V11,Out) 


### Specialization of cost equations lt/3 
* CE 31 is refined into CE [41] 
* CE 28 is refined into CE [42] 
* CE 29 is refined into CE [43] 
* CE 30 is refined into CE [44] 


### Cost equations --> "Loop" of lt/3 
* CEs [44] --> Loop 30 
* CEs [41] --> Loop 31 
* CEs [42] --> Loop 32 
* CEs [43] --> Loop 33 

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

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


### Specialization of cost equations minus/3 
* CE 26 is refined into CE [45] 
* CE 25 is refined into CE [46] 
* CE 27 is refined into CE [47] 


### Cost equations --> "Loop" of minus/3 
* CEs [47] --> Loop 34 
* CEs [45] --> Loop 35 
* CEs [46] --> 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 35 is refined into CE [48] 
* CE 36 is refined into CE [49] 
* CE 37 is refined into CE [50,51,52,53,54,55,56,57,58,59,60,61,62,63,64] 


### Cost equations --> "Loop" of (div)/3 
* CEs [61] --> Loop 37 
* CEs [59] --> Loop 38 
* CEs [58,62] --> Loop 39 
* CEs [60] --> Loop 40 
* CEs [52] --> Loop 41 
* CEs [54] --> Loop 42 
* CEs [53,56] --> Loop 43 
* CEs [55] --> Loop 44 
* CEs [50,51,57,63,64] --> Loop 45 
* CEs [48,49] --> Loop 46 

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

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


### Specialization of cost equations fun/3 
* CE 9 is refined into CE [65] 
* CE 12 is refined into CE [66] 
* CE 10 is refined into CE [67] 
* CE 11 is refined into CE [68] 


### Cost equations --> "Loop" of fun/3 
* CEs [68] --> Loop 47 
* CEs [65,66] --> Loop 48 
* CEs [67] --> Loop 49 

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

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


### Specialization of cost equations fun1/3 
* CE 13 is refined into CE [69] 
* CE 16 is refined into CE [70] 
* CE 14 is refined into CE [71] 
* CE 15 is refined into CE [72] 


### Cost equations --> "Loop" of fun1/3 
* CEs [72] --> Loop 50 
* CEs [69,70] --> Loop 51 
* CEs [71] --> Loop 52 

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

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


### Specialization of cost equations fun2/4 
* CE 19 is refined into CE [73] 
* CE 17 is refined into CE [74] 
* CE 18 is refined into CE [75] 


### Cost equations --> "Loop" of fun2/4 
* CEs [73] --> Loop 53 
* CEs [74] --> Loop 54 
* CEs [75] --> Loop 55 

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

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


### Specialization of cost equations fun3/3 
* CE 22 is refined into CE [76,77,78,79,80,81,82,83,84,85,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,111,112,113,114,115,116,117,118,119,120,121,122] 
* CE 20 is refined into CE [123] 
* CE 24 is refined into CE [124] 
* CE 21 is refined into CE [125] 
* CE 23 is refined into CE [126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208] 


### Cost equations --> "Loop" of fun3/3 
* CEs [174,182,190,198] --> Loop 56 
* CEs [158,162,166,170,178,186,194,202] --> Loop 57 
* CEs [173,181,189,197] --> Loop 58 
* CEs [157,161,165,169,177,185,193,201] --> Loop 59 
* CEs [155,205,207] --> Loop 60 
* CEs [204] --> Loop 61 
* CEs [203,208] --> Loop 62 
* CEs [172,180,188,196] --> Loop 63 
* CEs [156,160,164,168,176,184,192,200] --> Loop 64 
* CEs [171,179,187,195] --> Loop 65 
* CEs [159,163,167,175,183,191,199] --> Loop 66 
* CEs [130,134,138,142] --> Loop 67 
* CEs [132,136,140,144,146,148,150,152] --> Loop 68 
* CEs [131,135,139,143] --> Loop 69 
* CEs [133,137,141,145,147,149,151] --> Loop 70 
* CEs [126] --> Loop 71 
* CEs [127,128,153] --> Loop 72 
* CEs [129,154,206] --> Loop 73 
* CEs [102,106,110,114] --> Loop 74 
* CEs [96,98,100,104,108,112,116] --> Loop 75 
* CEs [93,119,121] --> Loop 76 
* CEs [118] --> Loop 77 
* CEs [101,105,109,113] --> Loop 78 
* CEs [94,117,122] --> Loop 79 
* CEs [80,82,84,86] --> Loop 80 
* CEs [81,83,85,87,88,89,90] --> Loop 81 
* CEs [123,124] --> Loop 82 
* CEs [76] --> Loop 83 
* CEs [77,78,91] --> Loop 84 
* CEs [79,92,95,97,99,103,107,111,115,120] --> Loop 85 
* CEs [125] --> Loop 86 

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

#### Partial ranking functions of CR fun3(V1,V,Out) 
* Partial RF of phase [56,57,58,59]:
  - RF of loop [56:1,57:1,58:1,59:1]:
    V1-1
    V1-V+1
* Partial RF of phase [67,68]:
  - RF of loop [67:1,68:1]:
    V1


### Specialization of cost equations start/3 
* CE 1 is refined into CE [209,210,211,212] 
* CE 2 is refined into CE [213,214,215,216] 
* CE 3 is refined into CE [217,218,219] 
* CE 4 is refined into CE [220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238] 
* CE 5 is refined into CE [239,240,241] 
* CE 6 is refined into CE [242,243,244,245,246] 
* CE 7 is refined into CE [247,248,249] 
* CE 8 is refined into CE [250,251,252,253,254] 


### Cost equations --> "Loop" of start/3 
* CEs [224,225,226,227,228,229,250,251] --> Loop 87 
* CEs [239,243] --> Loop 88 
* CEs [218,248] --> Loop 89 
* CEs [222,223] --> Loop 90 
* CEs [217,247] --> Loop 91 
* CEs [209,210,211,212,213,214,215,216,219,220,221,230,231,232,233,234,235,236,237,238,240,241,242,244,245,246,249,252,253,254] --> Loop 92 

### Ranking functions of CR start(V1,V,V11) 

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


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

#### Cost of chains of if(V1,V,V11,Out):
* Chain [29]: 0
  with precondition: [V1=1,V11=Out,V>=0,V11>=0] 

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

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


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

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

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

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

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

* Chain [31]: 0
  with precondition: [Out=0,V1>=0,V>=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 [[41,43],46]: 0
  with precondition: [V=1,V1>=1,Out>=0,V1>=Out] 

* Chain [[41,43],45,46]: 0
  with precondition: [V=1,V1>=2,Out>=0,V1>=Out+1] 

* Chain [[41,43],44,46]: 0
  with precondition: [V=1,V1>=2,Out>=0,V1>=Out+1] 

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

* Chain [[37,39],46]: 0
  with precondition: [V>=2,Out>=0,V1>=V,V1+2>=2*Out+V] 

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

* Chain [[37,39],40,46]: 0
  with precondition: [V>=2,Out>=0,V1>=2*V,V1+2>=2*Out+2*V] 

* Chain [[37,39],38,46]: 0
  with precondition: [V>=2,Out>=0,V1>=2*V,V1+4>=2*Out+2*V] 

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

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

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

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

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

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


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

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

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

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

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

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


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

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

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

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

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

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


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

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

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


#### Cost of chains of fun3(V1,V,Out):
* Chain [[67,68],86]: 5*it(67)+1
  Such that:aux(9) =< V1
it(67) =< aux(9)

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

* Chain [[67,68],85]: 5*it(67)+2
  Such that:aux(10) =< V1
it(67) =< aux(10)

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

* Chain [[67,68],82]: 5*it(67)+1
  Such that:aux(11) =< V1
it(67) =< aux(11)

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

* Chain [[67,68],81]: 5*it(67)+2
  Such that:aux(12) =< V1
it(67) =< aux(12)

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

* Chain [[67,68],80]: 5*it(67)+3
  Such that:aux(13) =< V1
it(67) =< aux(13)

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

* Chain [[67,68],73,86]: 5*it(67)+3
  Such that:aux(14) =< V1
it(67) =< aux(14)

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

* Chain [[67,68],73,82]: 5*it(67)+3
  Such that:aux(15) =< V1
it(67) =< aux(15)

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

* Chain [[67,68],70,86]: 5*it(67)+3
  Such that:aux(16) =< V1
it(67) =< aux(16)

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

* Chain [[67,68],70,82]: 5*it(67)+3
  Such that:aux(17) =< V1
it(67) =< aux(17)

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

* Chain [[67,68],69,86]: 5*it(67)+4
  Such that:aux(18) =< V1
it(67) =< aux(18)

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

* Chain [[67,68],69,82]: 5*it(67)+4
  Such that:aux(19) =< V1
it(67) =< aux(19)

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

* Chain [[56,57,58,59],86]: 10*it(56)+12*s(17)+1
  Such that:aux(23) =< V1-V+1
aux(26) =< V1
it(56) =< aux(26)
it(56) =< aux(23)
s(17) =< aux(26)

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

* Chain [[56,57,58,59],85]: 10*it(56)+12*s(17)+2
  Such that:aux(23) =< V1-V+1
aux(27) =< V1
it(56) =< aux(27)
it(56) =< aux(23)
s(17) =< aux(27)

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

* Chain [[56,57,58,59],84]: 10*it(56)+12*s(17)+3
  Such that:aux(23) =< V1-V+1
aux(28) =< V1
it(56) =< aux(28)
it(56) =< aux(23)
s(17) =< aux(28)

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

* Chain [[56,57,58,59],83]: 10*it(56)+12*s(17)+3
  Such that:aux(23) =< V1-V+1
aux(29) =< V1
it(56) =< aux(29)
it(56) =< aux(23)
s(17) =< aux(29)

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

* Chain [[56,57,58,59],82]: 10*it(56)+12*s(17)+1
  Such that:aux(23) =< V1-V+1
aux(30) =< V1
it(56) =< aux(30)
it(56) =< aux(23)
s(17) =< aux(30)

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

* Chain [[56,57,58,59],79]: 10*it(56)+13*s(17)+1*s(21)+3
  Such that:aux(23) =< V1-V+1
s(21) =< V
aux(31) =< V1
s(17) =< aux(31)
it(56) =< aux(31)
it(56) =< aux(23)

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

* Chain [[56,57,58,59],78]: 10*it(56)+12*s(17)+3
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(32) =< V1-V
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(32)
s(18) =< aux(32)
s(17) =< s(18)

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

* Chain [[56,57,58,59],77]: 10*it(56)+13*s(17)+3
  Such that:aux(23) =< V1-V+1
aux(33) =< V1
s(17) =< aux(33)
it(56) =< aux(33)
it(56) =< aux(23)

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

* Chain [[56,57,58,59],76]: 10*it(56)+15*s(17)+3
  Such that:aux(23) =< V1-V+1
aux(35) =< V1
s(17) =< aux(35)
it(56) =< aux(35)
it(56) =< aux(23)

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

* Chain [[56,57,58,59],75]: 10*it(56)+12*s(17)+7*s(27)+2
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(36) =< V
aux(37) =< V1-V
s(27) =< aux(36)
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(37)
s(18) =< aux(37)
s(17) =< s(18)

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

* Chain [[56,57,58,59],74]: 10*it(56)+12*s(17)+4*s(34)+3
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(38) =< V
aux(39) =< V1-V
s(34) =< aux(38)
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(39)
s(18) =< aux(39)
s(17) =< s(18)

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

* Chain [[56,57,58,59],73,86]: 10*it(56)+12*s(17)+3
  Such that:aux(23) =< V1-V+1
aux(40) =< V1
it(56) =< aux(40)
it(56) =< aux(23)
s(17) =< aux(40)

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

* Chain [[56,57,58,59],73,82]: 10*it(56)+12*s(17)+3
  Such that:aux(23) =< V1-V+1
aux(41) =< V1
it(56) =< aux(41)
it(56) =< aux(23)
s(17) =< aux(41)

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

* Chain [[56,57,58,59],72,86]: 10*it(56)+12*s(17)+4
  Such that:aux(23) =< V1-V+1
aux(42) =< V1
it(56) =< aux(42)
it(56) =< aux(23)
s(17) =< aux(42)

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

* Chain [[56,57,58,59],72,82]: 10*it(56)+12*s(17)+4
  Such that:aux(23) =< V1-V+1
aux(43) =< V1
it(56) =< aux(43)
it(56) =< aux(23)
s(17) =< aux(43)

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

* Chain [[56,57,58,59],71,86]: 10*it(56)+12*s(17)+4
  Such that:aux(23) =< V1-V+1
aux(44) =< V1
it(56) =< aux(44)
it(56) =< aux(23)
s(17) =< aux(44)

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

* Chain [[56,57,58,59],71,82]: 10*it(56)+12*s(17)+4
  Such that:aux(23) =< V1-V+1
aux(45) =< V1
it(56) =< aux(45)
it(56) =< aux(23)
s(17) =< aux(45)

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

* Chain [[56,57,58,59],66,86]: 10*it(56)+12*s(17)+3
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(46) =< V1-V
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(46)
s(18) =< aux(46)
s(17) =< s(18)

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

* Chain [[56,57,58,59],66,82]: 10*it(56)+12*s(17)+3
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(47) =< V1-V
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(47)
s(18) =< aux(47)
s(17) =< s(18)

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

* Chain [[56,57,58,59],65,86]: 10*it(56)+12*s(17)+4
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(48) =< V1-V
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(48)
s(18) =< aux(48)
s(17) =< s(18)

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

* Chain [[56,57,58,59],65,82]: 10*it(56)+12*s(17)+4
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(49) =< V1-V
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(49)
s(18) =< aux(49)
s(17) =< s(18)

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

* Chain [[56,57,58,59],64,86]: 10*it(56)+13*s(17)+7*s(39)+3
  Such that:aux(23) =< V1-V+1
aux(50) =< V
aux(51) =< V1
s(17) =< aux(51)
s(39) =< aux(50)
it(56) =< aux(51)
it(56) =< aux(23)

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

* Chain [[56,57,58,59],64,82]: 10*it(56)+13*s(17)+7*s(39)+3
  Such that:aux(23) =< V1-V+1
aux(50) =< V
aux(52) =< V1
s(17) =< aux(52)
s(39) =< aux(50)
it(56) =< aux(52)
it(56) =< aux(23)

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

* Chain [[56,57,58,59],63,86]: 10*it(56)+12*s(17)+4*s(46)+4
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(53) =< V
aux(54) =< V1-V
s(46) =< aux(53)
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(54)
s(18) =< aux(54)
s(17) =< s(18)

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

* Chain [[56,57,58,59],63,82]: 10*it(56)+12*s(17)+4*s(46)+4
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(53) =< V
aux(55) =< V1-V
s(46) =< aux(53)
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(55)
s(18) =< aux(55)
s(17) =< s(18)

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

* Chain [[56,57,58,59],62,86]: 10*it(56)+13*s(17)+4
  Such that:aux(23) =< V1-V+1
aux(56) =< V1
s(17) =< aux(56)
it(56) =< aux(56)
it(56) =< aux(23)

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

* Chain [[56,57,58,59],62,82]: 10*it(56)+13*s(17)+4
  Such that:aux(23) =< V1-V+1
aux(57) =< V1
s(17) =< aux(57)
it(56) =< aux(57)
it(56) =< aux(23)

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

* Chain [[56,57,58,59],61,86]: 10*it(56)+12*s(17)+1*s(51)+4
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(58) =< V1+3
s(51) =< aux(58)
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(58)
s(18) =< aux(58)
s(17) =< s(18)

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

* Chain [[56,57,58,59],61,82]: 10*it(56)+12*s(17)+1*s(51)+4
  Such that:aux(22) =< V1
aux(23) =< V1-V+1
aux(59) =< V1+2
s(51) =< aux(59)
it(56) =< aux(22)
s(18) =< aux(22)
it(56) =< aux(23)
it(56) =< aux(59)
s(18) =< aux(59)
s(17) =< s(18)

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

* Chain [[56,57,58,59],60,86]: 10*it(56)+15*s(17)+4
  Such that:aux(23) =< V1-V+1
aux(61) =< V1
s(17) =< aux(61)
it(56) =< aux(61)
it(56) =< aux(23)

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

* Chain [[56,57,58,59],60,82]: 10*it(56)+15*s(17)+4
  Such that:aux(23) =< V1-V+1
aux(62) =< V1
s(17) =< aux(62)
it(56) =< aux(62)
it(56) =< aux(23)

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

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

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

* Chain [84]: 3
  with precondition: [V1=1,Out=2,V>=2] 

* Chain [83]: 3
  with precondition: [V1=1,Out=3,V>=2] 

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

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

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

* Chain [79]: 1*s(21)+1*s(22)+3
  Such that:s(22) =< V1
s(21) =< V

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

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

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

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

* Chain [76]: 3*s(24)+3
  Such that:aux(34) =< V1
s(24) =< aux(34)

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

* Chain [75]: 7*s(27)+2
  Such that:aux(36) =< V
s(27) =< aux(36)

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

* Chain [74]: 4*s(34)+3
  Such that:aux(38) =< V
s(34) =< aux(38)

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

* Chain [73,86]: 3
  with precondition: [Out=2,V1>=1,V>=1] 

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

* Chain [72,86]: 4
  with precondition: [V1=1,Out=3,V>=2] 

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

* Chain [71,86]: 4
  with precondition: [V1=1,Out=4,V>=2] 

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

* Chain [70,86]: 3
  with precondition: [V=1,Out=2,V1>=1] 

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

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

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

* Chain [66,86]: 3
  with precondition: [Out=2,V>=2,V1>=V] 

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

* Chain [65,86]: 4
  with precondition: [Out=4,V>=2,V1>=V] 

* Chain [65,82]: 4
  with precondition: [Out=3,V>=2,V1>=V] 

* Chain [64,86]: 1*s(38)+7*s(39)+3
  Such that:s(38) =< V1
aux(50) =< V
s(39) =< aux(50)

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

* Chain [64,82]: 1*s(38)+7*s(39)+3
  Such that:s(38) =< V1
aux(50) =< V
s(39) =< aux(50)

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

* Chain [63,86]: 4*s(46)+4
  Such that:aux(53) =< V
s(46) =< aux(53)

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

* Chain [63,82]: 4*s(46)+4
  Such that:aux(53) =< V
s(46) =< aux(53)

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

* Chain [62,86]: 1*s(50)+4
  Such that:s(50) =< V1

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

* Chain [62,82]: 1*s(50)+4
  Such that:s(50) =< V1

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

* Chain [61,86]: 1*s(51)+4
  Such that:s(51) =< Out

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

* Chain [61,82]: 1*s(51)+4
  Such that:s(51) =< Out

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

* Chain [60,86]: 3*s(52)+4
  Such that:aux(60) =< V1
s(52) =< aux(60)

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

* Chain [60,82]: 3*s(52)+4
  Such that:aux(60) =< V1
s(52) =< aux(60)

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


#### Cost of chains of start(V1,V,V11):
* Chain [92]: 2*s(256)+70*s(257)+2*s(266)+10*s(267)+12*s(269)+90*s(270)+108*s(272)+270*s(273)+200*s(274)+2*s(280)+10*s(281)+12*s(283)+4
  Such that:aux(75) =< V1
aux(76) =< V1+1
aux(77) =< V1+2
aux(78) =< V1+3
aux(79) =< V1-V
aux(80) =< V1-V+1
aux(81) =< V
s(256) =< aux(76)
s(266) =< aux(77)
s(280) =< aux(78)
s(257) =< aux(81)
s(267) =< aux(75)
s(268) =< aux(75)
s(267) =< aux(80)
s(267) =< aux(77)
s(268) =< aux(77)
s(269) =< s(268)
s(270) =< aux(75)
s(271) =< aux(75)
s(270) =< aux(80)
s(270) =< aux(79)
s(271) =< aux(79)
s(272) =< s(271)
s(273) =< aux(75)
s(274) =< aux(75)
s(274) =< aux(80)
s(281) =< aux(75)
s(282) =< aux(75)
s(281) =< aux(80)
s(281) =< aux(78)
s(282) =< aux(78)
s(283) =< s(282)

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

* Chain [91]: 1
  with precondition: [V1=1,V>=0,V11>=0] 

* Chain [90]: 4
  with precondition: [V1=1,V>=2] 

* Chain [89]: 1
  with precondition: [V1=2,V>=0,V11>=0] 

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

* Chain [87]: 55*s(307)+4
  Such that:aux(82) =< V1
s(307) =< aux(82)

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


Closed-form bounds of start(V1,V,V11): 
-------------------------------------
* Chain [92] with precondition: [V1>=0,V>=0] 
    - Upper bound: 718*V1+70*V+16 
    - Complexity: n 
* Chain [91] with precondition: [V1=1,V>=0,V11>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [90] with precondition: [V1=1,V>=2] 
    - Upper bound: 4 
    - Complexity: constant 
* Chain [89] with precondition: [V1=2,V>=0,V11>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [88] with precondition: [V=0,V1>=0] 
    - Upper bound: 0 
    - Complexity: constant 
* Chain [87] with precondition: [V=1,V1>=1] 
    - Upper bound: 55*V1+4 
    - Complexity: n 

### Maximum cost of start(V1,V,V11): 718*V1+70*V+16 
Asymptotic class: n 
* Total analysis performed in 3199 ms.


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

(14)
BOUNDS(1, n^1)

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

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

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

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(0, s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   LT(z0, 0) -> c3
   LT(0, s(z0)) -> c4
   LT(s(z0), s(z1)) -> c5(LT(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   DIV(z0, 0) -> c8
   DIV(0, z0) -> c9
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), LT(z0, z1))
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), DIV(-(z0, z1), s(z1)), -'(z0, z1))

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

   -(z0, 0) -> z0
   -(0, s(z0)) -> 0
   -(s(z0), s(z1)) -> -(z0, z1)
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   div(z0, 0) -> 0
   div(0, z0) -> 0
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(-(z0, z1), s(z1))))

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

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

The rewrite sequence

-'(s(z0), s(z1)) ->^+ c2(-'(z0, z1))

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

The pumping substitution is [z0 / s(z0), z1 / s(z1)].

The result substitution is [ ].




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

(18)
Complex Obligation (BEST)

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

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

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(0, s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   LT(z0, 0) -> c3
   LT(0, s(z0)) -> c4
   LT(s(z0), s(z1)) -> c5(LT(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   DIV(z0, 0) -> c8
   DIV(0, z0) -> c9
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), LT(z0, z1))
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), DIV(-(z0, z1), s(z1)), -'(z0, z1))

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

   -(z0, 0) -> z0
   -(0, s(z0)) -> 0
   -(s(z0), s(z1)) -> -(z0, z1)
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   div(z0, 0) -> 0
   div(0, z0) -> 0
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(-(z0, z1), s(z1))))

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

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

(21)
BOUNDS(n^1, INF)

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

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

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(0, s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   LT(z0, 0) -> c3
   LT(0, s(z0)) -> c4
   LT(s(z0), s(z1)) -> c5(LT(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   DIV(z0, 0) -> c8
   DIV(0, z0) -> c9
   DIV(s(z0), s(z1)) -> c10(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), LT(z0, z1))
   DIV(s(z0), s(z1)) -> c11(IF(lt(z0, z1), 0, s(div(-(z0, z1), s(z1)))), DIV(-(z0, z1), s(z1)), -'(z0, z1))

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

   -(z0, 0) -> z0
   -(0, s(z0)) -> 0
   -(s(z0), s(z1)) -> -(z0, z1)
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   div(z0, 0) -> 0
   div(0, z0) -> 0
   div(s(z0), s(z1)) -> if(lt(z0, z1), 0, s(div(-(z0, z1), s(z1))))

Rewrite Strategy: INNERMOST