WORST_CASE(Omega(n^1),O(n^1))
proof of input_0n2AZpWoUl.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxWeightedTrs
    (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxTypedWeightedTrs
    (15) CompletionProof [UPPER BOUND(ID), 0 ms]
    (16) CpxTypedWeightedCompleteTrs
    (17) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (18) CpxRNTS
    (19) CompleteCoflocoProof [FINISHED, 2548 ms]
    (20) BOUNDS(1, n^1)
(21) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(22) CdtProblem
    (23) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) CpxRelTRS
    (27) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) typed CpxTrs
    (29) OrderProof [LOWER BOUND(ID), 4 ms]
    (30) typed CpxTrs
    (31) RewriteLemmaProof [LOWER BOUND(ID), 1335 ms]
    (32) typed CpxTrs
    (33) RewriteLemmaProof [LOWER BOUND(ID), 1073 ms]
    (34) BEST
        (35) proven lower bound
            (36) LowerBoundPropagationProof [FINISHED, 0 ms]
            (37) BOUNDS(n^1, INF)
        (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 48 ms]
            (40) typed CpxTrs


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

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


The TRS R consists of the following rules:

   minus(X, s(Y)) -> pred(minus(X, Y))
   minus(X, 0) -> X
   pred(s(X)) -> X
   le(s(X), s(Y)) -> le(X, Y)
   le(s(X), 0) -> false
   le(0, Y) -> true
   gcd(0, Y) -> 0
   gcd(s(X), 0) -> s(X)
   gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y))
   if(true, s(X), s(Y)) -> gcd(minus(X, Y), s(Y))
   if(false, s(X), s(Y)) -> gcd(minus(Y, X), s(X))

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, s(z1)) -> pred(minus(z0, z1))
   minus(z0, 0) -> z0
   pred(s(z0)) -> z0
   le(s(z0), s(z1)) -> le(z0, z1)
   le(s(z0), 0) -> false
   le(0, z0) -> true
   gcd(0, z0) -> 0
   gcd(s(z0), 0) -> s(z0)
   gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
   if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
   if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))
Tuples:
   MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
   MINUS(z0, 0) -> c1
   PRED(s(z0)) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   LE(s(z0), 0) -> c4
   LE(0, z0) -> c5
   GCD(0, z0) -> c6
   GCD(s(z0), 0) -> c7
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
S tuples:
   MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
   MINUS(z0, 0) -> c1
   PRED(s(z0)) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   LE(s(z0), 0) -> c4
   LE(0, z0) -> c5
   GCD(0, z0) -> c6
   GCD(s(z0), 0) -> c7
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
K tuples:none
Defined Rule Symbols:   minus_2, pred_1, le_2, gcd_2, if_3

Defined Pair Symbols:   MINUS_2, PRED_1, LE_2, GCD_2, IF_3

Compound Symbols:   c_2, c1, c2, c3_1, c4, c5, c6, c7, c8_2, c9_2, c10_2


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 6 trailing nodes:
   MINUS(z0, 0) -> c1
   LE(s(z0), 0) -> c4
   PRED(s(z0)) -> c2
   GCD(s(z0), 0) -> c7
   GCD(0, z0) -> c6
   LE(0, z0) -> c5

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, s(z1)) -> pred(minus(z0, z1))
   minus(z0, 0) -> z0
   pred(s(z0)) -> z0
   le(s(z0), s(z1)) -> le(z0, z1)
   le(s(z0), 0) -> false
   le(0, z0) -> true
   gcd(0, z0) -> 0
   gcd(s(z0), 0) -> s(z0)
   gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
   if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
   if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))
Tuples:
   MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
S tuples:
   MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
K tuples:none
Defined Rule Symbols:   minus_2, pred_1, le_2, gcd_2, if_3

Defined Pair Symbols:   MINUS_2, LE_2, GCD_2, IF_3

Compound Symbols:   c_2, c3_1, c8_2, c9_2, c10_2


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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, s(z1)) -> pred(minus(z0, z1))
   minus(z0, 0) -> z0
   pred(s(z0)) -> z0
   le(s(z0), s(z1)) -> le(z0, z1)
   le(s(z0), 0) -> false
   le(0, z0) -> true
   gcd(0, z0) -> 0
   gcd(s(z0), 0) -> s(z0)
   gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
   if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
   if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))
Tuples:
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
   MINUS(z0, s(z1)) -> c(MINUS(z0, z1))
S tuples:
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
   MINUS(z0, s(z1)) -> c(MINUS(z0, z1))
K tuples:none
Defined Rule Symbols:   minus_2, pred_1, le_2, gcd_2, if_3

Defined Pair Symbols:   LE_2, GCD_2, IF_3, MINUS_2

Compound Symbols:   c3_1, c8_2, c9_2, c10_2, c_1


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   gcd(0, z0) -> 0
   gcd(s(z0), 0) -> s(z0)
   gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
   if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
   if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(s(z0), s(z1)) -> le(z0, z1)
   le(s(z0), 0) -> false
   le(0, z0) -> true
   minus(z0, s(z1)) -> pred(minus(z0, z1))
   minus(z0, 0) -> z0
   pred(s(z0)) -> z0
Tuples:
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
   MINUS(z0, s(z1)) -> c(MINUS(z0, z1))
S tuples:
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
   MINUS(z0, s(z1)) -> c(MINUS(z0, z1))
K tuples:none
Defined Rule Symbols:   le_2, minus_2, pred_1

Defined Pair Symbols:   LE_2, GCD_2, IF_3, MINUS_2

Compound Symbols:   c3_1, c8_2, c9_2, c10_2, c_1


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

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

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


The TRS R consists of the following rules:

   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
   MINUS(z0, s(z1)) -> c(MINUS(z0, z1))

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

   le(s(z0), s(z1)) -> le(z0, z1)
   le(s(z0), 0) -> false
   le(0, z0) -> true
   minus(z0, s(z1)) -> pred(minus(z0, z1))
   minus(z0, 0) -> z0
   pred(s(z0)) -> z0

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

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

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


The TRS R consists of the following rules:

   LE(s(z0), s(z1)) -> c3(LE(z0, z1)) [1]
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0)) [1]
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0)) [1]
   MINUS(z0, s(z1)) -> c(MINUS(z0, z1)) [1]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   le(s(z0), 0) -> false [0]
   le(0, z0) -> true [0]
   minus(z0, s(z1)) -> pred(minus(z0, z1)) [0]
   minus(z0, 0) -> z0 [0]
   pred(s(z0)) -> z0 [0]

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

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

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

   LE(s(z0), s(z1)) -> c3(LE(z0, z1)) [1]
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0)) [1]
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0)) [1]
   MINUS(z0, s(z1)) -> c(MINUS(z0, z1)) [1]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   le(s(z0), 0) -> false [0]
   le(0, z0) -> true [0]
   minus(z0, s(z1)) -> pred(minus(z0, z1)) [0]
   minus(z0, 0) -> z0 [0]
   pred(s(z0)) -> z0 [0]

The TRS has the following type information:
LE :: s:0 -> s:0 -> c3
s :: s:0 -> s:0
c3 :: c3 -> c3
GCD :: s:0 -> s:0 -> c8
c8 :: c9:c10 -> c3 -> c8
IF :: true:false -> s:0 -> s:0 -> c9:c10
le :: s:0 -> s:0 -> true:false
true :: true:false
c9 :: c8 -> c -> c9:c10
minus :: s:0 -> s:0 -> s:0
MINUS :: s:0 -> s:0 -> c
false :: true:false
c10 :: c8 -> c -> c9:c10
c :: c -> c
0 :: s:0
pred :: s:0 -> s:0

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

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

   le(v0, v1) -> null_le [0]
   minus(v0, v1) -> null_minus [0]
   pred(v0) -> null_pred [0]
   LE(v0, v1) -> null_LE [0]
   GCD(v0, v1) -> null_GCD [0]
   IF(v0, v1, v2) -> null_IF [0]
   MINUS(v0, v1) -> null_MINUS [0]

