WORST_CASE(Omega(n^1),O(n^1))
proof of input_HnxljqWZUl.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 [ComplexityIfPolyImplication, 0 ms]
    (4) CdtProblem
    (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxTRS
    (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, 1018 ms]
    (18) BOUNDS(1, n^1)
(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), 9 ms]
    (28) typed CpxTrs
    (29) RewriteLemmaProof [LOWER BOUND(ID), 491 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), 138 ms]
            (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 157 ms]
            (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 159 ms]
            (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 135 ms]
            (42) typed CpxTrs
            (43) RewriteLemmaProof [LOWER BOUND(ID), 210 ms]
            (44) 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:

   f_0(x) -> a
   f_1(x) -> g_1(x, x)
   g_1(s(x), y) -> b(f_0(y), g_1(x, y))
   f_2(x) -> g_2(x, x)
   g_2(s(x), y) -> b(f_1(y), g_2(x, y))
   f_3(x) -> g_3(x, x)
   g_3(s(x), y) -> b(f_2(y), g_3(x, y))
   f_4(x) -> g_4(x, x)
   g_4(s(x), y) -> b(f_3(y), g_4(x, y))
   f_5(x) -> g_5(x, x)
   g_5(s(x), y) -> b(f_4(y), g_5(x, 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:
   f_0(z0) -> a
   f_1(z0) -> g_1(z0, z0)
   g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
   f_2(z0) -> g_2(z0, z0)
   g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
   f_3(z0) -> g_3(z0, z0)
   g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
   f_4(z0) -> g_4(z0, z0)
   g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
   f_5(z0) -> g_5(z0, z0)
   g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))
Tuples:
   F_0(z0) -> c
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c2(F_0(z1))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   F_5(z0) -> c13(G_5(z0, z0))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))
S tuples:
   F_0(z0) -> c
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c2(F_0(z1))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   F_5(z0) -> c13(G_5(z0, z0))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))
K tuples:none
Defined Rule Symbols:   f_0_1, f_1_1, g_1_2, f_2_1, g_2_2, f_3_1, g_3_2, f_4_1, g_4_2, f_5_1, g_5_2

Defined Pair Symbols:   F_0_1, F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, F_5_1, G_5_2

Compound Symbols:   c, c1_1, c2_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c13_1, c14_1, c15_1


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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   F_5(z0) -> c13(G_5(z0, z0))
Removed 2 trailing nodes:
   F_0(z0) -> c
   G_1(s(z0), z1) -> c2(F_0(z1))

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f_0(z0) -> a
   f_1(z0) -> g_1(z0, z0)
   g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
   f_2(z0) -> g_2(z0, z0)
   g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
   f_3(z0) -> g_3(z0, z0)
   g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
   f_4(z0) -> g_4(z0, z0)
   g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
   f_5(z0) -> g_5(z0, z0)
   g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))
Tuples:
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))
S tuples:
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))
K tuples:none
Defined Rule Symbols:   f_0_1, f_1_1, g_1_2, f_2_1, g_2_2, f_3_1, g_3_2, f_4_1, g_4_2, f_5_1, g_5_2

Defined Pair Symbols:   F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2

Compound Symbols:   c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   f_0(z0) -> a
   f_1(z0) -> g_1(z0, z0)
   g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
   f_2(z0) -> g_2(z0, z0)
   g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
   f_3(z0) -> g_3(z0, z0)
   g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
   f_4(z0) -> g_4(z0, z0)
   g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
   f_5(z0) -> g_5(z0, z0)
   g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))
S tuples:
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2

Compound Symbols:   c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_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 CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))

S is empty.
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^1).


The TRS R consists of the following rules:

   F_1(z0) -> c1(G_1(z0, z0)) [1]
   G_1(s(z0), z1) -> c3(G_1(z0, z1)) [1]
   F_2(z0) -> c4(G_2(z0, z0)) [1]
   G_2(s(z0), z1) -> c5(F_1(z1)) [1]
   G_2(s(z0), z1) -> c6(G_2(z0, z1)) [1]
   F_3(z0) -> c7(G_3(z0, z0)) [1]
   G_3(s(z0), z1) -> c8(F_2(z1)) [1]
   G_3(s(z0), z1) -> c9(G_3(z0, z1)) [1]
   F_4(z0) -> c10(G_4(z0, z0)) [1]
   G_4(s(z0), z1) -> c11(F_3(z1)) [1]
   G_4(s(z0), z1) -> c12(G_4(z0, z1)) [1]
   G_5(s(z0), z1) -> c14(F_4(z1)) [1]
   G_5(s(z0), z1) -> c15(G_5(z0, z1)) [1]

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:

   F_1(z0) -> c1(G_1(z0, z0)) [1]
   G_1(s(z0), z1) -> c3(G_1(z0, z1)) [1]
   F_2(z0) -> c4(G_2(z0, z0)) [1]
   G_2(s(z0), z1) -> c5(F_1(z1)) [1]
   G_2(s(z0), z1) -> c6(G_2(z0, z1)) [1]
   F_3(z0) -> c7(G_3(z0, z0)) [1]
   G_3(s(z0), z1) -> c8(F_2(z1)) [1]
   G_3(s(z0), z1) -> c9(G_3(z0, z1)) [1]
   F_4(z0) -> c10(G_4(z0, z0)) [1]
   G_4(s(z0), z1) -> c11(F_3(z1)) [1]
   G_4(s(z0), z1) -> c12(G_4(z0, z1)) [1]
   G_5(s(z0), z1) -> c14(F_4(z1)) [1]
   G_5(s(z0), z1) -> c15(G_5(z0, z1)) [1]

The TRS has the following type information:
F_1 :: s -> c1
c1 :: c3 -> c1
G_1 :: s -> s -> c3
s :: s -> s
c3 :: c3 -> c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15

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:

   G_1(v0, v1) -> null_G_1 [0]
   G_2(v0, v1) -> null_G_2 [0]
   G_3(v0, v1) -> null_G_3 [0]
   G_4(v0, v1) -> null_G_4 [0]
   G_5(v0, v1) -> null_G_5 [0]

