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

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


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

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


The TRS R consists of the following rules:

   gt(s(x), 0) -> true
   gt(0, y) -> false
   gt(s(x), s(y)) -> gt(x, y)
   divides(x, y) -> div(x, y, y)
   div(0, 0, z) -> true
   div(0, s(x), z) -> false
   div(s(x), 0, s(z)) -> div(s(x), s(z), s(z))
   div(s(x), s(y), z) -> div(x, y, z)
   prime(x) -> test(x, s(s(0)))
   test(x, y) -> if1(gt(x, y), x, y)
   if1(true, x, y) -> if2(divides(x, y), x, y)
   if1(false, x, y) -> true
   if2(true, x, y) -> false
   if2(false, x, y) -> test(x, s(y))

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   gt(s(z0), 0) -> true
   gt(0, z0) -> false
   gt(s(z0), s(z1)) -> gt(z0, z1)
   divides(z0, z1) -> div(z0, z1, z1)
   div(0, 0, z0) -> true
   div(0, s(z0), z1) -> false
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1))
   div(s(z0), s(z1), z2) -> div(z0, z1, z2)
   prime(z0) -> test(z0, s(s(0)))
   test(z0, z1) -> if1(gt(z0, z1), z0, z1)
   if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
   if1(false, z0, z1) -> true
   if2(true, z0, z1) -> false
   if2(false, z0, z1) -> test(z0, s(z1))
Tuples:
   GT(s(z0), 0) -> c
   GT(0, z0) -> c1
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(0, 0, z0) -> c4
   DIV(0, s(z0), z1) -> c5
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   PRIME(z0) -> c8(TEST(z0, s(s(0))))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF1(false, z0, z1) -> c11
   IF2(true, z0, z1) -> c12
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
S tuples:
   GT(s(z0), 0) -> c
   GT(0, z0) -> c1
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(0, 0, z0) -> c4
   DIV(0, s(z0), z1) -> c5
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   PRIME(z0) -> c8(TEST(z0, s(s(0))))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF1(false, z0, z1) -> c11
   IF2(true, z0, z1) -> c12
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
K tuples:none
Defined Rule Symbols:   gt_2, divides_2, div_3, prime_1, test_2, if1_3, if2_3

Defined Pair Symbols:   GT_2, DIVIDES_2, DIV_3, PRIME_1, TEST_2, IF1_3, IF2_3

Compound Symbols:   c, c1, c2_1, c3_1, c4, c5, c6_1, c7_1, c8_1, c9_2, c10_2, c11, c12, c13_1


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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   PRIME(z0) -> c8(TEST(z0, s(s(0))))
Removed 6 trailing nodes:
   GT(0, z0) -> c1
   IF2(true, z0, z1) -> c12
   IF1(false, z0, z1) -> c11
   DIV(0, 0, z0) -> c4
   DIV(0, s(z0), z1) -> c5
   GT(s(z0), 0) -> c

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   gt(s(z0), 0) -> true
   gt(0, z0) -> false
   gt(s(z0), s(z1)) -> gt(z0, z1)
   divides(z0, z1) -> div(z0, z1, z1)
   div(0, 0, z0) -> true
   div(0, s(z0), z1) -> false
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1))
   div(s(z0), s(z1), z2) -> div(z0, z1, z2)
   prime(z0) -> test(z0, s(s(0)))
   test(z0, z1) -> if1(gt(z0, z1), z0, z1)
   if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
   if1(false, z0, z1) -> true
   if2(true, z0, z1) -> false
   if2(false, z0, z1) -> test(z0, s(z1))
Tuples:
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
S tuples:
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
K tuples:none
Defined Rule Symbols:   gt_2, divides_2, div_3, prime_1, test_2, if1_3, if2_3

Defined Pair Symbols:   GT_2, DIVIDES_2, DIV_3, TEST_2, IF1_3, IF2_3

Compound Symbols:   c2_1, c3_1, c6_1, c7_1, c9_2, c10_2, c13_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   prime(z0) -> test(z0, s(s(0)))
   test(z0, z1) -> if1(gt(z0, z1), z0, z1)
   if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
   if1(false, z0, z1) -> true
   if2(true, z0, z1) -> false
   if2(false, z0, z1) -> test(z0, s(z1))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   gt(s(z0), 0) -> true
   gt(0, z0) -> false
   gt(s(z0), s(z1)) -> gt(z0, z1)
   divides(z0, z1) -> div(z0, z1, z1)
   div(0, 0, z0) -> true
   div(0, s(z0), z1) -> false
   div(s(z0), s(z1), z2) -> div(z0, z1, z2)
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1))
Tuples:
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
S tuples:
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
K tuples:none
Defined Rule Symbols:   gt_2, divides_2, div_3

Defined Pair Symbols:   GT_2, DIVIDES_2, DIV_3, TEST_2, IF1_3, IF2_3

Compound Symbols:   c2_1, c3_1, c6_1, c7_1, c9_2, c10_2, c13_1


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

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

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


The TRS R consists of the following rules:

   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))

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

   gt(s(z0), 0) -> true
   gt(0, z0) -> false
   gt(s(z0), s(z1)) -> gt(z0, z1)
   divides(z0, z1) -> div(z0, z1, z1)
   div(0, 0, z0) -> true
   div(0, s(z0), z1) -> false
   div(s(z0), s(z1), z2) -> div(z0, z1, z2)
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1))

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

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

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


The TRS R consists of the following rules:

   GT(s(z0), s(z1)) -> c2(GT(z0, z1)) [1]
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1)) [1]
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1))) [1]
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2)) [1]
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1)) [1]
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1)) [1]
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1))) [1]
   gt(s(z0), 0) -> true [0]
   gt(0, z0) -> false [0]
   gt(s(z0), s(z1)) -> gt(z0, z1) [0]
   divides(z0, z1) -> div(z0, z1, z1) [0]
   div(0, 0, z0) -> true [0]
   div(0, s(z0), z1) -> false [0]
   div(s(z0), s(z1), z2) -> div(z0, z1, z2) [0]
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1)) [0]

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

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

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

   GT(s(z0), s(z1)) -> c2(GT(z0, z1)) [1]
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1)) [1]
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1))) [1]
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2)) [1]
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1)) [1]
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1)) [1]
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1))) [1]
   gt(s(z0), 0) -> true [0]
   gt(0, z0) -> false [0]
   gt(s(z0), s(z1)) -> gt(z0, z1) [0]
   divides(z0, z1) -> div(z0, z1, z1) [0]
   div(0, 0, z0) -> true [0]
   div(0, s(z0), z1) -> false [0]
   div(s(z0), s(z1), z2) -> div(z0, z1, z2) [0]
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1)) [0]

The TRS has the following type information:
GT :: s:0 -> s:0 -> c2
s :: s:0 -> s:0
c2 :: c2 -> c2
DIVIDES :: s:0 -> s:0 -> c3
c3 :: c6:c7 -> c3
DIV :: s:0 -> s:0 -> s:0 -> c6:c7
0 :: s:0
c6 :: c6:c7 -> c6:c7
c7 :: c6:c7 -> c6:c7
TEST :: s:0 -> s:0 -> c9
c9 :: c10 -> c2 -> c9
IF1 :: true:false -> s:0 -> s:0 -> c10
gt :: s:0 -> s:0 -> true:false
true :: true:false
c10 :: c13 -> c3 -> c10
IF2 :: true:false -> s:0 -> s:0 -> c13
divides :: s:0 -> s:0 -> true:false
false :: true:false
c13 :: c9 -> c13
div :: s:0 -> s:0 -> s:0 -> true:false

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

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

   gt(v0, v1) -> null_gt [0]
   divides(v0, v1) -> null_divides [0]
   div(v0, v1, v2) -> null_div [0]
   GT(v0, v1) -> null_GT [0]
   DIV(v0, v1, v2) -> null_DIV [0]
   IF1(v0, v1, v2) -> null_IF1 [0]
   IF2(v0, v1, v2) -> null_IF2 [0]