And the following fresh constants:    null_le, null_minus, null_pred, null_LE, null_GCD, null_IF, null_MINUS

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

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

   LE(s(z0), s(z1)) -> c3(LE(z0, z1)) [1]
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0)) [1]
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0)) [1]
   MINUS(z0, s(z1)) -> c(MINUS(z0, z1)) [1]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   le(s(z0), 0) -> false [0]
   le(0, z0) -> true [0]
   minus(z0, s(z1)) -> pred(minus(z0, z1)) [0]
   minus(z0, 0) -> z0 [0]
   pred(s(z0)) -> z0 [0]
   le(v0, v1) -> null_le [0]
   minus(v0, v1) -> null_minus [0]
   pred(v0) -> null_pred [0]
   LE(v0, v1) -> null_LE [0]
   GCD(v0, v1) -> null_GCD [0]
   IF(v0, v1, v2) -> null_IF [0]
   MINUS(v0, v1) -> null_MINUS [0]

The TRS has the following type information:
LE :: s:0:null_minus:null_pred -> s:0:null_minus:null_pred -> c3:null_LE
s :: s:0:null_minus:null_pred -> s:0:null_minus:null_pred
c3 :: c3:null_LE -> c3:null_LE
GCD :: s:0:null_minus:null_pred -> s:0:null_minus:null_pred -> c8:null_GCD
c8 :: c9:c10:null_IF -> c3:null_LE -> c8:null_GCD
IF :: true:false:null_le -> s:0:null_minus:null_pred -> s:0:null_minus:null_pred -> c9:c10:null_IF
le :: s:0:null_minus:null_pred -> s:0:null_minus:null_pred -> true:false:null_le
true :: true:false:null_le
c9 :: c8:null_GCD -> c:null_MINUS -> c9:c10:null_IF
minus :: s:0:null_minus:null_pred -> s:0:null_minus:null_pred -> s:0:null_minus:null_pred
MINUS :: s:0:null_minus:null_pred -> s:0:null_minus:null_pred -> c:null_MINUS
false :: true:false:null_le
c10 :: c8:null_GCD -> c:null_MINUS -> c9:c10:null_IF
c :: c:null_MINUS -> c:null_MINUS
0 :: s:0:null_minus:null_pred
pred :: s:0:null_minus:null_pred -> s:0:null_minus:null_pred
null_le :: true:false:null_le
null_minus :: s:0:null_minus:null_pred
null_pred :: s:0:null_minus:null_pred
null_LE :: c3:null_LE
null_GCD :: c8:null_GCD
null_IF :: c9:c10:null_IF
null_MINUS :: c:null_MINUS

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

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

   true => 2
   false => 1
   0 => 0
   null_le => 0
   null_minus => 0
   null_pred => 0
   null_LE => 0
   null_GCD => 0
   null_IF => 0
   null_MINUS => 0

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

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

   GCD(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   GCD(z, z') -{ 1 }-> 1 + IF(le(z1, z0), 1 + z0, 1 + z1) + LE(z1, z0) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   IF(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + GCD(minus(z0, z1), 1 + z1) + MINUS(z0, z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = 1 + z0, z'' = 1 + z1
   IF(z, z', z'') -{ 1 }-> 1 + GCD(minus(z1, z0), 1 + z0) + MINUS(z1, z0) :|: z1 >= 0, z = 1, z0 >= 0, z' = 1 + z0, z'' = 1 + z1
   LE(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LE(z, z') -{ 1 }-> 1 + LE(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   MINUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   le(z, z') -{ 0 }-> le(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   le(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   le(z, z') -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   le(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 }-> pred(minus(z0, z1)) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   pred(z) -{ 0 }-> z0 :|: z = 1 + z0, z0 >= 0
   pred(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V1, V, V6),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[fun2(V1, V, V6, Out)],[V1 >= 0,V >= 0,V6 >= 0]).
eq(start(V1, V, V6),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[le(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[minus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[pred(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[fun(V3, V2, Ret1)],[Out = 1 + Ret1,V2 >= 0,V1 = 1 + V3,V3 >= 0,V = 1 + V2]).
eq(fun1(V1, V, Out),1,[le(V4, V5, Ret010),fun2(Ret010, 1 + V5, 1 + V4, Ret01),fun(V4, V5, Ret11)],[Out = 1 + Ret01 + Ret11,V4 >= 0,V1 = 1 + V5,V5 >= 0,V = 1 + V4]).
eq(fun2(V1, V, V6, Out),1,[minus(V8, V7, Ret0101),fun1(Ret0101, 1 + V7, Ret011),fun3(V8, V7, Ret12)],[Out = 1 + Ret011 + Ret12,V1 = 2,V7 >= 0,V8 >= 0,V = 1 + V8,V6 = 1 + V7]).
eq(fun2(V1, V, V6, Out),1,[minus(V10, V9, Ret0102),fun1(Ret0102, 1 + V9, Ret012),fun3(V10, V9, Ret13)],[Out = 1 + Ret012 + Ret13,V10 >= 0,V1 = 1,V9 >= 0,V = 1 + V9,V6 = 1 + V10]).
eq(fun3(V1, V, Out),1,[fun3(V12, V11, Ret14)],[Out = 1 + Ret14,V1 = V12,V11 >= 0,V12 >= 0,V = 1 + V11]).
eq(le(V1, V, Out),0,[le(V14, V13, Ret)],[Out = Ret,V13 >= 0,V1 = 1 + V14,V14 >= 0,V = 1 + V13]).
eq(le(V1, V, Out),0,[],[Out = 1,V1 = 1 + V15,V15 >= 0,V = 0]).
eq(le(V1, V, Out),0,[],[Out = 2,V16 >= 0,V1 = 0,V = V16]).
eq(minus(V1, V, Out),0,[minus(V18, V17, Ret0),pred(Ret0, Ret2)],[Out = Ret2,V1 = V18,V17 >= 0,V18 >= 0,V = 1 + V17]).
eq(minus(V1, V, Out),0,[],[Out = V19,V1 = V19,V19 >= 0,V = 0]).
eq(pred(V1, Out),0,[],[Out = V20,V1 = 1 + V20,V20 >= 0]).
eq(le(V1, V, Out),0,[],[Out = 0,V22 >= 0,V21 >= 0,V1 = V22,V = V21]).
eq(minus(V1, V, Out),0,[],[Out = 0,V24 >= 0,V23 >= 0,V1 = V24,V = V23]).
eq(pred(V1, Out),0,[],[Out = 0,V25 >= 0,V1 = V25]).
eq(fun(V1, V, Out),0,[],[Out = 0,V26 >= 0,V27 >= 0,V1 = V26,V = V27]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V28 >= 0,V29 >= 0,V1 = V28,V = V29]).
eq(fun2(V1, V, V6, Out),0,[],[Out = 0,V31 >= 0,V6 = V32,V30 >= 0,V1 = V31,V = V30,V32 >= 0]).
eq(fun3(V1, V, Out),0,[],[Out = 0,V34 >= 0,V33 >= 0,V1 = V34,V = V33]).
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,V6,Out),[V1,V,V6],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(le(V1,V,Out),[V1,V],[Out]).
input_output_vars(minus(V1,V,Out),[V1,V],[Out]).
input_output_vars(pred(V1,Out),[V1],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [fun/3]
1. recursive  : [fun3/3]
2. non_recursive  : [pred/2]
3. recursive [non_tail] : [minus/3]
4. recursive  : [le/3]
5. recursive [non_tail] : [fun1/3,fun2/4]
6. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/3
1. SCC is partially evaluated into fun3/3
2. SCC is partially evaluated into pred/2
3. SCC is partially evaluated into minus/3
4. SCC is partially evaluated into le/3
5. SCC is partially evaluated into fun1/3
6. SCC is partially evaluated into start/3

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

### Specialization of cost equations fun/3 
* CE 20 is refined into CE [27] 
* CE 19 is refined into CE [28] 


### Cost equations --> "Loop" of fun/3 
* CEs [28] --> Loop 20 
* CEs [27] --> Loop 21 

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

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


### Specialization of cost equations fun3/3 
* CE 18 is refined into CE [29] 
* CE 17 is refined into CE [30] 


### Cost equations --> "Loop" of fun3/3 
* CEs [30] --> Loop 22 
* CEs [29] --> Loop 23 

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

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


### Specialization of cost equations pred/2 
* CE 25 is refined into CE [31] 
* CE 26 is refined into CE [32] 


### Cost equations --> "Loop" of pred/2 
* CEs [31] --> Loop 24 
* CEs [32] --> Loop 25 

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

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


### Specialization of cost equations minus/3 
* CE 12 is refined into CE [33] 
* CE 11 is refined into CE [34] 
* CE 10 is refined into CE [35,36] 


### Cost equations --> "Loop" of minus/3 
* CEs [36] --> Loop 26 
* CEs [35] --> Loop 27 
* CEs [33] --> Loop 28 
* CEs [34] --> Loop 29 

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

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


### Specialization of cost equations le/3 
* CE 24 is refined into CE [37] 
* CE 22 is refined into CE [38] 
* CE 23 is refined into CE [39] 
* CE 21 is refined into CE [40] 


### Cost equations --> "Loop" of le/3 
* CEs [40] --> Loop 30 
* CEs [37] --> Loop 31 
* CEs [38] --> Loop 32 
* CEs [39] --> Loop 33 

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

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


### Specialization of cost equations fun1/3 
* CE 13 is refined into CE [41,42,43,44,45,46,47,48] 
* CE 16 is refined into CE [49] 
* CE 15 is refined into CE [50,51,52,53,54,55,56,57,58,59] 
* CE 14 is refined into CE [60,61,62,63,64,65,66,67,68,69] 


### Cost equations --> "Loop" of fun1/3 
* CEs [69] --> Loop 34 
* CEs [67,68] --> Loop 35 
* CEs [66] --> Loop 36 
* CEs [57,58] --> Loop 37 
* CEs [59] --> Loop 38 
* CEs [56] --> Loop 39 
* CEs [65] --> Loop 40 
* CEs [63,64] --> Loop 41 
* CEs [62] --> Loop 42 
* CEs [55] --> Loop 43 
* CEs [53,54] --> Loop 44 
* CEs [52] --> Loop 45 
* CEs [50] --> Loop 46 
* CEs [51] --> Loop 47 
* CEs [60] --> Loop 48 
* CEs [61] --> Loop 49 
* CEs [48] --> Loop 50 
* CEs [44,46] --> Loop 51 
* CEs [49] --> Loop 52 
* CEs [41] --> Loop 53 
* CEs [42,43,45,47] --> Loop 54 

### Ranking functions of CR fun1(V1,V,Out) 
* RF of phase [34,35,36,37,38,39]: [V1+V-3]
* RF of phase [46]: [V1]

#### Partial ranking functions of CR fun1(V1,V,Out) 
* Partial RF of phase [34,35,36,37,38,39]:
  - RF of loop [34:1,35:1,36:1]:
    V-2
    V1/2+V/2-2
  - RF of loop [37:1,38:1,39:1]:
    V1-1 depends on loops [34:1,35:1,36:1] 
    V1-V+1 depends on loops [34:1,35:1,36:1] 
* Partial RF of phase [46]:
  - RF of loop [46:1]:
    V1


### Specialization of cost equations start/3 
* CE 3 is refined into CE [70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92] 
* CE 1 is refined into CE [93] 
* CE 2 is refined into CE [94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116] 
* CE 4 is refined into CE [117,118] 
* CE 5 is refined into CE [119,120,121,122,123,124,125,126,127,128] 
* CE 6 is refined into CE [129,130] 
* CE 7 is refined into CE [131,132,133,134,135] 
* CE 8 is refined into CE [136,137,138] 
* CE 9 is refined into CE [139,140] 


### Cost equations --> "Loop" of start/3 
* CEs [123] --> Loop 55 
* CEs [132,136] --> Loop 56 
* CEs [75,76,77,78,79,80] --> Loop 57 
* CEs [70,71,72,73,74,81,82,83,84,85,86,87,88,89,90,91,92] --> Loop 58 
* CEs [99,100,101,102,103,104,119,120,121] --> Loop 59 
* CEs [94,95,96,97,98,105,106,107,108,109,110,111,112,113,114,115,116] --> Loop 60 
* CEs [93,117,118,122,124,125,126,127,128,129,130,131,133,134,135,137,138,139,140] --> Loop 61 

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

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


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

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

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

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


#### Cost of chains of fun3(V1,V,Out):
* Chain [[22],23]: 1*it(22)+0
  Such that:it(22) =< Out

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

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


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

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


#### Cost of chains of minus(V1,V,Out):
* Chain [[27],[26],29]: 0
  with precondition: [Out=0,V1>=1,V>=2] 

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

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

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

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

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


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

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

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

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

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

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


#### Cost of chains of fun1(V1,V,Out):
* Chain [[46],54]: 2*it(46)+1
  Such that:it(46) =< Out/2

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

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

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

* Chain [[46],52]: 2*it(46)+0
  Such that:it(46) =< Out/2

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

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

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

* Chain [[34,35,36,37,38,39],54]: 6*it(34)+6*it(37)+8*s(17)+1
  Such that:aux(27) =< V1-V+1
aux(39) =< V1
aux(40) =< V1+V
aux(41) =< V1/2+V/2
aux(42) =< V
aux(43) =< 2*V
aux(44) =< 3/2*V
it(34) =< aux(40)
it(37) =< aux(40)
it(34) =< aux(41)
it(37) =< aux(41)
it(34) =< aux(42)
aux(10) =< aux(43)
aux(10) =< aux(44)
it(37) =< aux(10)+aux(10)+aux(44)+aux(27)
it(37) =< aux(43)+aux(43)+aux(43)+aux(39)
s(17) =< aux(40)

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

* Chain [[34,35,36,37,38,39],52]: 6*it(34)+6*it(37)+8*s(17)+0
  Such that:aux(27) =< V1-V+1
aux(45) =< V1
aux(46) =< V1+V
aux(47) =< V1/2+V/2
aux(48) =< V
aux(49) =< 2*V
aux(50) =< 3/2*V
it(34) =< aux(46)
it(37) =< aux(46)
it(34) =< aux(47)
it(37) =< aux(47)
it(34) =< aux(48)
aux(10) =< aux(49)
aux(10) =< aux(50)
it(37) =< aux(10)+aux(10)+aux(50)+aux(27)
it(37) =< aux(49)+aux(49)+aux(49)+aux(45)
s(17) =< aux(46)

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

* Chain [[34,35,36,37,38,39],51]: 6*it(34)+6*it(37)+10*s(17)+1
  Such that:aux(27) =< V1-V+1
aux(31) =< V1/2+V/2
aux(38) =< 3*V
aux(37) =< 3/2*V
aux(51) =< V1
aux(52) =< V1+V
aux(53) =< V
aux(54) =< 2*V
s(17) =< aux(52)
it(34) =< aux(52)
it(37) =< aux(52)
it(34) =< aux(31)
it(34) =< aux(53)
aux(10) =< aux(54)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(38)
aux(10) =< aux(38)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(54)+aux(54)+aux(54)+aux(51)

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

* Chain [[34,35,36,37,38,39],50]: 6*it(34)+6*it(37)+8*s(17)+1*s(27)+1
  Such that:aux(27) =< V1-V+1
aux(37) =< 3/2*V
aux(55) =< V1
aux(56) =< V1+V
aux(57) =< V1/2+V/2
aux(58) =< V
aux(59) =< 2*V
aux(60) =< 3*V
s(27) =< aux(60)
it(34) =< aux(56)
it(37) =< aux(56)
it(34) =< aux(57)
it(37) =< aux(57)
it(34) =< aux(58)
aux(10) =< aux(59)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(60)
aux(10) =< aux(60)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(59)+aux(59)+aux(59)+aux(55)
s(17) =< aux(56)

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

* Chain [[34,35,36,37,38,39],49,52]: 6*it(34)+6*it(37)+8*s(17)+2
  Such that:aux(27) =< V1-V+1
aux(61) =< V1
aux(62) =< V1+V
aux(63) =< V1/2+V/2
aux(64) =< V
aux(65) =< 2*V
aux(66) =< 3/2*V
it(34) =< aux(62)
it(37) =< aux(62)
it(34) =< aux(63)
it(37) =< aux(63)
it(34) =< aux(64)
aux(10) =< aux(65)
aux(10) =< aux(66)
it(37) =< aux(10)+aux(10)+aux(66)+aux(27)
it(37) =< aux(65)+aux(65)+aux(65)+aux(61)
s(17) =< aux(62)

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

* Chain [[34,35,36,37,38,39],48,[46],54]: 6*it(34)+6*it(37)+2*it(46)+8*s(17)+3
  Such that:aux(27) =< V1-V+1
aux(31) =< V1/2+V/2
aux(37) =< 3/2*V
aux(67) =< V1
aux(68) =< V1+V
aux(69) =< V
aux(70) =< 2*V
aux(71) =< 3*V
it(46) =< aux(71)
it(34) =< aux(68)
it(37) =< aux(68)
it(34) =< aux(31)
it(34) =< aux(69)
aux(10) =< aux(70)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(71)
aux(10) =< aux(71)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(70)+aux(70)+aux(70)+aux(67)
s(17) =< aux(68)

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

* Chain [[34,35,36,37,38,39],48,[46],53]: 6*it(34)+6*it(37)+2*it(46)+8*s(17)+3
  Such that:aux(27) =< V1-V+1
aux(31) =< V1/2+V/2
aux(37) =< 3/2*V
aux(72) =< V1
aux(73) =< V1+V
aux(74) =< V
aux(75) =< 2*V
aux(76) =< 3*V
it(46) =< aux(76)
it(34) =< aux(73)
it(37) =< aux(73)
it(34) =< aux(31)
it(34) =< aux(74)
aux(10) =< aux(75)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(76)
aux(10) =< aux(76)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(75)+aux(75)+aux(75)+aux(72)
s(17) =< aux(73)

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

* Chain [[34,35,36,37,38,39],48,[46],52]: 6*it(34)+6*it(37)+2*it(46)+8*s(17)+2
  Such that:aux(27) =< V1-V+1
aux(31) =< V1/2+V/2
aux(37) =< 3/2*V
aux(77) =< V1
aux(78) =< V1+V
aux(79) =< V
aux(80) =< 2*V
aux(81) =< 3*V
it(46) =< aux(81)
it(34) =< aux(78)
it(37) =< aux(78)
it(34) =< aux(31)
it(34) =< aux(79)
aux(10) =< aux(80)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(81)
aux(10) =< aux(81)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(80)+aux(80)+aux(80)+aux(77)
s(17) =< aux(78)

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

* Chain [[34,35,36,37,38,39],48,[46],47,52]: 6*it(34)+6*it(37)+2*it(46)+8*s(17)+4
  Such that:aux(27) =< V1-V+1
aux(31) =< V1/2+V/2
aux(37) =< 3/2*V
aux(82) =< V1
aux(83) =< V1+V
aux(84) =< V
aux(85) =< 2*V
aux(86) =< 3*V
it(46) =< aux(86)
it(34) =< aux(83)
it(37) =< aux(83)
it(34) =< aux(31)
it(34) =< aux(84)
aux(10) =< aux(85)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(86)
aux(10) =< aux(86)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(85)+aux(85)+aux(85)+aux(82)
s(17) =< aux(83)

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

* Chain [[34,35,36,37,38,39],48,54]: 6*it(34)+6*it(37)+8*s(17)+3
  Such that:aux(27) =< V1-V+1
aux(87) =< V1
aux(88) =< V1+V
aux(89) =< V1/2+V/2
aux(90) =< V
aux(91) =< 2*V
aux(92) =< 3/2*V
it(34) =< aux(88)
it(37) =< aux(88)
it(34) =< aux(89)
it(37) =< aux(89)
it(34) =< aux(90)
aux(10) =< aux(91)
aux(10) =< aux(92)
it(37) =< aux(10)+aux(10)+aux(92)+aux(27)
it(37) =< aux(91)+aux(91)+aux(91)+aux(87)
s(17) =< aux(88)

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

* Chain [[34,35,36,37,38,39],48,53]: 6*it(34)+6*it(37)+8*s(17)+3
  Such that:aux(27) =< V1-V+1
aux(93) =< V1
aux(94) =< V1+V
aux(95) =< V1/2+V/2
aux(96) =< V
aux(97) =< 2*V
aux(98) =< 3/2*V
it(34) =< aux(94)
it(37) =< aux(94)
it(34) =< aux(95)
it(37) =< aux(95)
it(34) =< aux(96)
aux(10) =< aux(97)
aux(10) =< aux(98)
it(37) =< aux(10)+aux(10)+aux(98)+aux(27)
it(37) =< aux(97)+aux(97)+aux(97)+aux(93)
s(17) =< aux(94)

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

* Chain [[34,35,36,37,38,39],48,52]: 6*it(34)+6*it(37)+8*s(17)+2
  Such that:aux(27) =< V1-V+1
aux(99) =< V1
aux(100) =< V1+V
aux(101) =< V1/2+V/2
aux(102) =< V
aux(103) =< 2*V
aux(104) =< 3/2*V
it(34) =< aux(100)
it(37) =< aux(100)
it(34) =< aux(101)
it(37) =< aux(101)
it(34) =< aux(102)
aux(10) =< aux(103)
aux(10) =< aux(104)
it(37) =< aux(10)+aux(10)+aux(104)+aux(27)
it(37) =< aux(103)+aux(103)+aux(103)+aux(99)
s(17) =< aux(100)

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

* Chain [[34,35,36,37,38,39],48,47,52]: 6*it(34)+6*it(37)+8*s(17)+4
  Such that:aux(27) =< V1-V+1
aux(105) =< V1
aux(106) =< V1+V
aux(107) =< V1/2+V/2
aux(108) =< V
aux(109) =< 2*V
aux(110) =< 3/2*V
it(34) =< aux(106)
it(37) =< aux(106)
it(34) =< aux(107)
it(37) =< aux(107)
it(34) =< aux(108)
aux(10) =< aux(109)
aux(10) =< aux(110)
it(37) =< aux(10)+aux(10)+aux(110)+aux(27)
it(37) =< aux(109)+aux(109)+aux(109)+aux(105)
s(17) =< aux(106)

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

* Chain [[34,35,36,37,38,39],45,52]: 6*it(34)+6*it(37)+8*s(17)+2
  Such that:aux(27) =< V1-V+1
aux(111) =< V1
aux(112) =< V1+V
aux(113) =< V1/2+V/2
aux(114) =< V
aux(115) =< 2*V
aux(116) =< 3/2*V
it(34) =< aux(112)
it(37) =< aux(112)
it(34) =< aux(113)
it(37) =< aux(113)
it(34) =< aux(114)
aux(10) =< aux(115)
aux(10) =< aux(116)
it(37) =< aux(10)+aux(10)+aux(116)+aux(27)
it(37) =< aux(115)+aux(115)+aux(115)+aux(111)
s(17) =< aux(112)

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

* Chain [[34,35,36,37,38,39],44,52]: 6*it(34)+6*it(37)+8*s(17)+2*s(28)+2
  Such that:aux(27) =< V1-V+1
aux(37) =< 3/2*V
aux(118) =< V1
aux(119) =< V1+V
aux(120) =< V1/2+V/2
aux(121) =< V
aux(122) =< 2*V
aux(123) =< 3*V
s(28) =< aux(123)
it(34) =< aux(119)
it(37) =< aux(119)
it(34) =< aux(120)
it(37) =< aux(120)
it(34) =< aux(121)
aux(10) =< aux(122)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(123)
aux(10) =< aux(123)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(122)+aux(122)+aux(122)+aux(118)
s(17) =< aux(119)

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

* Chain [[34,35,36,37,38,39],43,52]: 6*it(34)+6*it(37)+8*s(17)+2*s(30)+2
  Such that:aux(27) =< V1-V+1
aux(37) =< 3/2*V
aux(125) =< V1
aux(126) =< V1+V
aux(127) =< V1/2+V/2
aux(128) =< V
aux(129) =< 2*V
aux(130) =< 3*V
s(30) =< aux(130)
it(34) =< aux(126)
it(37) =< aux(126)
it(34) =< aux(127)
it(37) =< aux(127)
it(34) =< aux(128)
aux(10) =< aux(129)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(130)
aux(10) =< aux(130)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(129)+aux(129)+aux(129)+aux(125)
s(17) =< aux(126)

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

* Chain [[34,35,36,37,38,39],42,52]: 6*it(34)+6*it(37)+8*s(17)+2
  Such that:aux(27) =< V1-V+1
aux(131) =< V1
aux(132) =< V1+V
aux(133) =< V1/2+V/2
aux(134) =< V
aux(135) =< 2*V
aux(136) =< 3/2*V
it(34) =< aux(132)
it(37) =< aux(132)
it(34) =< aux(133)
it(37) =< aux(133)
it(34) =< aux(134)
aux(10) =< aux(135)
aux(10) =< aux(136)
it(37) =< aux(10)+aux(10)+aux(136)+aux(27)
it(37) =< aux(135)+aux(135)+aux(135)+aux(131)
s(17) =< aux(132)

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

* Chain [[34,35,36,37,38,39],41,52]: 6*it(34)+6*it(37)+8*s(17)+2*s(32)+2
  Such that:aux(27) =< V1-V+1
aux(38) =< 3*V
aux(37) =< 3/2*V
aux(138) =< V1
aux(139) =< V1+V
aux(140) =< V1/2+V/2
aux(141) =< V
aux(142) =< 2*V
s(32) =< aux(138)
it(34) =< aux(139)
it(37) =< aux(139)
it(34) =< aux(140)
it(37) =< aux(140)
it(34) =< aux(141)
aux(10) =< aux(142)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(38)
aux(10) =< aux(38)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(142)+aux(142)+aux(142)+aux(138)
s(17) =< aux(139)

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

* Chain [[34,35,36,37,38,39],40,52]: 6*it(34)+6*it(37)+8*s(17)+2*s(34)+2
  Such that:aux(27) =< V1-V+1
aux(38) =< 3*V
aux(37) =< 3/2*V
aux(144) =< V1
aux(145) =< V1+V
aux(146) =< V1/2+V/2
aux(147) =< V
aux(148) =< 2*V
s(34) =< aux(144)
it(34) =< aux(145)
it(37) =< aux(145)
it(34) =< aux(146)
it(37) =< aux(146)
it(34) =< aux(147)
aux(10) =< aux(148)
aux(9) =< aux(37)
aux(10) =< aux(37)
aux(9) =< aux(38)
aux(10) =< aux(38)
it(37) =< aux(10)+aux(10)+aux(9)+aux(27)
it(37) =< aux(148)+aux(148)+aux(148)+aux(144)
s(17) =< aux(145)

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

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

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

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

* Chain [51]: 1*s(25)+1*s(26)+1
  Such that:s(26) =< V1
s(25) =< V

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

* Chain [50]: 1*s(27)+1
  Such that:s(27) =< V

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

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

* Chain [48,[46],54]: 2*it(46)+3
  Such that:it(46) =< Out/2

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

* Chain [48,[46],53]: 2*it(46)+3
  Such that:it(46) =< Out/2

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

* Chain [48,[46],52]: 2*it(46)+2
  Such that:it(46) =< Out/2

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

* Chain [48,[46],47,52]: 2*it(46)+4
  Such that:it(46) =< Out/2

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

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

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

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

* Chain [48,47,52]: 4
  with precondition: [V1=1,Out=4,V>=2] 

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

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

* Chain [44,52]: 2*s(28)+2
  Such that:aux(117) =< V
s(28) =< aux(117)

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

* Chain [43,52]: 2*s(30)+2
  Such that:aux(124) =< V
s(30) =< aux(124)

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

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

* Chain [41,52]: 2*s(32)+2
  Such that:aux(137) =< V1
s(32) =< aux(137)

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

* Chain [40,52]: 2*s(34)+2
  Such that:aux(143) =< V1
s(34) =< aux(143)

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


#### Cost of chains of start(V1,V,V6):
* Chain [61]: 8*s(293)+9*s(302)+114*s(304)+30*s(305)+154*s(308)+54*s(309)+13*s(311)+30*s(312)+4
  Such that:aux(175) =< V1
aux(176) =< V1-V+1
aux(177) =< V1+V
aux(178) =< V1/2+V/2
aux(179) =< V
aux(180) =< 2*V
aux(181) =< 3*V
aux(182) =< 3/2*V
s(293) =< aux(179)
s(302) =< aux(175)
s(304) =< aux(177)
s(305) =< aux(177)
s(304) =< aux(178)
s(305) =< aux(178)
s(304) =< aux(179)
s(306) =< aux(180)
s(307) =< aux(182)
s(306) =< aux(182)
s(307) =< aux(181)
s(306) =< aux(181)
s(305) =< s(306)+s(306)+s(307)+aux(176)
s(305) =< aux(180)+aux(180)+aux(180)+aux(175)
s(308) =< aux(177)
s(309) =< aux(177)
s(309) =< aux(178)
s(310) =< aux(180)
s(310) =< aux(182)
s(309) =< s(310)+s(310)+aux(182)+aux(176)
s(309) =< aux(180)+aux(180)+aux(180)+aux(175)
s(311) =< aux(181)
s(312) =< aux(177)
s(312) =< s(306)+s(306)+s(307)+aux(176)
s(312) =< aux(180)+aux(180)+aux(180)+aux(175)

  with precondition: [V1>=0] 

* Chain [60]: 316*s(347)+19*s(348)+18*s(359)+228*s(361)+60*s(362)+108*s(366)+26*s(368)+60*s(369)+5
  Such that:aux(186) =< -2*V+V6+1
aux(187) =< -V+V6
aux(188) =< V
aux(189) =< 2*V
aux(190) =< 3*V
aux(191) =< 3/2*V
aux(192) =< V6
aux(193) =< V6/2
s(348) =< aux(188)
s(359) =< aux(187)
s(361) =< aux(192)
s(362) =< aux(192)
s(361) =< aux(193)
s(362) =< aux(193)
s(361) =< aux(188)
s(363) =< aux(189)
s(364) =< aux(191)
s(363) =< aux(191)
s(364) =< aux(190)
s(363) =< aux(190)
s(362) =< s(363)+s(363)+s(364)+aux(186)
s(362) =< aux(189)+aux(189)+aux(189)+aux(187)
s(347) =< aux(192)
s(366) =< aux(192)
s(366) =< aux(193)
s(367) =< aux(189)
s(367) =< aux(191)
s(366) =< s(367)+s(367)+aux(191)+aux(186)
s(366) =< aux(189)+aux(189)+aux(189)+aux(187)
s(368) =< aux(190)
s(369) =< aux(192)
s(369) =< s(363)+s(363)+s(364)+aux(186)
s(369) =< aux(189)+aux(189)+aux(189)+aux(187)

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

* Chain [59]: 19*s(457)+8*s(465)+5
  Such that:s(464) =< V
aux(195) =< V6
s(457) =< aux(195)
s(465) =< s(464)

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

* Chain [58]: 316*s(467)+19*s(468)+18*s(479)+228*s(481)+60*s(482)+108*s(486)+26*s(488)+60*s(489)+5
  Such that:aux(199) =< V
aux(200) =< V-2*V6+1
aux(201) =< V-V6
aux(202) =< V/2
aux(203) =< V6
aux(204) =< 2*V6
aux(205) =< 3*V6
aux(206) =< 3/2*V6
s(468) =< aux(203)
s(467) =< aux(199)
s(479) =< aux(201)
s(481) =< aux(199)
s(482) =< aux(199)
s(481) =< aux(202)
s(482) =< aux(202)
s(481) =< aux(203)
s(483) =< aux(204)
s(484) =< aux(206)
s(483) =< aux(206)
s(484) =< aux(205)
s(483) =< aux(205)
s(482) =< s(483)+s(483)+s(484)+aux(200)
s(482) =< aux(204)+aux(204)+aux(204)+aux(201)
s(486) =< aux(199)
s(486) =< aux(202)
s(487) =< aux(204)
s(487) =< aux(206)
s(486) =< s(487)+s(487)+aux(206)+aux(200)
s(486) =< aux(204)+aux(204)+aux(204)+aux(201)
s(488) =< aux(205)
s(489) =< aux(199)
s(489) =< s(483)+s(483)+s(484)+aux(200)
s(489) =< aux(204)+aux(204)+aux(204)+aux(201)

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

* Chain [57]: 19*s(577)+5
  Such that:aux(208) =< V6
s(577) =< aux(208)

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

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

* Chain [55]: 8*s(585)+2
  Such that:s(584) =< V1
s(585) =< s(584)

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


Closed-form bounds of start(V1,V,V6): 
-------------------------------------
* Chain [61] with precondition: [V1>=0] 
    - Upper bound: 9*V1+4+nat(V)*8+nat(3*V)*13+nat(V1+V)*382 
    - Complexity: n 
* Chain [60] with precondition: [V1=1,V>=1,V6>=1] 
    - Upper bound: 97*V+772*V6+5+nat(-V+V6)*18 
    - Complexity: n 
* Chain [59] with precondition: [V1=1,V>=2] 
    - Upper bound: 8*V+5+nat(V6)*19 
    - Complexity: n 
* Chain [58] with precondition: [V1=2,V>=1,V6>=1] 
    - Upper bound: 772*V+97*V6+5+nat(V-V6)*18 
    - Complexity: n 
* Chain [57] with precondition: [V1=2,V=V6+1,V>=3] 
    - Upper bound: 19*V6+5 
    - Complexity: n 
* Chain [56] with precondition: [V=0,V1>=0] 
    - Upper bound: 0 
    - Complexity: constant 
* Chain [55] with precondition: [V=1,V1>=1] 
    - Upper bound: 8*V1+2 
    - Complexity: n 

### Maximum cost of start(V1,V,V6): max([max([8*V1+2,nat(V6)*19+5]),nat(V)*8+4+max([nat(V6)*19+1+(nat(V)*11+max([nat(3*V)*26+nat(V6)*753+nat(-V+V6)*18,nat(3*V6)*26+nat(V)*753+nat(V-V6)*18])),nat(3*V)*13+9*V1+nat(V1+V)*382])]) 
Asymptotic class: n 
* Total analysis performed in 2385 ms.


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

(20)
BOUNDS(1, n^1)

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

(21) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(22)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, s(z1)) -> pred(minus(z0, z1))
   minus(z0, 0) -> z0
   pred(s(z0)) -> z0
   le(s(z0), s(z1)) -> le(z0, z1)
   le(s(z0), 0) -> false
   le(0, z0) -> true
   gcd(0, z0) -> 0
   gcd(s(z0), 0) -> s(z0)
   gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
   if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
   if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))
Tuples:
   MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
   MINUS(z0, 0) -> c1
   PRED(s(z0)) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   LE(s(z0), 0) -> c4
   LE(0, z0) -> c5
   GCD(0, z0) -> c6
   GCD(s(z0), 0) -> c7
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
S tuples:
   MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
   MINUS(z0, 0) -> c1
   PRED(s(z0)) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   LE(s(z0), 0) -> c4
   LE(0, z0) -> c5
   GCD(0, z0) -> c6
   GCD(s(z0), 0) -> c7
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
K tuples:none
Defined Rule Symbols:   minus_2, pred_1, le_2, gcd_2, if_3

Defined Pair Symbols:   MINUS_2, PRED_1, LE_2, GCD_2, IF_3

Compound Symbols:   c_2, c1, c2, c3_1, c4, c5, c6, c7, c8_2, c9_2, c10_2


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

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

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

   MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
   MINUS(z0, 0) -> c1
   PRED(s(z0)) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   LE(s(z0), 0) -> c4
   LE(0, z0) -> c5
   GCD(0, z0) -> c6
   GCD(s(z0), 0) -> c7
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))

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

   minus(z0, s(z1)) -> pred(minus(z0, z1))
   minus(z0, 0) -> z0
   pred(s(z0)) -> z0
   le(s(z0), s(z1)) -> le(z0, z1)
   le(s(z0), 0) -> false
   le(0, z0) -> true
   gcd(0, z0) -> 0
   gcd(s(z0), 0) -> s(z0)
   gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
   if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
   if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

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

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

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

   MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
   MINUS(z0, 0') -> c1
   PRED(s(z0)) -> c2
   LE(s(z0), s(z1)) -> c3(LE(z0, z1))
   LE(s(z0), 0') -> c4
   LE(0', z0) -> c5
   GCD(0', z0) -> c6
   GCD(s(z0), 0') -> c7
   GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
   IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
   IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))

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

   minus(z0, s(z1)) -> pred(minus(z0, z1))
   minus(z0, 0') -> z0
   pred(s(z0)) -> z0
   le(s(z0), s(z1)) -> le(z0, z1)
   le(s(z0), 0') -> false
   le(0', z0) -> true
   gcd(0', z0) -> 0'
   gcd(s(z0), 0') -> s(z0)
   gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
   if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
   if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

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

(27) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
MINUS(z0, 0') -> c1
PRED(s(z0)) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
LE(s(z0), 0') -> c4
LE(0', z0) -> c5
GCD(0', z0) -> c6
GCD(s(z0), 0') -> c7
GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
minus(z0, s(z1)) -> pred(minus(z0, z1))
minus(z0, 0') -> z0
pred(s(z0)) -> z0
le(s(z0), s(z1)) -> le(z0, z1)
le(s(z0), 0') -> false
le(0', z0) -> true
gcd(0', z0) -> 0'
gcd(s(z0), 0') -> s(z0)
gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

Types:
MINUS :: s:0' -> s:0' -> c:c1
s :: s:0' -> s:0'
c :: c2 -> c:c1 -> c:c1
PRED :: s:0' -> c2
minus :: s:0' -> s:0' -> s:0'
0' :: s:0'
c1 :: c:c1
c2 :: c2
LE :: s:0' -> s:0' -> c3:c4:c5
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
GCD :: s:0' -> s:0' -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c9:c10 -> c3:c4:c5 -> c6:c7:c8
IF :: true:false -> s:0' -> s:0' -> c9:c10
le :: s:0' -> s:0' -> true:false
true :: true:false
c9 :: c6:c7:c8 -> c:c1 -> c9:c10
false :: true:false
c10 :: c6:c7:c8 -> c:c1 -> c9:c10
pred :: s:0' -> s:0'
gcd :: s:0' -> s:0' -> s:0'
if :: true:false -> s:0' -> s:0' -> s:0'
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c23_11 :: c2
hole_c3:c4:c54_11 :: c3:c4:c5
hole_c6:c7:c85_11 :: c6:c7:c8
hole_c9:c106_11 :: c9:c10
hole_true:false7_11 :: true:false
gen_c:c18_11 :: Nat -> c:c1
gen_s:0'9_11 :: Nat -> s:0'
gen_c3:c4:c510_11 :: Nat -> c3:c4:c5

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

(29) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MINUS, minus, LE, GCD, le, gcd

They will be analysed ascendingly in the following order:
minus < MINUS
MINUS < GCD
minus < GCD
minus < gcd
LE < GCD
le < GCD
le < gcd

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

(30)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
MINUS(z0, 0') -> c1
PRED(s(z0)) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
LE(s(z0), 0') -> c4
LE(0', z0) -> c5
GCD(0', z0) -> c6
GCD(s(z0), 0') -> c7
GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
minus(z0, s(z1)) -> pred(minus(z0, z1))
minus(z0, 0') -> z0
pred(s(z0)) -> z0
le(s(z0), s(z1)) -> le(z0, z1)
le(s(z0), 0') -> false
le(0', z0) -> true
gcd(0', z0) -> 0'
gcd(s(z0), 0') -> s(z0)
gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

Types:
MINUS :: s:0' -> s:0' -> c:c1
s :: s:0' -> s:0'
c :: c2 -> c:c1 -> c:c1
PRED :: s:0' -> c2
minus :: s:0' -> s:0' -> s:0'
0' :: s:0'
c1 :: c:c1
c2 :: c2
LE :: s:0' -> s:0' -> c3:c4:c5
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
GCD :: s:0' -> s:0' -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c9:c10 -> c3:c4:c5 -> c6:c7:c8
IF :: true:false -> s:0' -> s:0' -> c9:c10
le :: s:0' -> s:0' -> true:false
true :: true:false
c9 :: c6:c7:c8 -> c:c1 -> c9:c10
false :: true:false
c10 :: c6:c7:c8 -> c:c1 -> c9:c10
pred :: s:0' -> s:0'
gcd :: s:0' -> s:0' -> s:0'
if :: true:false -> s:0' -> s:0' -> s:0'
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c23_11 :: c2
hole_c3:c4:c54_11 :: c3:c4:c5
hole_c6:c7:c85_11 :: c6:c7:c8
hole_c9:c106_11 :: c9:c10
hole_true:false7_11 :: true:false
gen_c:c18_11 :: Nat -> c:c1
gen_s:0'9_11 :: Nat -> s:0'
gen_c3:c4:c510_11 :: Nat -> c3:c4:c5


Generator Equations:
gen_c:c18_11(0) <=> c1
gen_c:c18_11(+(x, 1)) <=> c(c2, gen_c:c18_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c3:c4:c510_11(0) <=> c4
gen_c3:c4:c510_11(+(x, 1)) <=> c3(gen_c3:c4:c510_11(x))


The following defined symbols remain to be analysed:
minus, MINUS, LE, GCD, le, gcd

They will be analysed ascendingly in the following order:
minus < MINUS
MINUS < GCD
minus < GCD
minus < gcd
LE < GCD
le < GCD
le < gcd

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minus(gen_s:0'9_11(a), gen_s:0'9_11(+(1, n12_11))) -> *11_11, rt in Omega(0)

Induction Base:
minus(gen_s:0'9_11(a), gen_s:0'9_11(+(1, 0)))

Induction Step:
minus(gen_s:0'9_11(a), gen_s:0'9_11(+(1, +(n12_11, 1)))) ->_R^Omega(0)
pred(minus(gen_s:0'9_11(a), gen_s:0'9_11(+(1, n12_11)))) ->_IH
pred(*11_11)

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

(32)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
MINUS(z0, 0') -> c1
PRED(s(z0)) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
LE(s(z0), 0') -> c4
LE(0', z0) -> c5
GCD(0', z0) -> c6
GCD(s(z0), 0') -> c7
GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
minus(z0, s(z1)) -> pred(minus(z0, z1))
minus(z0, 0') -> z0
pred(s(z0)) -> z0
le(s(z0), s(z1)) -> le(z0, z1)
le(s(z0), 0') -> false
le(0', z0) -> true
gcd(0', z0) -> 0'
gcd(s(z0), 0') -> s(z0)
gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

Types:
MINUS :: s:0' -> s:0' -> c:c1
s :: s:0' -> s:0'
c :: c2 -> c:c1 -> c:c1
PRED :: s:0' -> c2
minus :: s:0' -> s:0' -> s:0'
0' :: s:0'
c1 :: c:c1
c2 :: c2
LE :: s:0' -> s:0' -> c3:c4:c5
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
GCD :: s:0' -> s:0' -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c9:c10 -> c3:c4:c5 -> c6:c7:c8
IF :: true:false -> s:0' -> s:0' -> c9:c10
le :: s:0' -> s:0' -> true:false
true :: true:false
c9 :: c6:c7:c8 -> c:c1 -> c9:c10
false :: true:false
c10 :: c6:c7:c8 -> c:c1 -> c9:c10
pred :: s:0' -> s:0'
gcd :: s:0' -> s:0' -> s:0'
if :: true:false -> s:0' -> s:0' -> s:0'
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c23_11 :: c2
hole_c3:c4:c54_11 :: c3:c4:c5
hole_c6:c7:c85_11 :: c6:c7:c8
hole_c9:c106_11 :: c9:c10
hole_true:false7_11 :: true:false
gen_c:c18_11 :: Nat -> c:c1
gen_s:0'9_11 :: Nat -> s:0'
gen_c3:c4:c510_11 :: Nat -> c3:c4:c5


Lemmas:
minus(gen_s:0'9_11(a), gen_s:0'9_11(+(1, n12_11))) -> *11_11, rt in Omega(0)


Generator Equations:
gen_c:c18_11(0) <=> c1
gen_c:c18_11(+(x, 1)) <=> c(c2, gen_c:c18_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c3:c4:c510_11(0) <=> c4
gen_c3:c4:c510_11(+(x, 1)) <=> c3(gen_c3:c4:c510_11(x))


The following defined symbols remain to be analysed:
MINUS, LE, GCD, le, gcd

They will be analysed ascendingly in the following order:
MINUS < GCD
LE < GCD
le < GCD
le < gcd

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_s:0'9_11(+(1, n17276_11)), gen_s:0'9_11(n17276_11)) -> gen_c3:c4:c510_11(n17276_11), rt in Omega(1 + n17276_11)

Induction Base:
LE(gen_s:0'9_11(+(1, 0)), gen_s:0'9_11(0)) ->_R^Omega(1)
c4

Induction Step:
LE(gen_s:0'9_11(+(1, +(n17276_11, 1))), gen_s:0'9_11(+(n17276_11, 1))) ->_R^Omega(1)
c3(LE(gen_s:0'9_11(+(1, n17276_11)), gen_s:0'9_11(n17276_11))) ->_IH
c3(gen_c3:c4:c510_11(c17277_11))

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

(34)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
MINUS(z0, 0') -> c1
PRED(s(z0)) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
LE(s(z0), 0') -> c4
LE(0', z0) -> c5
GCD(0', z0) -> c6
GCD(s(z0), 0') -> c7
GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
minus(z0, s(z1)) -> pred(minus(z0, z1))
minus(z0, 0') -> z0
pred(s(z0)) -> z0
le(s(z0), s(z1)) -> le(z0, z1)
le(s(z0), 0') -> false
le(0', z0) -> true
gcd(0', z0) -> 0'
gcd(s(z0), 0') -> s(z0)
gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

Types:
MINUS :: s:0' -> s:0' -> c:c1
s :: s:0' -> s:0'
c :: c2 -> c:c1 -> c:c1
PRED :: s:0' -> c2
minus :: s:0' -> s:0' -> s:0'
0' :: s:0'
c1 :: c:c1
c2 :: c2
LE :: s:0' -> s:0' -> c3:c4:c5
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
GCD :: s:0' -> s:0' -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c9:c10 -> c3:c4:c5 -> c6:c7:c8
IF :: true:false -> s:0' -> s:0' -> c9:c10
le :: s:0' -> s:0' -> true:false
true :: true:false
c9 :: c6:c7:c8 -> c:c1 -> c9:c10
false :: true:false
c10 :: c6:c7:c8 -> c:c1 -> c9:c10
pred :: s:0' -> s:0'
gcd :: s:0' -> s:0' -> s:0'
if :: true:false -> s:0' -> s:0' -> s:0'
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c23_11 :: c2
hole_c3:c4:c54_11 :: c3:c4:c5
hole_c6:c7:c85_11 :: c6:c7:c8
hole_c9:c106_11 :: c9:c10
hole_true:false7_11 :: true:false
gen_c:c18_11 :: Nat -> c:c1
gen_s:0'9_11 :: Nat -> s:0'
gen_c3:c4:c510_11 :: Nat -> c3:c4:c5


Lemmas:
minus(gen_s:0'9_11(a), gen_s:0'9_11(+(1, n12_11))) -> *11_11, rt in Omega(0)


Generator Equations:
gen_c:c18_11(0) <=> c1
gen_c:c18_11(+(x, 1)) <=> c(c2, gen_c:c18_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c3:c4:c510_11(0) <=> c4
gen_c3:c4:c510_11(+(x, 1)) <=> c3(gen_c3:c4:c510_11(x))


The following defined symbols remain to be analysed:
LE, GCD, le, gcd

They will be analysed ascendingly in the following order:
LE < GCD
le < GCD
le < gcd

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

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

(37)
BOUNDS(n^1, INF)

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

(38)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
MINUS(z0, 0') -> c1
PRED(s(z0)) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
LE(s(z0), 0') -> c4
LE(0', z0) -> c5
GCD(0', z0) -> c6
GCD(s(z0), 0') -> c7
GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
minus(z0, s(z1)) -> pred(minus(z0, z1))
minus(z0, 0') -> z0
pred(s(z0)) -> z0
le(s(z0), s(z1)) -> le(z0, z1)
le(s(z0), 0') -> false
le(0', z0) -> true
gcd(0', z0) -> 0'
gcd(s(z0), 0') -> s(z0)
gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

Types:
MINUS :: s:0' -> s:0' -> c:c1
s :: s:0' -> s:0'
c :: c2 -> c:c1 -> c:c1
PRED :: s:0' -> c2
minus :: s:0' -> s:0' -> s:0'
0' :: s:0'
c1 :: c:c1
c2 :: c2
LE :: s:0' -> s:0' -> c3:c4:c5
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
GCD :: s:0' -> s:0' -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c9:c10 -> c3:c4:c5 -> c6:c7:c8
IF :: true:false -> s:0' -> s:0' -> c9:c10
le :: s:0' -> s:0' -> true:false
true :: true:false
c9 :: c6:c7:c8 -> c:c1 -> c9:c10
false :: true:false
c10 :: c6:c7:c8 -> c:c1 -> c9:c10
pred :: s:0' -> s:0'
gcd :: s:0' -> s:0' -> s:0'
if :: true:false -> s:0' -> s:0' -> s:0'
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c23_11 :: c2
hole_c3:c4:c54_11 :: c3:c4:c5
hole_c6:c7:c85_11 :: c6:c7:c8
hole_c9:c106_11 :: c9:c10
hole_true:false7_11 :: true:false
gen_c:c18_11 :: Nat -> c:c1
gen_s:0'9_11 :: Nat -> s:0'
gen_c3:c4:c510_11 :: Nat -> c3:c4:c5


Lemmas:
minus(gen_s:0'9_11(a), gen_s:0'9_11(+(1, n12_11))) -> *11_11, rt in Omega(0)
LE(gen_s:0'9_11(+(1, n17276_11)), gen_s:0'9_11(n17276_11)) -> gen_c3:c4:c510_11(n17276_11), rt in Omega(1 + n17276_11)


Generator Equations:
gen_c:c18_11(0) <=> c1
gen_c:c18_11(+(x, 1)) <=> c(c2, gen_c:c18_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c3:c4:c510_11(0) <=> c4
gen_c3:c4:c510_11(+(x, 1)) <=> c3(gen_c3:c4:c510_11(x))


The following defined symbols remain to be analysed:
le, GCD, gcd

They will be analysed ascendingly in the following order:
le < GCD
le < gcd

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

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_s:0'9_11(+(1, n18109_11)), gen_s:0'9_11(n18109_11)) -> false, rt in Omega(0)

Induction Base:
le(gen_s:0'9_11(+(1, 0)), gen_s:0'9_11(0)) ->_R^Omega(0)
false

Induction Step:
le(gen_s:0'9_11(+(1, +(n18109_11, 1))), gen_s:0'9_11(+(n18109_11, 1))) ->_R^Omega(0)
le(gen_s:0'9_11(+(1, n18109_11)), gen_s:0'9_11(n18109_11)) ->_IH
false

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

(40)
Obligation:
Innermost TRS:
Rules:
MINUS(z0, s(z1)) -> c(PRED(minus(z0, z1)), MINUS(z0, z1))
MINUS(z0, 0') -> c1
PRED(s(z0)) -> c2
LE(s(z0), s(z1)) -> c3(LE(z0, z1))
LE(s(z0), 0') -> c4
LE(0', z0) -> c5
GCD(0', z0) -> c6
GCD(s(z0), 0') -> c7
GCD(s(z0), s(z1)) -> c8(IF(le(z1, z0), s(z0), s(z1)), LE(z1, z0))
IF(true, s(z0), s(z1)) -> c9(GCD(minus(z0, z1), s(z1)), MINUS(z0, z1))
IF(false, s(z0), s(z1)) -> c10(GCD(minus(z1, z0), s(z0)), MINUS(z1, z0))
minus(z0, s(z1)) -> pred(minus(z0, z1))
minus(z0, 0') -> z0
pred(s(z0)) -> z0
le(s(z0), s(z1)) -> le(z0, z1)
le(s(z0), 0') -> false
le(0', z0) -> true
gcd(0', z0) -> 0'
gcd(s(z0), 0') -> s(z0)
gcd(s(z0), s(z1)) -> if(le(z1, z0), s(z0), s(z1))
if(true, s(z0), s(z1)) -> gcd(minus(z0, z1), s(z1))
if(false, s(z0), s(z1)) -> gcd(minus(z1, z0), s(z0))

Types:
MINUS :: s:0' -> s:0' -> c:c1
s :: s:0' -> s:0'
c :: c2 -> c:c1 -> c:c1
PRED :: s:0' -> c2
minus :: s:0' -> s:0' -> s:0'
0' :: s:0'
c1 :: c:c1
c2 :: c2
LE :: s:0' -> s:0' -> c3:c4:c5
c3 :: c3:c4:c5 -> c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5
GCD :: s:0' -> s:0' -> c6:c7:c8
c6 :: c6:c7:c8
c7 :: c6:c7:c8
c8 :: c9:c10 -> c3:c4:c5 -> c6:c7:c8
IF :: true:false -> s:0' -> s:0' -> c9:c10
le :: s:0' -> s:0' -> true:false
true :: true:false
c9 :: c6:c7:c8 -> c:c1 -> c9:c10
false :: true:false
c10 :: c6:c7:c8 -> c:c1 -> c9:c10
pred :: s:0' -> s:0'
gcd :: s:0' -> s:0' -> s:0'
if :: true:false -> s:0' -> s:0' -> s:0'
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c23_11 :: c2
hole_c3:c4:c54_11 :: c3:c4:c5
hole_c6:c7:c85_11 :: c6:c7:c8
hole_c9:c106_11 :: c9:c10
hole_true:false7_11 :: true:false
gen_c:c18_11 :: Nat -> c:c1
gen_s:0'9_11 :: Nat -> s:0'
gen_c3:c4:c510_11 :: Nat -> c3:c4:c5


Lemmas:
minus(gen_s:0'9_11(a), gen_s:0'9_11(+(1, n12_11))) -> *11_11, rt in Omega(0)
LE(gen_s:0'9_11(+(1, n17276_11)), gen_s:0'9_11(n17276_11)) -> gen_c3:c4:c510_11(n17276_11), rt in Omega(1 + n17276_11)
le(gen_s:0'9_11(+(1, n18109_11)), gen_s:0'9_11(n18109_11)) -> false, rt in Omega(0)


Generator Equations:
gen_c:c18_11(0) <=> c1
gen_c:c18_11(+(x, 1)) <=> c(c2, gen_c:c18_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c3:c4:c510_11(0) <=> c4
gen_c3:c4:c510_11(+(x, 1)) <=> c3(gen_c3:c4:c510_11(x))


The following defined symbols remain to be analysed:
GCD, gcd