And the following fresh constants:    null_G_1, null_G_2, null_G_3, null_G_4, null_G_5, const, const1, const2, const3, const4

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

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

   F_1(z0) -> c1(G_1(z0, z0)) [1]
   G_1(s(z0), z1) -> c3(G_1(z0, z1)) [1]
   F_2(z0) -> c4(G_2(z0, z0)) [1]
   G_2(s(z0), z1) -> c5(F_1(z1)) [1]
   G_2(s(z0), z1) -> c6(G_2(z0, z1)) [1]
   F_3(z0) -> c7(G_3(z0, z0)) [1]
   G_3(s(z0), z1) -> c8(F_2(z1)) [1]
   G_3(s(z0), z1) -> c9(G_3(z0, z1)) [1]
   F_4(z0) -> c10(G_4(z0, z0)) [1]
   G_4(s(z0), z1) -> c11(F_3(z1)) [1]
   G_4(s(z0), z1) -> c12(G_4(z0, z1)) [1]
   G_5(s(z0), z1) -> c14(F_4(z1)) [1]
   G_5(s(z0), z1) -> c15(G_5(z0, z1)) [1]
   G_1(v0, v1) -> null_G_1 [0]
   G_2(v0, v1) -> null_G_2 [0]
   G_3(v0, v1) -> null_G_3 [0]
   G_4(v0, v1) -> null_G_4 [0]
   G_5(v0, v1) -> null_G_5 [0]