And the following fresh constants:    null_gt, null_divides, null_div, null_GT, null_DIV, null_IF1, null_IF2, const, const1

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

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

   GT(s(z0), s(z1)) -> c2(GT(z0, z1)) [1]
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1)) [1]
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1))) [1]
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2)) [1]
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1)) [1]
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1)) [1]
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1))) [1]
   gt(s(z0), 0) -> true [0]
   gt(0, z0) -> false [0]
   gt(s(z0), s(z1)) -> gt(z0, z1) [0]
   divides(z0, z1) -> div(z0, z1, z1) [0]
   div(0, 0, z0) -> true [0]
   div(0, s(z0), z1) -> false [0]
   div(s(z0), s(z1), z2) -> div(z0, z1, z2) [0]
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1)) [0]
   gt(v0, v1) -> null_gt [0]
   divides(v0, v1) -> null_divides [0]
   div(v0, v1, v2) -> null_div [0]
   GT(v0, v1) -> null_GT [0]
   DIV(v0, v1, v2) -> null_DIV [0]
   IF1(v0, v1, v2) -> null_IF1 [0]
   IF2(v0, v1, v2) -> null_IF2 [0]

The TRS has the following type information:
GT :: s:0 -> s:0 -> c2:null_GT
s :: s:0 -> s:0
c2 :: c2:null_GT -> c2:null_GT
DIVIDES :: s:0 -> s:0 -> c3
c3 :: c6:c7:null_DIV -> c3
DIV :: s:0 -> s:0 -> s:0 -> c6:c7:null_DIV
0 :: s:0
c6 :: c6:c7:null_DIV -> c6:c7:null_DIV
c7 :: c6:c7:null_DIV -> c6:c7:null_DIV
TEST :: s:0 -> s:0 -> c9
c9 :: c10:null_IF1 -> c2:null_GT -> c9
IF1 :: true:false:null_gt:null_divides:null_div -> s:0 -> s:0 -> c10:null_IF1
gt :: s:0 -> s:0 -> true:false:null_gt:null_divides:null_div
true :: true:false:null_gt:null_divides:null_div
c10 :: c13:null_IF2 -> c3 -> c10:null_IF1
IF2 :: true:false:null_gt:null_divides:null_div -> s:0 -> s:0 -> c13:null_IF2
divides :: s:0 -> s:0 -> true:false:null_gt:null_divides:null_div
false :: true:false:null_gt:null_divides:null_div
c13 :: c9 -> c13:null_IF2
div :: s:0 -> s:0 -> s:0 -> true:false:null_gt:null_divides:null_div
null_gt :: true:false:null_gt:null_divides:null_div
null_divides :: true:false:null_gt:null_divides:null_div
null_div :: true:false:null_gt:null_divides:null_div
null_GT :: c2:null_GT
null_DIV :: c6:c7:null_DIV
null_IF1 :: c10:null_IF1
null_IF2 :: c13:null_IF2
const :: c3
const1 :: c9

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

(15) 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
   true => 2
   false => 1
   null_gt => 0
   null_divides => 0
   null_div => 0
   null_GT => 0
   null_DIV => 0
   null_IF1 => 0
   null_IF2 => 0
   const => 0
   const1 => 0

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

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

   DIV(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   DIV(z, z', z'') -{ 1 }-> 1 + DIV(z0, z1, z2) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z2 >= 0
   DIV(z, z', z'') -{ 1 }-> 1 + DIV(1 + z0, 1 + z1, 1 + z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z'' = 1 + z1, z' = 0
   DIVIDES(z, z') -{ 1 }-> 1 + DIV(z0, z1, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   GT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   GT(z, z') -{ 1 }-> 1 + GT(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   IF1(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IF1(z, z', z'') -{ 1 }-> 1 + IF2(divides(z0, z1), z0, z1) + DIVIDES(z0, z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   IF2(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IF2(z, z', z'') -{ 1 }-> 1 + TEST(z0, 1 + z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   TEST(z, z') -{ 1 }-> 1 + IF1(gt(z0, z1), z0, z1) + GT(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   div(z, z', z'') -{ 0 }-> div(z0, z1, z2) :|: z'' = z2, z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1, z2 >= 0
   div(z, z', z'') -{ 0 }-> div(1 + z0, 1 + z1, 1 + z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z'' = 1 + z1, z' = 0
   div(z, z', z'') -{ 0 }-> 2 :|: z'' = z0, z0 >= 0, z = 0, z' = 0
   div(z, z', z'') -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z' = 1 + z0, z = 0, z'' = z1
   div(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   divides(z, z') -{ 0 }-> div(z0, z1, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   divides(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   gt(z, z') -{ 0 }-> gt(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   gt(z, z') -{ 0 }-> 2 :|: z = 1 + z0, z0 >= 0, z' = 0
   gt(z, z') -{ 0 }-> 1 :|: z0 >= 0, z = 0, z' = z0
   gt(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

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

(17) 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,[fun4(V1, V, V6, Out)],[V1 >= 0,V >= 0,V6 >= 0]).
eq(start(V1, V, V6),0,[fun5(V1, V, V6, Out)],[V1 >= 0,V >= 0,V6 >= 0]).
eq(start(V1, V, V6),0,[gt(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[divides(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[div(V1, V, V6, Out)],[V1 >= 0,V >= 0,V6 >= 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,[fun2(V5, V4, V4, Ret11)],[Out = 1 + Ret11,V1 = V5,V4 >= 0,V = V4,V5 >= 0]).
eq(fun2(V1, V, V6, Out),1,[fun2(1 + V8, 1 + V7, 1 + V7, Ret12)],[Out = 1 + Ret12,V7 >= 0,V1 = 1 + V8,V8 >= 0,V6 = 1 + V7,V = 0]).
eq(fun2(V1, V, V6, Out),1,[fun2(V9, V10, V11, Ret13)],[Out = 1 + Ret13,V6 = V11,V10 >= 0,V1 = 1 + V9,V9 >= 0,V = 1 + V10,V11 >= 0]).
eq(fun3(V1, V, Out),1,[gt(V13, V12, Ret010),fun4(Ret010, V13, V12, Ret01),fun(V13, V12, Ret14)],[Out = 1 + Ret01 + Ret14,V1 = V13,V12 >= 0,V = V12,V13 >= 0]).
eq(fun4(V1, V, V6, Out),1,[divides(V15, V14, Ret0101),fun5(Ret0101, V15, V14, Ret011),fun1(V15, V14, Ret15)],[Out = 1 + Ret011 + Ret15,V1 = 2,V14 >= 0,V15 >= 0,V = V15,V6 = V14]).
eq(fun5(V1, V, V6, Out),1,[fun3(V17, 1 + V16, Ret16)],[Out = 1 + Ret16,V16 >= 0,V1 = 1,V17 >= 0,V = V17,V6 = V16]).
eq(gt(V1, V, Out),0,[],[Out = 2,V1 = 1 + V18,V18 >= 0,V = 0]).
eq(gt(V1, V, Out),0,[],[Out = 1,V19 >= 0,V1 = 0,V = V19]).
eq(gt(V1, V, Out),0,[gt(V20, V21, Ret)],[Out = Ret,V21 >= 0,V1 = 1 + V20,V20 >= 0,V = 1 + V21]).
eq(divides(V1, V, Out),0,[div(V22, V23, V23, Ret2)],[Out = Ret2,V1 = V22,V23 >= 0,V = V23,V22 >= 0]).
eq(div(V1, V, V6, Out),0,[],[Out = 2,V6 = V24,V24 >= 0,V1 = 0,V = 0]).
eq(div(V1, V, V6, Out),0,[],[Out = 1,V26 >= 0,V25 >= 0,V = 1 + V25,V1 = 0,V6 = V26]).
eq(div(V1, V, V6, Out),0,[div(V28, V29, V27, Ret3)],[Out = Ret3,V6 = V27,V29 >= 0,V1 = 1 + V28,V28 >= 0,V = 1 + V29,V27 >= 0]).
eq(div(V1, V, V6, Out),0,[div(1 + V31, 1 + V30, 1 + V30, Ret4)],[Out = Ret4,V30 >= 0,V1 = 1 + V31,V31 >= 0,V6 = 1 + V30,V = 0]).
eq(gt(V1, V, Out),0,[],[Out = 0,V33 >= 0,V32 >= 0,V1 = V33,V = V32]).
eq(divides(V1, V, Out),0,[],[Out = 0,V35 >= 0,V34 >= 0,V1 = V35,V = V34]).
eq(div(V1, V, V6, Out),0,[],[Out = 0,V37 >= 0,V6 = V38,V36 >= 0,V1 = V37,V = V36,V38 >= 0]).
eq(fun(V1, V, Out),0,[],[Out = 0,V39 >= 0,V40 >= 0,V1 = V39,V = V40]).
eq(fun2(V1, V, V6, Out),0,[],[Out = 0,V42 >= 0,V6 = V43,V41 >= 0,V1 = V42,V = V41,V43 >= 0]).
eq(fun4(V1, V, V6, Out),0,[],[Out = 0,V45 >= 0,V6 = V46,V44 >= 0,V1 = V45,V = V44,V46 >= 0]).
eq(fun5(V1, V, V6, Out),0,[],[Out = 0,V48 >= 0,V6 = V49,V47 >= 0,V1 = V48,V = V47,V49 >= 0]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,V,V6,Out),[V1,V,V6],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun4(V1,V,V6,Out),[V1,V,V6],[Out]).
input_output_vars(fun5(V1,V,V6,Out),[V1,V,V6],[Out]).
input_output_vars(gt(V1,V,Out),[V1,V],[Out]).
input_output_vars(divides(V1,V,Out),[V1,V],[Out]).
input_output_vars(div(V1,V,V6,Out),[V1,V,V6],[Out]).


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

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

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into (div)/4
1. SCC is partially evaluated into divides/3
2. SCC is partially evaluated into fun/3
3. SCC is partially evaluated into fun2/4
4. SCC is completely evaluated into other SCCs
5. SCC is partially evaluated into gt/3
6. SCC is partially evaluated into fun3/3
7. SCC is partially evaluated into start/3

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

### Specialization of cost equations (div)/4 
* CE 30 is refined into CE [31] 
* CE 27 is refined into CE [32] 
* CE 26 is refined into CE [33] 
* CE 28 is refined into CE [34] 
* CE 29 is refined into CE [35] 


### Cost equations --> "Loop" of (div)/4 
* CEs [34] --> Loop 20 
* CEs [35] --> Loop 21 
* CEs [31] --> Loop 22 
* CEs [32] --> Loop 23 
* CEs [33] --> Loop 24 

### Ranking functions of CR div(V1,V,V6,Out) 

#### Partial ranking functions of CR div(V1,V,V6,Out) 
* Partial RF of phase [20,21]:
  - RF of loop [20:1]:
    V depends on loops [21:1] 
    V1
  - RF of loop [21:1]:
    -V+1 depends on loops [20:1] 


### Specialization of cost equations divides/3 
* CE 12 is refined into CE [36,37,38,39,40] 
* CE 13 is refined into CE [41] 


### Cost equations --> "Loop" of divides/3 
* CEs [40] --> Loop 25 
* CEs [39] --> Loop 26 
* CEs [38,41] --> Loop 27 
* CEs [37] --> Loop 28 
* CEs [36] --> Loop 29 

### Ranking functions of CR divides(V1,V,Out) 

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


### Specialization of cost equations fun/3 
* CE 21 is refined into CE [42] 
* CE 20 is refined into CE [43] 


### Cost equations --> "Loop" of fun/3 
* CEs [43] --> Loop 30 
* CEs [42] --> Loop 31 

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

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


### Specialization of cost equations fun2/4 
* CE 19 is refined into CE [44] 
* CE 18 is refined into CE [45] 
* CE 17 is refined into CE [46] 


### Cost equations --> "Loop" of fun2/4 
* CEs [45] --> Loop 32 
* CEs [46] --> Loop 33 
* CEs [44] --> Loop 34 

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

#### Partial ranking functions of CR fun2(V1,V,V6,Out) 
* Partial RF of phase [32,33]:
  - RF of loop [32:1]:
    V depends on loops [33:1] 
    V1
  - RF of loop [33:1]:
    -V+1 depends on loops [32:1] 


### Specialization of cost equations gt/3 
* CE 25 is refined into CE [47] 
* CE 22 is refined into CE [48] 
* CE 23 is refined into CE [49] 
* CE 24 is refined into CE [50] 


### Cost equations --> "Loop" of gt/3 
* CEs [50] --> Loop 35 
* CEs [47] --> Loop 36 
* CEs [48] --> Loop 37 
* CEs [49] --> Loop 38 

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

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


### Specialization of cost equations fun3/3 
* CE 14 is refined into CE [51,52,53,54,55,56,57,58] 
* CE 16 is refined into CE [59,60,61,62,63,64,65,66,67,68,69,70,71] 
* CE 15 is refined into CE [72,73,74,75] 


### Cost equations --> "Loop" of fun3/3 
* CEs [72] --> Loop 39 
* CEs [73] --> Loop 40 
* CEs [74,75] --> Loop 41 
* CEs [58] --> Loop 42 
* CEs [54,56] --> Loop 43 
* CEs [61,62,63,65,66,67,69,70,71] --> Loop 44 
* CEs [60,64,68] --> Loop 45 
* CEs [59] --> Loop 46 
* CEs [52] --> Loop 47 
* CEs [51,53,55,57] --> Loop 48 

### Ranking functions of CR fun3(V1,V,Out) 
* RF of phase [39,40,41]: [V1-V]

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


### Specialization of cost equations start/3 
* CE 2 is refined into CE [76,77,78,79,80,81,82,83,84] 
* CE 3 is refined into CE [85,86,87,88,89,90,91,92] 
* CE 1 is refined into CE [93] 
* CE 4 is refined into CE [94,95,96,97] 
* CE 5 is refined into CE [98,99] 
* CE 6 is refined into CE [100,101] 
* CE 7 is refined into CE [102,103] 
* CE 8 is refined into CE [104,105,106,107,108] 
* CE 9 is refined into CE [109,110,111,112,113] 
* CE 10 is refined into CE [114,115,116,117,118] 
* CE 11 is refined into CE [119,120,121,122,123] 


### Cost equations --> "Loop" of start/3 
* CEs [76,86,105,110] --> Loop 49 
* CEs [77,78,79,80,81,82,83,84,85,87,88,89,90,91,92] --> Loop 50 
* CEs [94,95,96,97] --> Loop 51 
* CEs [93,98,99,100,101,102,103,104,106,107,108,109,111,112,113,114,115,116,117,118,119,120,121,122,123] --> Loop 52 

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

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


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

#### Cost of chains of div(V1,V,V6,Out):
* Chain [[20,21],24]: 0
  with precondition: [Out=2,V1>=1,V>=0,V6>=0,V1>=V,V+V6>=1] 

* Chain [[20,21],23]: 0
  with precondition: [Out=1,V1>=1,V>=0,V6>=0,V+V6>=1] 

* Chain [[20,21],22]: 0
  with precondition: [Out=0,V1>=1,V>=0,V6>=0,V+V6>=1] 

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

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

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


#### Cost of chains of divides(V1,V,Out):
* Chain [29]: 0
  with precondition: [V1=0,V=0,Out=2] 

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

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

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

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


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

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

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


#### Cost of chains of fun2(V1,V,V6,Out):
* Chain [[32,33],34]: 1*it(32)+1*it(33)+0
  Such that:it(32) =< V1
aux(15) =< -V+1
it(33) =< it(32)+aux(15)

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

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


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

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

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

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

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

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


#### Cost of chains of fun3(V1,V,Out):
* Chain [[39,40,41],48]: 12*it(39)+1*s(15)+2*s(16)+2*s(17)+1*s(18)+1
  Such that:aux(26) =< V1
s(19) =< -V+1
aux(29) =< V1-V
s(19) =< aux(29)
it(39) =< aux(29)
aux(25) =< aux(26)
s(20) =< it(39)*aux(26)
s(15) =< it(39)*aux(26)
s(18) =< it(39)*aux(25)
s(16) =< s(20)
s(17) =< s(16)+s(19)

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

* Chain [[39,40,41],45]: 12*it(39)+1*s(15)+2*s(16)+2*s(17)+1*s(18)+3
  Such that:aux(26) =< V1
s(19) =< -V+1
aux(30) =< V1-V
s(19) =< aux(30)
it(39) =< aux(30)
aux(25) =< aux(26)
s(20) =< it(39)*aux(26)
s(15) =< it(39)*aux(26)
s(18) =< it(39)*aux(25)
s(16) =< s(20)
s(17) =< s(16)+s(19)

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

* Chain [[39,40,41],44]: 12*it(39)+1*s(15)+2*s(16)+2*s(17)+1*s(18)+12*s(21)+6*s(24)+3
  Such that:aux(32) =< -V
s(19) =< -V+1
aux(34) =< V1
aux(35) =< V1-V
s(19) =< aux(35)
s(21) =< aux(34)
s(24) =< s(21)+aux(32)
it(39) =< aux(35)
aux(25) =< aux(34)
s(20) =< it(39)*aux(34)
s(15) =< it(39)*aux(34)
s(18) =< it(39)*aux(25)
s(16) =< s(20)
s(17) =< s(16)+s(19)

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

* Chain [[39,40,41],43]: 12*it(39)+1*s(15)+2*s(16)+2*s(17)+1*s(18)+2*s(45)+1
  Such that:s(19) =< -V+1
aux(36) =< V1
aux(37) =< V1-V
s(45) =< aux(36)
s(19) =< aux(37)
it(39) =< aux(37)
aux(25) =< aux(36)
s(20) =< it(39)*aux(36)
s(15) =< it(39)*aux(36)
s(18) =< it(39)*aux(25)
s(16) =< s(20)
s(17) =< s(16)+s(19)

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

* Chain [[39,40,41],42]: 12*it(39)+1*s(15)+2*s(16)+2*s(17)+1*s(18)+1*s(47)+1
  Such that:s(19) =< -V+1
aux(38) =< V1
aux(39) =< V1-V
s(47) =< aux(38)
s(19) =< aux(39)
it(39) =< aux(39)
aux(25) =< aux(38)
s(20) =< it(39)*aux(38)
s(15) =< it(39)*aux(38)
s(18) =< it(39)*aux(25)
s(16) =< s(20)
s(17) =< s(16)+s(19)

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

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

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

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

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

* Chain [44]: 6*s(21)+6*s(22)+6*s(24)+3
  Such that:aux(31) =< V1
aux(32) =< -V+1
aux(33) =< V
s(22) =< aux(31)
s(21) =< aux(33)
s(24) =< s(22)+aux(32)

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

* Chain [43]: 1*s(45)+1*s(46)+1
  Such that:s(46) =< V1
s(45) =< V

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

* Chain [42]: 1*s(47)+1
  Such that:s(47) =< V

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


#### Cost of chains of start(V1,V,V6):
* Chain [52]: 9*s(112)+24*s(113)+8*s(115)+60*s(128)+5*s(131)+5*s(132)+10*s(133)+10*s(134)+6*s(135)+3
  Such that:s(122) =< V1-V
s(119) =< -V
aux(44) =< V1
aux(45) =< -V+1
aux(46) =< V
s(113) =< aux(44)
s(112) =< aux(46)
s(115) =< s(113)+aux(45)
s(124) =< aux(45)
s(124) =< s(122)
s(128) =< s(122)
s(129) =< aux(44)
s(130) =< s(128)*aux(44)
s(131) =< s(128)*aux(44)
s(132) =< s(128)*s(129)
s(133) =< s(130)
s(134) =< s(133)+s(124)
s(135) =< s(113)+s(119)

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

* Chain [51]: 22*s(145)+8*s(146)+12*s(147)+60*s(148)+5*s(151)+5*s(152)+10*s(153)+10*s(154)+4
  Such that:s(142) =< V-V6
aux(47) =< -V6
aux(48) =< V
aux(49) =< V6+1
s(145) =< aux(48)
s(144) =< aux(47)
s(146) =< aux(49)
s(147) =< s(145)+aux(47)
s(144) =< s(142)
s(148) =< s(142)
s(149) =< aux(48)
s(150) =< s(148)*aux(48)
s(151) =< s(148)*aux(48)
s(152) =< s(148)*s(149)
s(153) =< s(150)
s(154) =< s(153)+s(144)

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

* Chain [50]: 51*s(159)+7*s(161)+16*s(172)+24*s(173)+120*s(174)+10*s(177)+10*s(178)+20*s(179)+20*s(180)+6
  Such that:aux(54) =< V
aux(55) =< V-V6
aux(56) =< -V6
aux(57) =< -V6+1
aux(58) =< V6+1
s(159) =< aux(54)
s(161) =< s(159)+aux(57)
s(170) =< aux(56)
s(172) =< aux(58)
s(173) =< s(159)+aux(56)
s(170) =< aux(55)
s(174) =< aux(55)
s(175) =< aux(54)
s(176) =< s(174)*aux(54)
s(177) =< s(174)*aux(54)
s(178) =< s(174)*s(175)
s(179) =< s(176)
s(180) =< s(179)+s(170)

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

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


Closed-form bounds of start(V1,V,V6): 
-------------------------------------
* Chain [52] with precondition: [V1>=0,V>=0] 
    - Upper bound: 38*V1+3+30*V1*nat(V1-V)+9*V+nat(-V+1)*18+nat(V1-V)*60 
    - Complexity: n^2 
* Chain [51] with precondition: [V1=1,V>=0,V6>=0] 
    - Upper bound: 34*V+4+30*V*nat(V-V6)+(8*V6+8)+nat(V-V6)*60 
    - Complexity: n^2 
* Chain [50] with precondition: [V1=2,V>=0,V6>=0] 
    - Upper bound: 82*V+6+60*V*nat(V-V6)+(16*V6+16)+nat(-V6+1)*7+nat(V-V6)*120 
    - Complexity: n^2 
* Chain [49] with precondition: [V=0,V1>=1] 
    - Upper bound: 4 
    - Complexity: constant 

### Maximum cost of start(V1,V,V6): max([1,9*V+max([30*V1*nat(V1-V)+38*V1+nat(-V+1)*18+nat(V1-V)*60,48*V+2+30*V*nat(V-V6)+nat(V6+1)*8+nat(-V6+1)*7+nat(V-V6)*60+(25*V+1+30*V*nat(V-V6)+nat(V6+1)*8+nat(V-V6)*60)])])+3 
Asymptotic class: n^2 
* Total analysis performed in 905 ms.


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

(18)
BOUNDS(1, n^2)

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

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

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   gt(s(z0), 0) -> true
   gt(0, z0) -> false
   gt(s(z0), s(z1)) -> gt(z0, z1)
   divides(z0, z1) -> div(z0, z1, z1)
   div(0, 0, z0) -> true
   div(0, s(z0), z1) -> false
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1))
   div(s(z0), s(z1), z2) -> div(z0, z1, z2)
   prime(z0) -> test(z0, s(s(0)))
   test(z0, z1) -> if1(gt(z0, z1), z0, z1)
   if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
   if1(false, z0, z1) -> true
   if2(true, z0, z1) -> false
   if2(false, z0, z1) -> test(z0, s(z1))
Tuples:
   GT(s(z0), 0) -> c
   GT(0, z0) -> c1
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(0, 0, z0) -> c4
   DIV(0, s(z0), z1) -> c5
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   PRIME(z0) -> c8(TEST(z0, s(s(0))))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF1(false, z0, z1) -> c11
   IF2(true, z0, z1) -> c12
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
S tuples:
   GT(s(z0), 0) -> c
   GT(0, z0) -> c1
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(0, 0, z0) -> c4
   DIV(0, s(z0), z1) -> c5
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   PRIME(z0) -> c8(TEST(z0, s(s(0))))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF1(false, z0, z1) -> c11
   IF2(true, z0, z1) -> c12
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
K tuples:none
Defined Rule Symbols:   gt_2, divides_2, div_3, prime_1, test_2, if1_3, if2_3

Defined Pair Symbols:   GT_2, DIVIDES_2, DIV_3, PRIME_1, TEST_2, IF1_3, IF2_3

Compound Symbols:   c, c1, c2_1, c3_1, c4, c5, c6_1, c7_1, c8_1, c9_2, c10_2, c11, c12, c13_1


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

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

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

   GT(s(z0), 0) -> c
   GT(0, z0) -> c1
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(0, 0, z0) -> c4
   DIV(0, s(z0), z1) -> c5
   DIV(s(z0), 0, s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   PRIME(z0) -> c8(TEST(z0, s(s(0))))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF1(false, z0, z1) -> c11
   IF2(true, z0, z1) -> c12
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))

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

   gt(s(z0), 0) -> true
   gt(0, z0) -> false
   gt(s(z0), s(z1)) -> gt(z0, z1)
   divides(z0, z1) -> div(z0, z1, z1)
   div(0, 0, z0) -> true
   div(0, s(z0), z1) -> false
   div(s(z0), 0, s(z1)) -> div(s(z0), s(z1), s(z1))
   div(s(z0), s(z1), z2) -> div(z0, z1, z2)
   prime(z0) -> test(z0, s(s(0)))
   test(z0, z1) -> if1(gt(z0, z1), z0, z1)
   if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
   if1(false, z0, z1) -> true
   if2(true, z0, z1) -> false
   if2(false, z0, z1) -> test(z0, s(z1))

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

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

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

   GT(s(z0), 0') -> c
   GT(0', z0) -> c1
   GT(s(z0), s(z1)) -> c2(GT(z0, z1))
   DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
   DIV(0', 0', z0) -> c4
   DIV(0', s(z0), z1) -> c5
   DIV(s(z0), 0', s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
   DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
   PRIME(z0) -> c8(TEST(z0, s(s(0'))))
   TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
   IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
   IF1(false, z0, z1) -> c11
   IF2(true, z0, z1) -> c12
   IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))

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

   gt(s(z0), 0') -> true
   gt(0', z0) -> false
   gt(s(z0), s(z1)) -> gt(z0, z1)
   divides(z0, z1) -> div(z0, z1, z1)
   div(0', 0', z0) -> true
   div(0', s(z0), z1) -> false
   div(s(z0), 0', s(z1)) -> div(s(z0), s(z1), s(z1))
   div(s(z0), s(z1), z2) -> div(z0, z1, z2)
   prime(z0) -> test(z0, s(s(0')))
   test(z0, z1) -> if1(gt(z0, z1), z0, z1)
   if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
   if1(false, z0, z1) -> true
   if2(true, z0, z1) -> false
   if2(false, z0, z1) -> test(z0, s(z1))

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

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

(26)
Obligation:
Innermost TRS:
Rules:
GT(s(z0), 0') -> c
GT(0', z0) -> c1
GT(s(z0), s(z1)) -> c2(GT(z0, z1))
DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
DIV(0', 0', z0) -> c4
DIV(0', s(z0), z1) -> c5
DIV(s(z0), 0', s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
PRIME(z0) -> c8(TEST(z0, s(s(0'))))
TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
IF1(false, z0, z1) -> c11
IF2(true, z0, z1) -> c12
IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
gt(s(z0), 0') -> true
gt(0', z0) -> false
gt(s(z0), s(z1)) -> gt(z0, z1)
divides(z0, z1) -> div(z0, z1, z1)
div(0', 0', z0) -> true
div(0', s(z0), z1) -> false
div(s(z0), 0', s(z1)) -> div(s(z0), s(z1), s(z1))
div(s(z0), s(z1), z2) -> div(z0, z1, z2)
prime(z0) -> test(z0, s(s(0')))
test(z0, z1) -> if1(gt(z0, z1), z0, z1)
if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
if1(false, z0, z1) -> true
if2(true, z0, z1) -> false
if2(false, z0, z1) -> test(z0, s(z1))

Types:
GT :: s:0' -> s:0' -> c:c1:c2
s :: s:0' -> s:0'
0' :: s:0'
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DIVIDES :: s:0' -> s:0' -> c3
c3 :: c4:c5:c6:c7 -> c3
DIV :: s:0' -> s:0' -> s:0' -> c4:c5:c6:c7
c4 :: c4:c5:c6:c7
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7 -> c4:c5:c6:c7
c7 :: c4:c5:c6:c7 -> c4:c5:c6:c7
PRIME :: s:0' -> c8
c8 :: c9 -> c8
TEST :: s:0' -> s:0' -> c9
c9 :: c10:c11 -> c:c1:c2 -> c9
IF1 :: true:false -> s:0' -> s:0' -> c10:c11
gt :: s:0' -> s:0' -> true:false
true :: true:false
c10 :: c12:c13 -> c3 -> c10:c11
IF2 :: true:false -> s:0' -> s:0' -> c12:c13
divides :: s:0' -> s:0' -> true:false
false :: true:false
c11 :: c10:c11
c12 :: c12:c13
c13 :: c9 -> c12:c13
div :: s:0' -> s:0' -> s:0' -> true:false
prime :: s:0' -> true:false
test :: s:0' -> s:0' -> true:false
if1 :: true:false -> s:0' -> s:0' -> true:false
if2 :: true:false -> s:0' -> s:0' -> true:false
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0'2_14 :: s:0'
hole_c33_14 :: c3
hole_c4:c5:c6:c74_14 :: c4:c5:c6:c7
hole_c85_14 :: c8
hole_c96_14 :: c9
hole_c10:c117_14 :: c10:c11
hole_true:false8_14 :: true:false
hole_c12:c139_14 :: c12:c13
gen_c:c1:c210_14 :: Nat -> c:c1:c2
gen_s:0'11_14 :: Nat -> s:0'
gen_c4:c5:c6:c712_14 :: Nat -> c4:c5:c6:c7

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

(27) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
GT, DIV, TEST, gt, div, test

They will be analysed ascendingly in the following order:
GT < TEST
gt < TEST
gt < test

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

(28)
Obligation:
Innermost TRS:
Rules:
GT(s(z0), 0') -> c
GT(0', z0) -> c1
GT(s(z0), s(z1)) -> c2(GT(z0, z1))
DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
DIV(0', 0', z0) -> c4
DIV(0', s(z0), z1) -> c5
DIV(s(z0), 0', s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
PRIME(z0) -> c8(TEST(z0, s(s(0'))))
TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
IF1(false, z0, z1) -> c11
IF2(true, z0, z1) -> c12
IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
gt(s(z0), 0') -> true
gt(0', z0) -> false
gt(s(z0), s(z1)) -> gt(z0, z1)
divides(z0, z1) -> div(z0, z1, z1)
div(0', 0', z0) -> true
div(0', s(z0), z1) -> false
div(s(z0), 0', s(z1)) -> div(s(z0), s(z1), s(z1))
div(s(z0), s(z1), z2) -> div(z0, z1, z2)
prime(z0) -> test(z0, s(s(0')))
test(z0, z1) -> if1(gt(z0, z1), z0, z1)
if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
if1(false, z0, z1) -> true
if2(true, z0, z1) -> false
if2(false, z0, z1) -> test(z0, s(z1))

Types:
GT :: s:0' -> s:0' -> c:c1:c2
s :: s:0' -> s:0'
0' :: s:0'
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DIVIDES :: s:0' -> s:0' -> c3
c3 :: c4:c5:c6:c7 -> c3
DIV :: s:0' -> s:0' -> s:0' -> c4:c5:c6:c7
c4 :: c4:c5:c6:c7
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7 -> c4:c5:c6:c7
c7 :: c4:c5:c6:c7 -> c4:c5:c6:c7
PRIME :: s:0' -> c8
c8 :: c9 -> c8
TEST :: s:0' -> s:0' -> c9
c9 :: c10:c11 -> c:c1:c2 -> c9
IF1 :: true:false -> s:0' -> s:0' -> c10:c11
gt :: s:0' -> s:0' -> true:false
true :: true:false
c10 :: c12:c13 -> c3 -> c10:c11
IF2 :: true:false -> s:0' -> s:0' -> c12:c13
divides :: s:0' -> s:0' -> true:false
false :: true:false
c11 :: c10:c11
c12 :: c12:c13
c13 :: c9 -> c12:c13
div :: s:0' -> s:0' -> s:0' -> true:false
prime :: s:0' -> true:false
test :: s:0' -> s:0' -> true:false
if1 :: true:false -> s:0' -> s:0' -> true:false
if2 :: true:false -> s:0' -> s:0' -> true:false
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0'2_14 :: s:0'
hole_c33_14 :: c3
hole_c4:c5:c6:c74_14 :: c4:c5:c6:c7
hole_c85_14 :: c8
hole_c96_14 :: c9
hole_c10:c117_14 :: c10:c11
hole_true:false8_14 :: true:false
hole_c12:c139_14 :: c12:c13
gen_c:c1:c210_14 :: Nat -> c:c1:c2
gen_s:0'11_14 :: Nat -> s:0'
gen_c4:c5:c6:c712_14 :: Nat -> c4:c5:c6:c7


Generator Equations:
gen_c:c1:c210_14(0) <=> c
gen_c:c1:c210_14(+(x, 1)) <=> c2(gen_c:c1:c210_14(x))
gen_s:0'11_14(0) <=> 0'
gen_s:0'11_14(+(x, 1)) <=> s(gen_s:0'11_14(x))
gen_c4:c5:c6:c712_14(0) <=> c4
gen_c4:c5:c6:c712_14(+(x, 1)) <=> c6(gen_c4:c5:c6:c712_14(x))


The following defined symbols remain to be analysed:
GT, DIV, TEST, gt, div, test

They will be analysed ascendingly in the following order:
GT < TEST
gt < TEST
gt < test

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GT(gen_s:0'11_14(+(1, n14_14)), gen_s:0'11_14(n14_14)) -> gen_c:c1:c210_14(n14_14), rt in Omega(1 + n14_14)

Induction Base:
GT(gen_s:0'11_14(+(1, 0)), gen_s:0'11_14(0)) ->_R^Omega(1)
c

Induction Step:
GT(gen_s:0'11_14(+(1, +(n14_14, 1))), gen_s:0'11_14(+(n14_14, 1))) ->_R^Omega(1)
c2(GT(gen_s:0'11_14(+(1, n14_14)), gen_s:0'11_14(n14_14))) ->_IH
c2(gen_c:c1:c210_14(c15_14))

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

(30)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
GT(s(z0), 0') -> c
GT(0', z0) -> c1
GT(s(z0), s(z1)) -> c2(GT(z0, z1))
DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
DIV(0', 0', z0) -> c4
DIV(0', s(z0), z1) -> c5
DIV(s(z0), 0', s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
PRIME(z0) -> c8(TEST(z0, s(s(0'))))
TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
IF1(false, z0, z1) -> c11
IF2(true, z0, z1) -> c12
IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
gt(s(z0), 0') -> true
gt(0', z0) -> false
gt(s(z0), s(z1)) -> gt(z0, z1)
divides(z0, z1) -> div(z0, z1, z1)
div(0', 0', z0) -> true
div(0', s(z0), z1) -> false
div(s(z0), 0', s(z1)) -> div(s(z0), s(z1), s(z1))
div(s(z0), s(z1), z2) -> div(z0, z1, z2)
prime(z0) -> test(z0, s(s(0')))
test(z0, z1) -> if1(gt(z0, z1), z0, z1)
if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
if1(false, z0, z1) -> true
if2(true, z0, z1) -> false
if2(false, z0, z1) -> test(z0, s(z1))

Types:
GT :: s:0' -> s:0' -> c:c1:c2
s :: s:0' -> s:0'
0' :: s:0'
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DIVIDES :: s:0' -> s:0' -> c3
c3 :: c4:c5:c6:c7 -> c3
DIV :: s:0' -> s:0' -> s:0' -> c4:c5:c6:c7
c4 :: c4:c5:c6:c7
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7 -> c4:c5:c6:c7
c7 :: c4:c5:c6:c7 -> c4:c5:c6:c7
PRIME :: s:0' -> c8
c8 :: c9 -> c8
TEST :: s:0' -> s:0' -> c9
c9 :: c10:c11 -> c:c1:c2 -> c9
IF1 :: true:false -> s:0' -> s:0' -> c10:c11
gt :: s:0' -> s:0' -> true:false
true :: true:false
c10 :: c12:c13 -> c3 -> c10:c11
IF2 :: true:false -> s:0' -> s:0' -> c12:c13
divides :: s:0' -> s:0' -> true:false
false :: true:false
c11 :: c10:c11
c12 :: c12:c13
c13 :: c9 -> c12:c13
div :: s:0' -> s:0' -> s:0' -> true:false
prime :: s:0' -> true:false
test :: s:0' -> s:0' -> true:false
if1 :: true:false -> s:0' -> s:0' -> true:false
if2 :: true:false -> s:0' -> s:0' -> true:false
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0'2_14 :: s:0'
hole_c33_14 :: c3
hole_c4:c5:c6:c74_14 :: c4:c5:c6:c7
hole_c85_14 :: c8
hole_c96_14 :: c9
hole_c10:c117_14 :: c10:c11
hole_true:false8_14 :: true:false
hole_c12:c139_14 :: c12:c13
gen_c:c1:c210_14 :: Nat -> c:c1:c2
gen_s:0'11_14 :: Nat -> s:0'
gen_c4:c5:c6:c712_14 :: Nat -> c4:c5:c6:c7


Generator Equations:
gen_c:c1:c210_14(0) <=> c
gen_c:c1:c210_14(+(x, 1)) <=> c2(gen_c:c1:c210_14(x))
gen_s:0'11_14(0) <=> 0'
gen_s:0'11_14(+(x, 1)) <=> s(gen_s:0'11_14(x))
gen_c4:c5:c6:c712_14(0) <=> c4
gen_c4:c5:c6:c712_14(+(x, 1)) <=> c6(gen_c4:c5:c6:c712_14(x))


The following defined symbols remain to be analysed:
GT, DIV, TEST, gt, div, test

They will be analysed ascendingly in the following order:
GT < TEST
gt < TEST
gt < test

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

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

(33)
BOUNDS(n^1, INF)

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

(34)
Obligation:
Innermost TRS:
Rules:
GT(s(z0), 0') -> c
GT(0', z0) -> c1
GT(s(z0), s(z1)) -> c2(GT(z0, z1))
DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
DIV(0', 0', z0) -> c4
DIV(0', s(z0), z1) -> c5
DIV(s(z0), 0', s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
PRIME(z0) -> c8(TEST(z0, s(s(0'))))
TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
IF1(false, z0, z1) -> c11
IF2(true, z0, z1) -> c12
IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
gt(s(z0), 0') -> true
gt(0', z0) -> false
gt(s(z0), s(z1)) -> gt(z0, z1)
divides(z0, z1) -> div(z0, z1, z1)
div(0', 0', z0) -> true
div(0', s(z0), z1) -> false
div(s(z0), 0', s(z1)) -> div(s(z0), s(z1), s(z1))
div(s(z0), s(z1), z2) -> div(z0, z1, z2)
prime(z0) -> test(z0, s(s(0')))
test(z0, z1) -> if1(gt(z0, z1), z0, z1)
if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
if1(false, z0, z1) -> true
if2(true, z0, z1) -> false
if2(false, z0, z1) -> test(z0, s(z1))

Types:
GT :: s:0' -> s:0' -> c:c1:c2
s :: s:0' -> s:0'
0' :: s:0'
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DIVIDES :: s:0' -> s:0' -> c3
c3 :: c4:c5:c6:c7 -> c3
DIV :: s:0' -> s:0' -> s:0' -> c4:c5:c6:c7
c4 :: c4:c5:c6:c7
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7 -> c4:c5:c6:c7
c7 :: c4:c5:c6:c7 -> c4:c5:c6:c7
PRIME :: s:0' -> c8
c8 :: c9 -> c8
TEST :: s:0' -> s:0' -> c9
c9 :: c10:c11 -> c:c1:c2 -> c9
IF1 :: true:false -> s:0' -> s:0' -> c10:c11
gt :: s:0' -> s:0' -> true:false
true :: true:false
c10 :: c12:c13 -> c3 -> c10:c11
IF2 :: true:false -> s:0' -> s:0' -> c12:c13
divides :: s:0' -> s:0' -> true:false
false :: true:false
c11 :: c10:c11
c12 :: c12:c13
c13 :: c9 -> c12:c13
div :: s:0' -> s:0' -> s:0' -> true:false
prime :: s:0' -> true:false
test :: s:0' -> s:0' -> true:false
if1 :: true:false -> s:0' -> s:0' -> true:false
if2 :: true:false -> s:0' -> s:0' -> true:false
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0'2_14 :: s:0'
hole_c33_14 :: c3
hole_c4:c5:c6:c74_14 :: c4:c5:c6:c7
hole_c85_14 :: c8
hole_c96_14 :: c9
hole_c10:c117_14 :: c10:c11
hole_true:false8_14 :: true:false
hole_c12:c139_14 :: c12:c13
gen_c:c1:c210_14 :: Nat -> c:c1:c2
gen_s:0'11_14 :: Nat -> s:0'
gen_c4:c5:c6:c712_14 :: Nat -> c4:c5:c6:c7


Lemmas:
GT(gen_s:0'11_14(+(1, n14_14)), gen_s:0'11_14(n14_14)) -> gen_c:c1:c210_14(n14_14), rt in Omega(1 + n14_14)


Generator Equations:
gen_c:c1:c210_14(0) <=> c
gen_c:c1:c210_14(+(x, 1)) <=> c2(gen_c:c1:c210_14(x))
gen_s:0'11_14(0) <=> 0'
gen_s:0'11_14(+(x, 1)) <=> s(gen_s:0'11_14(x))
gen_c4:c5:c6:c712_14(0) <=> c4
gen_c4:c5:c6:c712_14(+(x, 1)) <=> c6(gen_c4:c5:c6:c712_14(x))


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

They will be analysed ascendingly in the following order:
gt < TEST
gt < test

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DIV(gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(c)) -> *13_14, rt in Omega(n604_14)

Induction Base:
DIV(gen_s:0'11_14(+(1, 0)), gen_s:0'11_14(+(1, 0)), gen_s:0'11_14(c))

Induction Step:
DIV(gen_s:0'11_14(+(1, +(n604_14, 1))), gen_s:0'11_14(+(1, +(n604_14, 1))), gen_s:0'11_14(c)) ->_R^Omega(1)
c7(DIV(gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(c))) ->_IH
c7(*13_14)

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

(36)
Obligation:
Innermost TRS:
Rules:
GT(s(z0), 0') -> c
GT(0', z0) -> c1
GT(s(z0), s(z1)) -> c2(GT(z0, z1))
DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
DIV(0', 0', z0) -> c4
DIV(0', s(z0), z1) -> c5
DIV(s(z0), 0', s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
PRIME(z0) -> c8(TEST(z0, s(s(0'))))
TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
IF1(false, z0, z1) -> c11
IF2(true, z0, z1) -> c12
IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
gt(s(z0), 0') -> true
gt(0', z0) -> false
gt(s(z0), s(z1)) -> gt(z0, z1)
divides(z0, z1) -> div(z0, z1, z1)
div(0', 0', z0) -> true
div(0', s(z0), z1) -> false
div(s(z0), 0', s(z1)) -> div(s(z0), s(z1), s(z1))
div(s(z0), s(z1), z2) -> div(z0, z1, z2)
prime(z0) -> test(z0, s(s(0')))
test(z0, z1) -> if1(gt(z0, z1), z0, z1)
if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
if1(false, z0, z1) -> true
if2(true, z0, z1) -> false
if2(false, z0, z1) -> test(z0, s(z1))

Types:
GT :: s:0' -> s:0' -> c:c1:c2
s :: s:0' -> s:0'
0' :: s:0'
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DIVIDES :: s:0' -> s:0' -> c3
c3 :: c4:c5:c6:c7 -> c3
DIV :: s:0' -> s:0' -> s:0' -> c4:c5:c6:c7
c4 :: c4:c5:c6:c7
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7 -> c4:c5:c6:c7
c7 :: c4:c5:c6:c7 -> c4:c5:c6:c7
PRIME :: s:0' -> c8
c8 :: c9 -> c8
TEST :: s:0' -> s:0' -> c9
c9 :: c10:c11 -> c:c1:c2 -> c9
IF1 :: true:false -> s:0' -> s:0' -> c10:c11
gt :: s:0' -> s:0' -> true:false
true :: true:false
c10 :: c12:c13 -> c3 -> c10:c11
IF2 :: true:false -> s:0' -> s:0' -> c12:c13
divides :: s:0' -> s:0' -> true:false
false :: true:false
c11 :: c10:c11
c12 :: c12:c13
c13 :: c9 -> c12:c13
div :: s:0' -> s:0' -> s:0' -> true:false
prime :: s:0' -> true:false
test :: s:0' -> s:0' -> true:false
if1 :: true:false -> s:0' -> s:0' -> true:false
if2 :: true:false -> s:0' -> s:0' -> true:false
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0'2_14 :: s:0'
hole_c33_14 :: c3
hole_c4:c5:c6:c74_14 :: c4:c5:c6:c7
hole_c85_14 :: c8
hole_c96_14 :: c9
hole_c10:c117_14 :: c10:c11
hole_true:false8_14 :: true:false
hole_c12:c139_14 :: c12:c13
gen_c:c1:c210_14 :: Nat -> c:c1:c2
gen_s:0'11_14 :: Nat -> s:0'
gen_c4:c5:c6:c712_14 :: Nat -> c4:c5:c6:c7


Lemmas:
GT(gen_s:0'11_14(+(1, n14_14)), gen_s:0'11_14(n14_14)) -> gen_c:c1:c210_14(n14_14), rt in Omega(1 + n14_14)
DIV(gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(c)) -> *13_14, rt in Omega(n604_14)


Generator Equations:
gen_c:c1:c210_14(0) <=> c
gen_c:c1:c210_14(+(x, 1)) <=> c2(gen_c:c1:c210_14(x))
gen_s:0'11_14(0) <=> 0'
gen_s:0'11_14(+(x, 1)) <=> s(gen_s:0'11_14(x))
gen_c4:c5:c6:c712_14(0) <=> c4
gen_c4:c5:c6:c712_14(+(x, 1)) <=> c6(gen_c4:c5:c6:c712_14(x))


The following defined symbols remain to be analysed:
gt, TEST, div, test

They will be analysed ascendingly in the following order:
gt < TEST
gt < test

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
gt(gen_s:0'11_14(+(1, n5895_14)), gen_s:0'11_14(n5895_14)) -> true, rt in Omega(0)

Induction Base:
gt(gen_s:0'11_14(+(1, 0)), gen_s:0'11_14(0)) ->_R^Omega(0)
true

Induction Step:
gt(gen_s:0'11_14(+(1, +(n5895_14, 1))), gen_s:0'11_14(+(n5895_14, 1))) ->_R^Omega(0)
gt(gen_s:0'11_14(+(1, n5895_14)), gen_s:0'11_14(n5895_14)) ->_IH
true

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

(38)
Obligation:
Innermost TRS:
Rules:
GT(s(z0), 0') -> c
GT(0', z0) -> c1
GT(s(z0), s(z1)) -> c2(GT(z0, z1))
DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
DIV(0', 0', z0) -> c4
DIV(0', s(z0), z1) -> c5
DIV(s(z0), 0', s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
PRIME(z0) -> c8(TEST(z0, s(s(0'))))
TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
IF1(false, z0, z1) -> c11
IF2(true, z0, z1) -> c12
IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
gt(s(z0), 0') -> true
gt(0', z0) -> false
gt(s(z0), s(z1)) -> gt(z0, z1)
divides(z0, z1) -> div(z0, z1, z1)
div(0', 0', z0) -> true
div(0', s(z0), z1) -> false
div(s(z0), 0', s(z1)) -> div(s(z0), s(z1), s(z1))
div(s(z0), s(z1), z2) -> div(z0, z1, z2)
prime(z0) -> test(z0, s(s(0')))
test(z0, z1) -> if1(gt(z0, z1), z0, z1)
if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
if1(false, z0, z1) -> true
if2(true, z0, z1) -> false
if2(false, z0, z1) -> test(z0, s(z1))

Types:
GT :: s:0' -> s:0' -> c:c1:c2
s :: s:0' -> s:0'
0' :: s:0'
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DIVIDES :: s:0' -> s:0' -> c3
c3 :: c4:c5:c6:c7 -> c3
DIV :: s:0' -> s:0' -> s:0' -> c4:c5:c6:c7
c4 :: c4:c5:c6:c7
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7 -> c4:c5:c6:c7
c7 :: c4:c5:c6:c7 -> c4:c5:c6:c7
PRIME :: s:0' -> c8
c8 :: c9 -> c8
TEST :: s:0' -> s:0' -> c9
c9 :: c10:c11 -> c:c1:c2 -> c9
IF1 :: true:false -> s:0' -> s:0' -> c10:c11
gt :: s:0' -> s:0' -> true:false
true :: true:false
c10 :: c12:c13 -> c3 -> c10:c11
IF2 :: true:false -> s:0' -> s:0' -> c12:c13
divides :: s:0' -> s:0' -> true:false
false :: true:false
c11 :: c10:c11
c12 :: c12:c13
c13 :: c9 -> c12:c13
div :: s:0' -> s:0' -> s:0' -> true:false
prime :: s:0' -> true:false
test :: s:0' -> s:0' -> true:false
if1 :: true:false -> s:0' -> s:0' -> true:false
if2 :: true:false -> s:0' -> s:0' -> true:false
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0'2_14 :: s:0'
hole_c33_14 :: c3
hole_c4:c5:c6:c74_14 :: c4:c5:c6:c7
hole_c85_14 :: c8
hole_c96_14 :: c9
hole_c10:c117_14 :: c10:c11
hole_true:false8_14 :: true:false
hole_c12:c139_14 :: c12:c13
gen_c:c1:c210_14 :: Nat -> c:c1:c2
gen_s:0'11_14 :: Nat -> s:0'
gen_c4:c5:c6:c712_14 :: Nat -> c4:c5:c6:c7


Lemmas:
GT(gen_s:0'11_14(+(1, n14_14)), gen_s:0'11_14(n14_14)) -> gen_c:c1:c210_14(n14_14), rt in Omega(1 + n14_14)
DIV(gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(c)) -> *13_14, rt in Omega(n604_14)
gt(gen_s:0'11_14(+(1, n5895_14)), gen_s:0'11_14(n5895_14)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c210_14(0) <=> c
gen_c:c1:c210_14(+(x, 1)) <=> c2(gen_c:c1:c210_14(x))
gen_s:0'11_14(0) <=> 0'
gen_s:0'11_14(+(x, 1)) <=> s(gen_s:0'11_14(x))
gen_c4:c5:c6:c712_14(0) <=> c4
gen_c4:c5:c6:c712_14(+(x, 1)) <=> c6(gen_c4:c5:c6:c712_14(x))


The following defined symbols remain to be analysed:
TEST, div, test
----------------------------------------

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
div(gen_s:0'11_14(n38449_14), gen_s:0'11_14(n38449_14), gen_s:0'11_14(c)) -> true, rt in Omega(0)

Induction Base:
div(gen_s:0'11_14(0), gen_s:0'11_14(0), gen_s:0'11_14(c)) ->_R^Omega(0)
true

Induction Step:
div(gen_s:0'11_14(+(n38449_14, 1)), gen_s:0'11_14(+(n38449_14, 1)), gen_s:0'11_14(c)) ->_R^Omega(0)
div(gen_s:0'11_14(n38449_14), gen_s:0'11_14(n38449_14), gen_s:0'11_14(c)) ->_IH
true

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:
GT(s(z0), 0') -> c
GT(0', z0) -> c1
GT(s(z0), s(z1)) -> c2(GT(z0, z1))
DIVIDES(z0, z1) -> c3(DIV(z0, z1, z1))
DIV(0', 0', z0) -> c4
DIV(0', s(z0), z1) -> c5
DIV(s(z0), 0', s(z1)) -> c6(DIV(s(z0), s(z1), s(z1)))
DIV(s(z0), s(z1), z2) -> c7(DIV(z0, z1, z2))
PRIME(z0) -> c8(TEST(z0, s(s(0'))))
TEST(z0, z1) -> c9(IF1(gt(z0, z1), z0, z1), GT(z0, z1))
IF1(true, z0, z1) -> c10(IF2(divides(z0, z1), z0, z1), DIVIDES(z0, z1))
IF1(false, z0, z1) -> c11
IF2(true, z0, z1) -> c12
IF2(false, z0, z1) -> c13(TEST(z0, s(z1)))
gt(s(z0), 0') -> true
gt(0', z0) -> false
gt(s(z0), s(z1)) -> gt(z0, z1)
divides(z0, z1) -> div(z0, z1, z1)
div(0', 0', z0) -> true
div(0', s(z0), z1) -> false
div(s(z0), 0', s(z1)) -> div(s(z0), s(z1), s(z1))
div(s(z0), s(z1), z2) -> div(z0, z1, z2)
prime(z0) -> test(z0, s(s(0')))
test(z0, z1) -> if1(gt(z0, z1), z0, z1)
if1(true, z0, z1) -> if2(divides(z0, z1), z0, z1)
if1(false, z0, z1) -> true
if2(true, z0, z1) -> false
if2(false, z0, z1) -> test(z0, s(z1))

Types:
GT :: s:0' -> s:0' -> c:c1:c2
s :: s:0' -> s:0'
0' :: s:0'
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
DIVIDES :: s:0' -> s:0' -> c3
c3 :: c4:c5:c6:c7 -> c3
DIV :: s:0' -> s:0' -> s:0' -> c4:c5:c6:c7
c4 :: c4:c5:c6:c7
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7 -> c4:c5:c6:c7
c7 :: c4:c5:c6:c7 -> c4:c5:c6:c7
PRIME :: s:0' -> c8
c8 :: c9 -> c8
TEST :: s:0' -> s:0' -> c9
c9 :: c10:c11 -> c:c1:c2 -> c9
IF1 :: true:false -> s:0' -> s:0' -> c10:c11
gt :: s:0' -> s:0' -> true:false
true :: true:false
c10 :: c12:c13 -> c3 -> c10:c11
IF2 :: true:false -> s:0' -> s:0' -> c12:c13
divides :: s:0' -> s:0' -> true:false
false :: true:false
c11 :: c10:c11
c12 :: c12:c13
c13 :: c9 -> c12:c13
div :: s:0' -> s:0' -> s:0' -> true:false
prime :: s:0' -> true:false
test :: s:0' -> s:0' -> true:false
if1 :: true:false -> s:0' -> s:0' -> true:false
if2 :: true:false -> s:0' -> s:0' -> true:false
hole_c:c1:c21_14 :: c:c1:c2
hole_s:0'2_14 :: s:0'
hole_c33_14 :: c3
hole_c4:c5:c6:c74_14 :: c4:c5:c6:c7
hole_c85_14 :: c8
hole_c96_14 :: c9
hole_c10:c117_14 :: c10:c11
hole_true:false8_14 :: true:false
hole_c12:c139_14 :: c12:c13
gen_c:c1:c210_14 :: Nat -> c:c1:c2
gen_s:0'11_14 :: Nat -> s:0'
gen_c4:c5:c6:c712_14 :: Nat -> c4:c5:c6:c7


Lemmas:
GT(gen_s:0'11_14(+(1, n14_14)), gen_s:0'11_14(n14_14)) -> gen_c:c1:c210_14(n14_14), rt in Omega(1 + n14_14)
DIV(gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(+(1, n604_14)), gen_s:0'11_14(c)) -> *13_14, rt in Omega(n604_14)
gt(gen_s:0'11_14(+(1, n5895_14)), gen_s:0'11_14(n5895_14)) -> true, rt in Omega(0)
div(gen_s:0'11_14(n38449_14), gen_s:0'11_14(n38449_14), gen_s:0'11_14(c)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c210_14(0) <=> c
gen_c:c1:c210_14(+(x, 1)) <=> c2(gen_c:c1:c210_14(x))
gen_s:0'11_14(0) <=> 0'
gen_s:0'11_14(+(x, 1)) <=> s(gen_s:0'11_14(x))
gen_c4:c5:c6:c712_14(0) <=> c4
gen_c4:c5:c6:c712_14(+(x, 1)) <=> c6(gen_c4:c5:c6:c712_14(x))


The following defined symbols remain to be analysed:
test