The TRS has the following type information:
F_1 :: s -> c1
c1 :: c3:null_G_1 -> c1
G_1 :: s -> s -> c3:null_G_1
s :: s -> s
c3 :: c3:null_G_1 -> c3:null_G_1
F_2 :: s -> c4
c4 :: c5:c6:null_G_2 -> c4
G_2 :: s -> s -> c5:c6:null_G_2
c5 :: c1 -> c5:c6:null_G_2
c6 :: c5:c6:null_G_2 -> c5:c6:null_G_2
F_3 :: s -> c7
c7 :: c8:c9:null_G_3 -> c7
G_3 :: s -> s -> c8:c9:null_G_3
c8 :: c4 -> c8:c9:null_G_3
c9 :: c8:c9:null_G_3 -> c8:c9:null_G_3
F_4 :: s -> c10
c10 :: c11:c12:null_G_4 -> c10
G_4 :: s -> s -> c11:c12:null_G_4
c11 :: c7 -> c11:c12:null_G_4
c12 :: c11:c12:null_G_4 -> c11:c12:null_G_4
G_5 :: s -> s -> c14:c15:null_G_5
c14 :: c10 -> c14:c15:null_G_5
c15 :: c14:c15:null_G_5 -> c14:c15:null_G_5
null_G_1 :: c3:null_G_1
null_G_2 :: c5:c6:null_G_2
null_G_3 :: c8:c9:null_G_3
null_G_4 :: c11:c12:null_G_4
null_G_5 :: c14:c15:null_G_5
const :: c1
const1 :: s
const2 :: c4
const3 :: c7
const4 :: c10

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:

   null_G_1 => 0
   null_G_2 => 0
   null_G_3 => 0
   null_G_4 => 0
   null_G_5 => 0
   const => 0
   const1 => 0
   const2 => 0
   const3 => 0
   const4 => 0

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

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

   F_1(z) -{ 1 }-> 1 + G_1(z0, z0) :|: z = z0, z0 >= 0
   F_2(z) -{ 1 }-> 1 + G_2(z0, z0) :|: z = z0, z0 >= 0
   F_3(z) -{ 1 }-> 1 + G_3(z0, z0) :|: z = z0, z0 >= 0
   F_4(z) -{ 1 }-> 1 + G_4(z0, z0) :|: z = z0, z0 >= 0
   G_1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   G_1(z, z') -{ 1 }-> 1 + G_1(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   G_2(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   G_2(z, z') -{ 1 }-> 1 + G_2(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   G_2(z, z') -{ 1 }-> 1 + F_1(z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   G_3(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   G_3(z, z') -{ 1 }-> 1 + G_3(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   G_3(z, z') -{ 1 }-> 1 + F_2(z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   G_4(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   G_4(z, z') -{ 1 }-> 1 + G_4(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   G_4(z, z') -{ 1 }-> 1 + F_3(z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   G_5(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   G_5(z, z') -{ 1 }-> 1 + G_5(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   G_5(z, z') -{ 1 }-> 1 + F_4(z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0

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(V, V2),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V2),0,[fun1(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2),0,[fun2(V, Out)],[V >= 0]).
eq(start(V, V2),0,[fun3(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2),0,[fun4(V, Out)],[V >= 0]).
eq(start(V, V2),0,[fun5(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2),0,[fun6(V, Out)],[V >= 0]).
eq(start(V, V2),0,[fun7(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(start(V, V2),0,[fun8(V, V2, Out)],[V >= 0,V2 >= 0]).
eq(fun(V, Out),1,[fun1(V1, V1, Ret1)],[Out = 1 + Ret1,V = V1,V1 >= 0]).
eq(fun1(V, V2, Out),1,[fun1(V4, V3, Ret11)],[Out = 1 + Ret11,V3 >= 0,V = 1 + V4,V2 = V3,V4 >= 0]).
eq(fun2(V, Out),1,[fun3(V5, V5, Ret12)],[Out = 1 + Ret12,V = V5,V5 >= 0]).
eq(fun3(V, V2, Out),1,[fun(V7, Ret13)],[Out = 1 + Ret13,V7 >= 0,V = 1 + V6,V2 = V7,V6 >= 0]).
eq(fun3(V, V2, Out),1,[fun3(V8, V9, Ret14)],[Out = 1 + Ret14,V9 >= 0,V = 1 + V8,V2 = V9,V8 >= 0]).
eq(fun4(V, Out),1,[fun5(V10, V10, Ret15)],[Out = 1 + Ret15,V = V10,V10 >= 0]).
eq(fun5(V, V2, Out),1,[fun2(V12, Ret16)],[Out = 1 + Ret16,V12 >= 0,V = 1 + V11,V2 = V12,V11 >= 0]).
eq(fun5(V, V2, Out),1,[fun5(V14, V13, Ret17)],[Out = 1 + Ret17,V13 >= 0,V = 1 + V14,V2 = V13,V14 >= 0]).
eq(fun6(V, Out),1,[fun7(V15, V15, Ret18)],[Out = 1 + Ret18,V = V15,V15 >= 0]).
eq(fun7(V, V2, Out),1,[fun4(V16, Ret19)],[Out = 1 + Ret19,V16 >= 0,V = 1 + V17,V2 = V16,V17 >= 0]).
eq(fun7(V, V2, Out),1,[fun7(V19, V18, Ret110)],[Out = 1 + Ret110,V18 >= 0,V = 1 + V19,V2 = V18,V19 >= 0]).
eq(fun8(V, V2, Out),1,[fun6(V20, Ret111)],[Out = 1 + Ret111,V20 >= 0,V = 1 + V21,V2 = V20,V21 >= 0]).
eq(fun8(V, V2, Out),1,[fun8(V22, V23, Ret112)],[Out = 1 + Ret112,V23 >= 0,V = 1 + V22,V2 = V23,V22 >= 0]).
eq(fun1(V, V2, Out),0,[],[Out = 0,V25 >= 0,V24 >= 0,V = V25,V2 = V24]).
eq(fun3(V, V2, Out),0,[],[Out = 0,V27 >= 0,V26 >= 0,V = V27,V2 = V26]).
eq(fun5(V, V2, Out),0,[],[Out = 0,V29 >= 0,V28 >= 0,V = V29,V2 = V28]).
eq(fun7(V, V2, Out),0,[],[Out = 0,V30 >= 0,V31 >= 0,V = V30,V2 = V31]).
eq(fun8(V, V2, Out),0,[],[Out = 0,V33 >= 0,V32 >= 0,V = V33,V2 = V32]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,V2,Out),[V,V2],[Out]).
input_output_vars(fun2(V,Out),[V],[Out]).
input_output_vars(fun3(V,V2,Out),[V,V2],[Out]).
input_output_vars(fun4(V,Out),[V],[Out]).
input_output_vars(fun5(V,V2,Out),[V,V2],[Out]).
input_output_vars(fun6(V,Out),[V],[Out]).
input_output_vars(fun7(V,V2,Out),[V,V2],[Out]).
input_output_vars(fun8(V,V2,Out),[V,V2],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [fun1/3]
1. non_recursive  : [fun/2]
2. recursive  : [fun3/3]
3. non_recursive  : [fun2/2]
4. recursive  : [fun5/3]
5. non_recursive  : [fun4/2]
6. recursive  : [fun7/3]
7. non_recursive  : [fun6/2]
8. recursive  : [fun8/3]
9. non_recursive  : [start/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun1/3
1. SCC is completely evaluated into other SCCs
2. SCC is partially evaluated into fun3/3
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into fun5/3
5. SCC is completely evaluated into other SCCs
6. SCC is partially evaluated into fun7/3
7. SCC is completely evaluated into other SCCs
8. SCC is partially evaluated into fun8/3
9. SCC is partially evaluated into start/2

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

### Specialization of cost equations fun1/3 
* CE 11 is refined into CE [24] 
* CE 10 is refined into CE [25] 


### Cost equations --> "Loop" of fun1/3 
* CEs [25] --> Loop 16 
* CEs [24] --> Loop 17 

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

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


### Specialization of cost equations fun3/3 
* CE 12 is refined into CE [26,27] 
* CE 14 is refined into CE [28] 
* CE 13 is refined into CE [29] 


### Cost equations --> "Loop" of fun3/3 
* CEs [29] --> Loop 18 
* CEs [27] --> Loop 19 
* CEs [26] --> Loop 20 
* CEs [28] --> Loop 21 

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

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


### Specialization of cost equations fun5/3 
* CE 15 is refined into CE [30,31,32,33,34,35] 
* CE 17 is refined into CE [36] 
* CE 16 is refined into CE [37] 


### Cost equations --> "Loop" of fun5/3 
* CEs [37] --> Loop 22 
* CEs [32,35] --> Loop 23 
* CEs [34] --> Loop 24 
* CEs [33] --> Loop 25 
* CEs [31] --> Loop 26 
* CEs [30] --> Loop 27 
* CEs [36] --> Loop 28 

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

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


### Specialization of cost equations fun7/3 
* CE 18 is refined into CE [38,39,40,41,42,43,44,45,46,47,48,49] 
* CE 20 is refined into CE [50] 
* CE 19 is refined into CE [51] 


### Cost equations --> "Loop" of fun7/3 
* CEs [51] --> Loop 29 
* CEs [43] --> Loop 30 
* CEs [42,48] --> Loop 31 
* CEs [47] --> Loop 32 
* CEs [46] --> Loop 33 
* CEs [41,45] --> Loop 34 
* CEs [44,49] --> Loop 35 
* CEs [40] --> Loop 36 
* CEs [39] --> Loop 37 
* CEs [38] --> Loop 38 
* CEs [50] --> Loop 39 

### Ranking functions of CR fun7(V,V2,Out) 
* RF of phase [29]: [V]

#### Partial ranking functions of CR fun7(V,V2,Out) 
* Partial RF of phase [29]:
  - RF of loop [29:1]:
    V


### Specialization of cost equations fun8/3 
* CE 21 is refined into CE [52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71] 
* CE 23 is refined into CE [72] 
* CE 22 is refined into CE [73] 


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

### Ranking functions of CR fun8(V,V2,Out) 
* RF of phase [40]: [V]

#### Partial ranking functions of CR fun8(V,V2,Out) 
* Partial RF of phase [40]:
  - RF of loop [40:1]:
    V


### Specialization of cost equations start/2 
* CE 1 is refined into CE [74,75] 
* CE 2 is refined into CE [76,77] 
* CE 3 is refined into CE [78,79,80,81,82,83] 
* CE 4 is refined into CE [84,85,86,87,88,89] 
* CE 5 is refined into CE [90,91,92,93,94,95,96,97,98,99,100,101] 
* CE 6 is refined into CE [102,103,104,105,106,107,108,109,110,111,112,113] 
* CE 7 is refined into CE [114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133] 
* CE 8 is refined into CE [134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153] 
* CE 9 is refined into CE [154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183] 


### Cost equations --> "Loop" of start/2 
* CEs [74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183] --> Loop 56 

### Ranking functions of CR start(V,V2) 

#### Partial ranking functions of CR start(V,V2) 


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

#### Cost of chains of fun1(V,V2,Out):
* Chain [[16],17]: 1*it(16)+0
  Such that:it(16) =< Out

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

* Chain [17]: 0
  with precondition: [Out=0,V>=0,V2>=0] 


#### Cost of chains of fun3(V,V2,Out):
* Chain [[18],21]: 1*it(18)+0
  Such that:it(18) =< Out

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

* Chain [[18],20]: 1*it(18)+2
  Such that:it(18) =< Out

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

* Chain [[18],19]: 1*it(18)+1*s(1)+2
  Such that:it(18) =< V
s(1) =< V2

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

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

* Chain [20]: 2
  with precondition: [Out=2,V>=1,V2>=0] 

* Chain [19]: 1*s(1)+2
  Such that:s(1) =< V2

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


#### Cost of chains of fun5(V,V2,Out):
* Chain [[22],28]: 1*it(22)+0
  Such that:it(22) =< Out

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

* Chain [[22],27]: 1*it(22)+2
  Such that:it(22) =< Out

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

* Chain [[22],26]: 1*it(22)+4
  Such that:it(22) =< Out

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

* Chain [[22],25]: 1*it(22)+2*s(2)+4
  Such that:it(22) =< V
aux(1) =< V2
s(2) =< aux(1)

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

* Chain [[22],24]: 1*it(22)+1*s(4)+2
  Such that:it(22) =< V
s(4) =< V2

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

* Chain [[22],23]: 1*it(22)+1*s(5)+1*s(6)+4
  Such that:it(22) =< V
s(5) =< V2
s(6) =< V2+1

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

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

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

* Chain [26]: 4
  with precondition: [Out=4,V>=1,V2>=1] 

* Chain [25]: 2*s(2)+4
  Such that:aux(1) =< V2
s(2) =< aux(1)

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

* Chain [24]: 1*s(4)+2
  Such that:s(4) =< V2

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

* Chain [23]: 1*s(5)+1*s(6)+4
  Such that:s(5) =< V2
s(6) =< V2+1

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


#### Cost of chains of fun7(V,V2,Out):
* Chain [[29],39]: 1*it(29)+0
  Such that:it(29) =< Out

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

* Chain [[29],38]: 1*it(29)+2
  Such that:it(29) =< Out

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

* Chain [[29],37]: 1*it(29)+4
  Such that:it(29) =< Out

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

* Chain [[29],36]: 1*it(29)+6
  Such that:it(29) =< Out

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

* Chain [[29],35]: 1*it(29)+2*s(7)+1*s(9)+6
  Such that:it(29) =< V
aux(2) =< V2
s(9) =< V2+3
s(7) =< aux(2)

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

* Chain [[29],34]: 1*it(29)+4*s(11)+1*s(14)+6
  Such that:it(29) =< V
aux(4) =< V2
s(14) =< V2+1
s(11) =< aux(4)

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

* Chain [[29],33]: 1*it(29)+3*s(15)+6
  Such that:it(29) =< V
aux(5) =< V2
s(15) =< aux(5)

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

* Chain [[29],32]: 1*it(29)+1*s(18)+2
  Such that:it(29) =< V
s(18) =< V2

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

* Chain [[29],31]: 1*it(29)+1*s(19)+1*s(20)+4
  Such that:it(29) =< V
s(19) =< V2
s(20) =< V2+1

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

* Chain [[29],30]: 1*it(29)+1*s(21)+1*s(22)+6
  Such that:it(29) =< V
s(21) =< V2
s(22) =< V2+1

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

* Chain [39]: 0
  with precondition: [Out=0,V>=0,V2>=0] 

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

* Chain [37]: 4
  with precondition: [Out=4,V>=1,V2>=1] 

* Chain [36]: 6
  with precondition: [Out=6,V>=1,V2>=1] 

* Chain [35]: 2*s(7)+1*s(9)+6
  Such that:aux(2) =< V2
s(9) =< V2+3
s(7) =< aux(2)

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

* Chain [34]: 4*s(11)+1*s(14)+6
  Such that:s(14) =< V2+1
aux(4) =< V2
s(11) =< aux(4)

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

* Chain [33]: 3*s(15)+6
  Such that:aux(5) =< V2
s(15) =< aux(5)

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

* Chain [32]: 1*s(18)+2
  Such that:s(18) =< V2

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

* Chain [31]: 1*s(19)+1*s(20)+4
  Such that:s(19) =< V2
s(20) =< V2+1

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

* Chain [30]: 1*s(21)+1*s(22)+6
  Such that:s(21) =< V2
s(22) =< V2+1

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


#### Cost of chains of fun8(V,V2,Out):
* Chain [[40],55]: 1*it(40)+0
  Such that:it(40) =< Out

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

* Chain [[40],54]: 1*it(40)+2
  Such that:it(40) =< Out

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

* Chain [[40],53]: 1*it(40)+4
  Such that:it(40) =< Out

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

* Chain [[40],52]: 1*it(40)+6
  Such that:it(40) =< Out

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

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

  with precondition: [V2>=1,Out>=9,V+7>=Out] 

* Chain [[40],50]: 1*it(40)+2*s(23)+1*s(25)+6
  Such that:it(40) =< V
aux(6) =< V2
s(25) =< V2+3
s(23) =< aux(6)

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

* Chain [[40],49]: 1*it(40)+1*s(27)+4*s(28)+1*s(31)+1*s(32)+8
  Such that:it(40) =< V
aux(8) =< V2
s(31) =< V2+1
s(27) =< V2+3
s(32) =< V2+5
s(28) =< aux(8)

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

* Chain [[40],48]: 1*it(40)+3*s(33)+1*s(35)+8
  Such that:it(40) =< V
aux(9) =< V2
s(35) =< V2+3
s(33) =< aux(9)

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

* Chain [[40],47]: 1*it(40)+2*s(37)+6*s(39)+8
  Such that:it(40) =< V
aux(11) =< V2
aux(12) =< V2+1
s(37) =< aux(12)
s(39) =< aux(11)

  with precondition: [V>=2,V2>=2,Out>=11,V+2*V2+6>=Out] 

* Chain [[40],46]: 1*it(40)+8*s(44)+1*s(47)+8
  Such that:it(40) =< V
aux(14) =< V2
s(47) =< V2+1
s(44) =< aux(14)

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

* Chain [[40],45]: 1*it(40)+4*s(49)+8
  Such that:it(40) =< V
aux(15) =< V2
s(49) =< aux(15)

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

* Chain [[40],44]: 1*it(40)+1*s(52)+2
  Such that:it(40) =< V
s(52) =< V2

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

* Chain [[40],43]: 1*it(40)+1*s(53)+1*s(54)+4
  Such that:it(40) =< V
s(53) =< V2
s(54) =< V2+1

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

* Chain [[40],42]: 1*it(40)+1*s(55)+1*s(56)+6
  Such that:it(40) =< V
s(55) =< V2
s(56) =< V2+1

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

* Chain [[40],41]: 1*it(40)+1*s(57)+1*s(58)+8
  Such that:it(40) =< V
s(57) =< V2
s(58) =< V2+1

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

* Chain [55]: 0
  with precondition: [Out=0,V>=0,V2>=0] 

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

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

* Chain [52]: 6
  with precondition: [Out=6,V>=1,V2>=1] 

* Chain [51]: 8
  with precondition: [Out=8,V>=1,V2>=1] 

* Chain [50]: 2*s(23)+1*s(25)+6
  Such that:aux(6) =< V2
s(25) =< V2+3
s(23) =< aux(6)

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

* Chain [49]: 1*s(27)+4*s(28)+1*s(31)+1*s(32)+8
  Such that:s(31) =< V2+1
s(27) =< V2+3
s(32) =< V2+5
aux(8) =< V2
s(28) =< aux(8)

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

* Chain [48]: 3*s(33)+1*s(35)+8
  Such that:s(35) =< V2+3
aux(9) =< V2
s(33) =< aux(9)

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

* Chain [47]: 2*s(37)+6*s(39)+8
  Such that:aux(11) =< V2
aux(12) =< V2+1
s(37) =< aux(12)
s(39) =< aux(11)

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

* Chain [46]: 8*s(44)+1*s(47)+8
  Such that:s(47) =< V2+1
aux(14) =< V2
s(44) =< aux(14)

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

* Chain [45]: 4*s(49)+8
  Such that:aux(15) =< V2
s(49) =< aux(15)

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

* Chain [44]: 1*s(52)+2
  Such that:s(52) =< V2

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

* Chain [43]: 1*s(53)+1*s(54)+4
  Such that:s(53) =< V2
s(54) =< V2+1

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

* Chain [42]: 1*s(55)+1*s(56)+6
  Such that:s(55) =< V2
s(56) =< V2+1

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

* Chain [41]: 1*s(57)+1*s(58)+8
  Such that:s(57) =< V2
s(58) =< V2+1

  with precondition: [V>=1,Out>=9,V2+8>=Out] 


#### Cost of chains of start(V,V2):
* Chain [56]: 73*s(59)+15*s(65)+96*s(66)+7*s(86)+22*s(91)+3*s(138)+8*s(140)+2*s(180)+1*s(243)+8
  Such that:s(243) =< V+7
aux(26) =< V
aux(27) =< V+1
aux(28) =< V+3
aux(29) =< V+5
aux(30) =< V2
aux(31) =< V2+1
aux(32) =< V2+3
aux(33) =< V2+5
s(59) =< aux(26)
s(65) =< aux(27)
s(86) =< aux(28)
s(138) =< aux(29)
s(66) =< aux(30)
s(91) =< aux(31)
s(140) =< aux(32)
s(180) =< aux(33)

  with precondition: [V>=0] 


Closed-form bounds of start(V,V2): 
-------------------------------------
* Chain [56] with precondition: [V>=0] 
    - Upper bound: 73*V+8+nat(V2)*96+(15*V+15)+(7*V+21)+(3*V+15)+(V+7)+nat(V2+1)*22+nat(V2+3)*8+nat(V2+5)*2 
    - Complexity: n 

### Maximum cost of start(V,V2): 73*V+8+nat(V2)*96+(15*V+15)+(7*V+21)+(3*V+15)+(V+7)+nat(V2+1)*22+nat(V2+3)*8+nat(V2+5)*2 
Asymptotic class: n 
* Total analysis performed in 908 ms.


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

(18)
BOUNDS(1, n^1)

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

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

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f_0(z0) -> a
   f_1(z0) -> g_1(z0, z0)
   g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
   f_2(z0) -> g_2(z0, z0)
   g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
   f_3(z0) -> g_3(z0, z0)
   g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
   f_4(z0) -> g_4(z0, z0)
   g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
   f_5(z0) -> g_5(z0, z0)
   g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))
Tuples:
   F_0(z0) -> c
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c2(F_0(z1))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   F_5(z0) -> c13(G_5(z0, z0))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))
S tuples:
   F_0(z0) -> c
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c2(F_0(z1))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   F_5(z0) -> c13(G_5(z0, z0))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))
K tuples:none
Defined Rule Symbols:   f_0_1, f_1_1, g_1_2, f_2_1, g_2_2, f_3_1, g_3_2, f_4_1, g_4_2, f_5_1, g_5_2

Defined Pair Symbols:   F_0_1, F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, F_5_1, G_5_2

Compound Symbols:   c, c1_1, c2_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c13_1, c14_1, c15_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:

   F_0(z0) -> c
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c2(F_0(z1))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   F_5(z0) -> c13(G_5(z0, z0))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))

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

   f_0(z0) -> a
   f_1(z0) -> g_1(z0, z0)
   g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
   f_2(z0) -> g_2(z0, z0)
   g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
   f_3(z0) -> g_3(z0, z0)
   g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
   f_4(z0) -> g_4(z0, z0)
   g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
   f_5(z0) -> g_5(z0, z0)
   g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, 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:

   F_0(z0) -> c
   F_1(z0) -> c1(G_1(z0, z0))
   G_1(s(z0), z1) -> c2(F_0(z1))
   G_1(s(z0), z1) -> c3(G_1(z0, z1))
   F_2(z0) -> c4(G_2(z0, z0))
   G_2(s(z0), z1) -> c5(F_1(z1))
   G_2(s(z0), z1) -> c6(G_2(z0, z1))
   F_3(z0) -> c7(G_3(z0, z0))
   G_3(s(z0), z1) -> c8(F_2(z1))
   G_3(s(z0), z1) -> c9(G_3(z0, z1))
   F_4(z0) -> c10(G_4(z0, z0))
   G_4(s(z0), z1) -> c11(F_3(z1))
   G_4(s(z0), z1) -> c12(G_4(z0, z1))
   F_5(z0) -> c13(G_5(z0, z0))
   G_5(s(z0), z1) -> c14(F_4(z1))
   G_5(s(z0), z1) -> c15(G_5(z0, z1))

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

   f_0(z0) -> a
   f_1(z0) -> g_1(z0, z0)
   g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
   f_2(z0) -> g_2(z0, z0)
   g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
   f_3(z0) -> g_3(z0, z0)
   g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
   f_4(z0) -> g_4(z0, z0)
   g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
   f_5(z0) -> g_5(z0, z0)
   g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

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

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

(26)
Obligation:
Innermost TRS:
Rules:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b

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

(27) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
G_1, G_2, G_3, G_4, G_5, g_1, g_2, g_3, g_4, g_5
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b


Generator Equations:
gen_s14_16(0) <=> hole_s2_16
gen_s14_16(+(x, 1)) <=> s(gen_s14_16(x))
gen_c2:c315_16(0) <=> c2(c)
gen_c2:c315_16(+(x, 1)) <=> c3(gen_c2:c315_16(x))
gen_c5:c616_16(0) <=> c5(c1(c2(c)))
gen_c5:c616_16(+(x, 1)) <=> c6(gen_c5:c616_16(x))
gen_c8:c917_16(0) <=> c8(c4(c5(c1(c2(c)))))
gen_c8:c917_16(+(x, 1)) <=> c9(gen_c8:c917_16(x))
gen_c11:c1218_16(0) <=> c11(c7(c8(c4(c5(c1(c2(c)))))))
gen_c11:c1218_16(+(x, 1)) <=> c12(gen_c11:c1218_16(x))
gen_c14:c1519_16(0) <=> c14(c10(c11(c7(c8(c4(c5(c1(c2(c)))))))))
gen_c14:c1519_16(+(x, 1)) <=> c15(gen_c14:c1519_16(x))
gen_a:b20_16(0) <=> a
gen_a:b20_16(+(x, 1)) <=> b(a, gen_a:b20_16(x))


The following defined symbols remain to be analysed:
G_1, G_2, G_3, G_4, G_5, g_1, g_2, g_3, g_4, g_5
----------------------------------------

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
G_1(gen_s14_16(+(1, n22_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n22_16)

Induction Base:
G_1(gen_s14_16(+(1, 0)), gen_s14_16(b))

Induction Step:
G_1(gen_s14_16(+(1, +(n22_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c3(G_1(gen_s14_16(+(1, n22_16)), gen_s14_16(b))) ->_IH
c3(*21_16)

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:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b


Generator Equations:
gen_s14_16(0) <=> hole_s2_16
gen_s14_16(+(x, 1)) <=> s(gen_s14_16(x))
gen_c2:c315_16(0) <=> c2(c)
gen_c2:c315_16(+(x, 1)) <=> c3(gen_c2:c315_16(x))
gen_c5:c616_16(0) <=> c5(c1(c2(c)))
gen_c5:c616_16(+(x, 1)) <=> c6(gen_c5:c616_16(x))
gen_c8:c917_16(0) <=> c8(c4(c5(c1(c2(c)))))
gen_c8:c917_16(+(x, 1)) <=> c9(gen_c8:c917_16(x))
gen_c11:c1218_16(0) <=> c11(c7(c8(c4(c5(c1(c2(c)))))))
gen_c11:c1218_16(+(x, 1)) <=> c12(gen_c11:c1218_16(x))
gen_c14:c1519_16(0) <=> c14(c10(c11(c7(c8(c4(c5(c1(c2(c)))))))))
gen_c14:c1519_16(+(x, 1)) <=> c15(gen_c14:c1519_16(x))
gen_a:b20_16(0) <=> a
gen_a:b20_16(+(x, 1)) <=> b(a, gen_a:b20_16(x))


The following defined symbols remain to be analysed:
G_1, G_2, G_3, G_4, G_5, g_1, g_2, g_3, g_4, g_5
----------------------------------------

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

(33)
BOUNDS(n^1, INF)

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

(34)
Obligation:
Innermost TRS:
Rules:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b


Lemmas:
G_1(gen_s14_16(+(1, n22_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n22_16)


Generator Equations:
gen_s14_16(0) <=> hole_s2_16
gen_s14_16(+(x, 1)) <=> s(gen_s14_16(x))
gen_c2:c315_16(0) <=> c2(c)
gen_c2:c315_16(+(x, 1)) <=> c3(gen_c2:c315_16(x))
gen_c5:c616_16(0) <=> c5(c1(c2(c)))
gen_c5:c616_16(+(x, 1)) <=> c6(gen_c5:c616_16(x))
gen_c8:c917_16(0) <=> c8(c4(c5(c1(c2(c)))))
gen_c8:c917_16(+(x, 1)) <=> c9(gen_c8:c917_16(x))
gen_c11:c1218_16(0) <=> c11(c7(c8(c4(c5(c1(c2(c)))))))
gen_c11:c1218_16(+(x, 1)) <=> c12(gen_c11:c1218_16(x))
gen_c14:c1519_16(0) <=> c14(c10(c11(c7(c8(c4(c5(c1(c2(c)))))))))
gen_c14:c1519_16(+(x, 1)) <=> c15(gen_c14:c1519_16(x))
gen_a:b20_16(0) <=> a
gen_a:b20_16(+(x, 1)) <=> b(a, gen_a:b20_16(x))


The following defined symbols remain to be analysed:
G_2, G_3, G_4, G_5, g_1, g_2, g_3, g_4, g_5
----------------------------------------

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
G_2(gen_s14_16(+(1, n978_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n978_16)

Induction Base:
G_2(gen_s14_16(+(1, 0)), gen_s14_16(b))

Induction Step:
G_2(gen_s14_16(+(1, +(n978_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c6(G_2(gen_s14_16(+(1, n978_16)), gen_s14_16(b))) ->_IH
c6(*21_16)

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:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b


Lemmas:
G_1(gen_s14_16(+(1, n22_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n978_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n978_16)


Generator Equations:
gen_s14_16(0) <=> hole_s2_16
gen_s14_16(+(x, 1)) <=> s(gen_s14_16(x))
gen_c2:c315_16(0) <=> c2(c)
gen_c2:c315_16(+(x, 1)) <=> c3(gen_c2:c315_16(x))
gen_c5:c616_16(0) <=> c5(c1(c2(c)))
gen_c5:c616_16(+(x, 1)) <=> c6(gen_c5:c616_16(x))
gen_c8:c917_16(0) <=> c8(c4(c5(c1(c2(c)))))
gen_c8:c917_16(+(x, 1)) <=> c9(gen_c8:c917_16(x))
gen_c11:c1218_16(0) <=> c11(c7(c8(c4(c5(c1(c2(c)))))))
gen_c11:c1218_16(+(x, 1)) <=> c12(gen_c11:c1218_16(x))
gen_c14:c1519_16(0) <=> c14(c10(c11(c7(c8(c4(c5(c1(c2(c)))))))))
gen_c14:c1519_16(+(x, 1)) <=> c15(gen_c14:c1519_16(x))
gen_a:b20_16(0) <=> a
gen_a:b20_16(+(x, 1)) <=> b(a, gen_a:b20_16(x))


The following defined symbols remain to be analysed:
G_3, G_4, G_5, g_1, g_2, g_3, g_4, g_5
----------------------------------------

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
G_3(gen_s14_16(+(1, n2540_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n2540_16)

Induction Base:
G_3(gen_s14_16(+(1, 0)), gen_s14_16(b))

Induction Step:
G_3(gen_s14_16(+(1, +(n2540_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c9(G_3(gen_s14_16(+(1, n2540_16)), gen_s14_16(b))) ->_IH
c9(*21_16)

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

(38)
Obligation:
Innermost TRS:
Rules:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b


Lemmas:
G_1(gen_s14_16(+(1, n22_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n978_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n978_16)
G_3(gen_s14_16(+(1, n2540_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n2540_16)


Generator Equations:
gen_s14_16(0) <=> hole_s2_16
gen_s14_16(+(x, 1)) <=> s(gen_s14_16(x))
gen_c2:c315_16(0) <=> c2(c)
gen_c2:c315_16(+(x, 1)) <=> c3(gen_c2:c315_16(x))
gen_c5:c616_16(0) <=> c5(c1(c2(c)))
gen_c5:c616_16(+(x, 1)) <=> c6(gen_c5:c616_16(x))
gen_c8:c917_16(0) <=> c8(c4(c5(c1(c2(c)))))
gen_c8:c917_16(+(x, 1)) <=> c9(gen_c8:c917_16(x))
gen_c11:c1218_16(0) <=> c11(c7(c8(c4(c5(c1(c2(c)))))))
gen_c11:c1218_16(+(x, 1)) <=> c12(gen_c11:c1218_16(x))
gen_c14:c1519_16(0) <=> c14(c10(c11(c7(c8(c4(c5(c1(c2(c)))))))))
gen_c14:c1519_16(+(x, 1)) <=> c15(gen_c14:c1519_16(x))
gen_a:b20_16(0) <=> a
gen_a:b20_16(+(x, 1)) <=> b(a, gen_a:b20_16(x))


The following defined symbols remain to be analysed:
G_4, G_5, g_1, g_2, g_3, g_4, g_5
----------------------------------------

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
G_4(gen_s14_16(+(1, n4422_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n4422_16)

Induction Base:
G_4(gen_s14_16(+(1, 0)), gen_s14_16(b))

Induction Step:
G_4(gen_s14_16(+(1, +(n4422_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c12(G_4(gen_s14_16(+(1, n4422_16)), gen_s14_16(b))) ->_IH
c12(*21_16)

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

(40)
Obligation:
Innermost TRS:
Rules:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b


Lemmas:
G_1(gen_s14_16(+(1, n22_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n978_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n978_16)
G_3(gen_s14_16(+(1, n2540_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n2540_16)
G_4(gen_s14_16(+(1, n4422_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n4422_16)


Generator Equations:
gen_s14_16(0) <=> hole_s2_16
gen_s14_16(+(x, 1)) <=> s(gen_s14_16(x))
gen_c2:c315_16(0) <=> c2(c)
gen_c2:c315_16(+(x, 1)) <=> c3(gen_c2:c315_16(x))
gen_c5:c616_16(0) <=> c5(c1(c2(c)))
gen_c5:c616_16(+(x, 1)) <=> c6(gen_c5:c616_16(x))
gen_c8:c917_16(0) <=> c8(c4(c5(c1(c2(c)))))
gen_c8:c917_16(+(x, 1)) <=> c9(gen_c8:c917_16(x))
gen_c11:c1218_16(0) <=> c11(c7(c8(c4(c5(c1(c2(c)))))))
gen_c11:c1218_16(+(x, 1)) <=> c12(gen_c11:c1218_16(x))
gen_c14:c1519_16(0) <=> c14(c10(c11(c7(c8(c4(c5(c1(c2(c)))))))))
gen_c14:c1519_16(+(x, 1)) <=> c15(gen_c14:c1519_16(x))
gen_a:b20_16(0) <=> a
gen_a:b20_16(+(x, 1)) <=> b(a, gen_a:b20_16(x))


The following defined symbols remain to be analysed:
G_5, g_1, g_2, g_3, g_4, g_5
----------------------------------------

(41) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
G_5(gen_s14_16(+(1, n6624_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n6624_16)

Induction Base:
G_5(gen_s14_16(+(1, 0)), gen_s14_16(b))

Induction Step:
G_5(gen_s14_16(+(1, +(n6624_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c15(G_5(gen_s14_16(+(1, n6624_16)), gen_s14_16(b))) ->_IH
c15(*21_16)

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

(42)
Obligation:
Innermost TRS:
Rules:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b


Lemmas:
G_1(gen_s14_16(+(1, n22_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n978_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n978_16)
G_3(gen_s14_16(+(1, n2540_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n2540_16)
G_4(gen_s14_16(+(1, n4422_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n4422_16)
G_5(gen_s14_16(+(1, n6624_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n6624_16)


Generator Equations:
gen_s14_16(0) <=> hole_s2_16
gen_s14_16(+(x, 1)) <=> s(gen_s14_16(x))
gen_c2:c315_16(0) <=> c2(c)
gen_c2:c315_16(+(x, 1)) <=> c3(gen_c2:c315_16(x))
gen_c5:c616_16(0) <=> c5(c1(c2(c)))
gen_c5:c616_16(+(x, 1)) <=> c6(gen_c5:c616_16(x))
gen_c8:c917_16(0) <=> c8(c4(c5(c1(c2(c)))))
gen_c8:c917_16(+(x, 1)) <=> c9(gen_c8:c917_16(x))
gen_c11:c1218_16(0) <=> c11(c7(c8(c4(c5(c1(c2(c)))))))
gen_c11:c1218_16(+(x, 1)) <=> c12(gen_c11:c1218_16(x))
gen_c14:c1519_16(0) <=> c14(c10(c11(c7(c8(c4(c5(c1(c2(c)))))))))
gen_c14:c1519_16(+(x, 1)) <=> c15(gen_c14:c1519_16(x))
gen_a:b20_16(0) <=> a
gen_a:b20_16(+(x, 1)) <=> b(a, gen_a:b20_16(x))


The following defined symbols remain to be analysed:
g_1, g_2, g_3, g_4, g_5
----------------------------------------

(43) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
g_1(gen_s14_16(+(1, n9146_16)), gen_s14_16(b)) -> *21_16, rt in Omega(0)

Induction Base:
g_1(gen_s14_16(+(1, 0)), gen_s14_16(b))

Induction Step:
g_1(gen_s14_16(+(1, +(n9146_16, 1))), gen_s14_16(b)) ->_R^Omega(0)
b(f_0(gen_s14_16(b)), g_1(gen_s14_16(+(1, n9146_16)), gen_s14_16(b))) ->_R^Omega(0)
b(a, g_1(gen_s14_16(+(1, n9146_16)), gen_s14_16(b))) ->_IH
b(a, *21_16)

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

(44)
Obligation:
Innermost TRS:
Rules:
F_0(z0) -> c
F_1(z0) -> c1(G_1(z0, z0))
G_1(s(z0), z1) -> c2(F_0(z1))
G_1(s(z0), z1) -> c3(G_1(z0, z1))
F_2(z0) -> c4(G_2(z0, z0))
G_2(s(z0), z1) -> c5(F_1(z1))
G_2(s(z0), z1) -> c6(G_2(z0, z1))
F_3(z0) -> c7(G_3(z0, z0))
G_3(s(z0), z1) -> c8(F_2(z1))
G_3(s(z0), z1) -> c9(G_3(z0, z1))
F_4(z0) -> c10(G_4(z0, z0))
G_4(s(z0), z1) -> c11(F_3(z1))
G_4(s(z0), z1) -> c12(G_4(z0, z1))
F_5(z0) -> c13(G_5(z0, z0))
G_5(s(z0), z1) -> c14(F_4(z1))
G_5(s(z0), z1) -> c15(G_5(z0, z1))
f_0(z0) -> a
f_1(z0) -> g_1(z0, z0)
g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1))
f_2(z0) -> g_2(z0, z0)
g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1))
f_3(z0) -> g_3(z0, z0)
g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1))
f_4(z0) -> g_4(z0, z0)
g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1))
f_5(z0) -> g_5(z0, z0)
g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1))

Types:
F_0 :: s -> c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: s -> s -> c2:c3
s :: s -> s
c2 :: c -> c2:c3
c3 :: c2:c3 -> c2:c3
F_2 :: s -> c4
c4 :: c5:c6 -> c4
G_2 :: s -> s -> c5:c6
c5 :: c1 -> c5:c6
c6 :: c5:c6 -> c5:c6
F_3 :: s -> c7
c7 :: c8:c9 -> c7
G_3 :: s -> s -> c8:c9
c8 :: c4 -> c8:c9
c9 :: c8:c9 -> c8:c9
F_4 :: s -> c10
c10 :: c11:c12 -> c10
G_4 :: s -> s -> c11:c12
c11 :: c7 -> c11:c12
c12 :: c11:c12 -> c11:c12
F_5 :: s -> c13
c13 :: c14:c15 -> c13
G_5 :: s -> s -> c14:c15
c14 :: c10 -> c14:c15
c15 :: c14:c15 -> c14:c15
f_0 :: s -> a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: s -> s -> a:b
b :: a:b -> a:b -> a:b
f_2 :: s -> a:b
g_2 :: s -> s -> a:b
f_3 :: s -> a:b
g_3 :: s -> s -> a:b
f_4 :: s -> a:b
g_4 :: s -> s -> a:b
f_5 :: s -> a:b
g_5 :: s -> s -> a:b
hole_c1_16 :: c
hole_s2_16 :: s
hole_c13_16 :: c1
hole_c2:c34_16 :: c2:c3
hole_c45_16 :: c4
hole_c5:c66_16 :: c5:c6
hole_c77_16 :: c7
hole_c8:c98_16 :: c8:c9
hole_c109_16 :: c10
hole_c11:c1210_16 :: c11:c12
hole_c1311_16 :: c13
hole_c14:c1512_16 :: c14:c15
hole_a:b13_16 :: a:b
gen_s14_16 :: Nat -> s
gen_c2:c315_16 :: Nat -> c2:c3
gen_c5:c616_16 :: Nat -> c5:c6
gen_c8:c917_16 :: Nat -> c8:c9
gen_c11:c1218_16 :: Nat -> c11:c12
gen_c14:c1519_16 :: Nat -> c14:c15
gen_a:b20_16 :: Nat -> a:b


Lemmas:
G_1(gen_s14_16(+(1, n22_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n978_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n978_16)
G_3(gen_s14_16(+(1, n2540_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n2540_16)
G_4(gen_s14_16(+(1, n4422_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n4422_16)
G_5(gen_s14_16(+(1, n6624_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n6624_16)
g_1(gen_s14_16(+(1, n9146_16)), gen_s14_16(b)) -> *21_16, rt in Omega(0)


Generator Equations:
gen_s14_16(0) <=> hole_s2_16
gen_s14_16(+(x, 1)) <=> s(gen_s14_16(x))
gen_c2:c315_16(0) <=> c2(c)
gen_c2:c315_16(+(x, 1)) <=> c3(gen_c2:c315_16(x))
gen_c5:c616_16(0) <=> c5(c1(c2(c)))
gen_c5:c616_16(+(x, 1)) <=> c6(gen_c5:c616_16(x))
gen_c8:c917_16(0) <=> c8(c4(c5(c1(c2(c)))))
gen_c8:c917_16(+(x, 1)) <=> c9(gen_c8:c917_16(x))
gen_c11:c1218_16(0) <=> c11(c7(c8(c4(c5(c1(c2(c)))))))
gen_c11:c1218_16(+(x, 1)) <=> c12(gen_c11:c1218_16(x))
gen_c14:c1519_16(0) <=> c14(c10(c11(c7(c8(c4(c5(c1(c2(c)))))))))
gen_c14:c1519_16(+(x, 1)) <=> c15(gen_c14:c1519_16(x))
gen_a:b20_16(0) <=> a
gen_a:b20_16(+(x, 1)) <=> b(a, gen_a:b20_16(x))


The following defined symbols remain to be analysed:
g_2, g_3, g_4, g_5