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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 345 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 84 ms]
    (12) CdtProblem
    (13) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 19 ms]
    (16) CdtProblem
    (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 23 ms]
    (18) CdtProblem
    (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 4 ms]
    (20) CdtProblem
    (21) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) BOUNDS(1, 1)
(23) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(24) CpxRelTRS
    (25) SlicingProof [LOWER BOUND(ID), 0 ms]
    (26) CpxRelTRS
    (27) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) typed CpxTrs
    (29) OrderProof [LOWER BOUND(ID), 0 ms]
    (30) typed CpxTrs
    (31) RewriteLemmaProof [LOWER BOUND(ID), 417 ms]
    (32) BEST
        (33) proven lower bound
            (34) LowerBoundPropagationProof [FINISHED, 0 ms]
            (35) BOUNDS(n^1, INF)
        (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 129 ms]
            (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 109 ms]
            (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 105 ms]
            (42) typed CpxTrs
            (43) RewriteLemmaProof [LOWER BOUND(ID), 125 ms]
            (44) typed CpxTrs
            (45) RewriteLemmaProof [LOWER BOUND(ID), 133 ms]
            (46) typed CpxTrs


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

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


The TRS R consists of the following rules:

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

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

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


The TRS R consists of the following rules:

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

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(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))
   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))
Tuples:
   F_0'(z0) -> c16
   F_1'(z0) -> c17(G_1'(z0, z0))
   G_1'(s(z0), z1) -> c18(F_0'(z1), G_1'(z0, z1))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   F_5'(z0) -> c25(G_5'(z0, z0))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_0''(z0) -> c27
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c29(F_0''(z1))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   F_5''(z0) -> c40(G_5''(z0, z0))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
S tuples:
   F_0''(z0) -> c27
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c29(F_0''(z1))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   F_5''(z0) -> c40(G_5''(z0, z0))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(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, 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, 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:   c16, c17_1, c18_2, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c25_1, c26_2, c27, c28_1, c29_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c40_1, c41_1, c42_1


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

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 2 leading nodes:
   F_5'(z0) -> c25(G_5'(z0, z0))
   F_5''(z0) -> c40(G_5''(z0, z0))
Removed 3 trailing nodes:
   F_0''(z0) -> c27
   G_1''(s(z0), z1) -> c29(F_0''(z1))
   F_0'(z0) -> c16

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

(6)
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))
   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))
Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   G_1'(s(z0), z1) -> c18(F_0'(z1), G_1'(z0, z1))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
S tuples:
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(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, 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, 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:   c17_1, c18_2, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c26_2, c28_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c41_1, c42_1


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

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

(8)
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))
   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))
Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
S tuples:
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(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, 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, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, G_5'_2, 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, G_1'_2

Compound Symbols:   c17_1, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c26_2, c28_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c41_1, c42_1, c18_1


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

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

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
S tuples:
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, G_5'_2, 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, G_1'_2

Compound Symbols:   c17_1, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c26_2, c28_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c41_1, c42_1, c18_1


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

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(F_1'(x_1)) = 0
   POL(F_1''(x_1)) = 0
   POL(F_2'(x_1)) = 0
   POL(F_2''(x_1)) = x_1
   POL(F_3'(x_1)) = 0
   POL(F_3''(x_1)) = [1] + x_1
   POL(F_4'(x_1)) = [1]
   POL(F_4''(x_1)) = [1] + x_1
   POL(G_1'(x_1, x_2)) = 0
   POL(G_1''(x_1, x_2)) = 0
   POL(G_2'(x_1, x_2)) = 0
   POL(G_2''(x_1, x_2)) = x_1
   POL(G_3'(x_1, x_2)) = 0
   POL(G_3''(x_1, x_2)) = x_2
   POL(G_4'(x_1, x_2)) = [1]
   POL(G_4''(x_1, x_2)) = [1] + x_2
   POL(G_5'(x_1, x_2)) = x_1
   POL(G_5''(x_1, x_2)) = x_1 + x_2
   POL(c17(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c19(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c22(x_1, x_2)) = x_1 + x_2
   POL(c23(x_1)) = x_1
   POL(c24(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2)) = x_1 + x_2
   POL(c28(x_1)) = x_1
   POL(c30(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c32(x_1)) = x_1
   POL(c33(x_1)) = x_1
   POL(c34(x_1)) = x_1
   POL(c35(x_1)) = x_1
   POL(c36(x_1)) = x_1
   POL(c37(x_1)) = x_1
   POL(c38(x_1)) = x_1
   POL(c39(x_1)) = x_1
   POL(c41(x_1)) = x_1
   POL(c42(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
S tuples:
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
K tuples:
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
Defined Rule Symbols:none

Defined Pair Symbols:   F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, G_5'_2, 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, G_1'_2

Compound Symbols:   c17_1, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c26_2, c28_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c41_1, c42_1, c18_1


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

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   F_4''(z0) -> c37(G_4''(z0, z0))

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
S tuples:
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
K tuples:
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
Defined Rule Symbols:none

Defined Pair Symbols:   F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, G_5'_2, 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, G_1'_2

Compound Symbols:   c17_1, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c26_2, c28_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c41_1, c42_1, c18_1


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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(F_1'(x_1)) = 0
   POL(F_1''(x_1)) = 0
   POL(F_2'(x_1)) = 0
   POL(F_2''(x_1)) = [1]
   POL(F_3'(x_1)) = 0
   POL(F_3''(x_1)) = [1]
   POL(F_4'(x_1)) = [1]
   POL(F_4''(x_1)) = [1] + x_1
   POL(G_1'(x_1, x_2)) = 0
   POL(G_1''(x_1, x_2)) = 0
   POL(G_2'(x_1, x_2)) = 0
   POL(G_2''(x_1, x_2)) = 0
   POL(G_3'(x_1, x_2)) = 0
   POL(G_3''(x_1, x_2)) = [1]
   POL(G_4'(x_1, x_2)) = [1]
   POL(G_4''(x_1, x_2)) = [1] + x_1
   POL(G_5'(x_1, x_2)) = x_1
   POL(G_5''(x_1, x_2)) = x_1 + x_2
   POL(c17(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c19(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c22(x_1, x_2)) = x_1 + x_2
   POL(c23(x_1)) = x_1
   POL(c24(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2)) = x_1 + x_2
   POL(c28(x_1)) = x_1
   POL(c30(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c32(x_1)) = x_1
   POL(c33(x_1)) = x_1
   POL(c34(x_1)) = x_1
   POL(c35(x_1)) = x_1
   POL(c36(x_1)) = x_1
   POL(c37(x_1)) = x_1
   POL(c38(x_1)) = x_1
   POL(c39(x_1)) = x_1
   POL(c41(x_1)) = x_1
   POL(c42(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
S tuples:
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
K tuples:
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
Defined Rule Symbols:none

Defined Pair Symbols:   F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, G_5'_2, 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, G_1'_2

Compound Symbols:   c17_1, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c26_2, c28_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c41_1, c42_1, c18_1


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

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(F_1'(x_1)) = 0
   POL(F_1''(x_1)) = [1] + x_1
   POL(F_2'(x_1)) = 0
   POL(F_2''(x_1)) = [1] + x_1
   POL(F_3'(x_1)) = 0
   POL(F_3''(x_1)) = [1] + x_1
   POL(F_4'(x_1)) = [1]
   POL(F_4''(x_1)) = [1] + x_1
   POL(G_1'(x_1, x_2)) = 0
   POL(G_1''(x_1, x_2)) = [1] + x_1
   POL(G_2'(x_1, x_2)) = 0
   POL(G_2''(x_1, x_2)) = [1] + x_2
   POL(G_3'(x_1, x_2)) = 0
   POL(G_3''(x_1, x_2)) = [1] + x_2
   POL(G_4'(x_1, x_2)) = [1]
   POL(G_4''(x_1, x_2)) = [1] + x_2
   POL(G_5'(x_1, x_2)) = x_1
   POL(G_5''(x_1, x_2)) = [1] + x_2
   POL(c17(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c19(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c22(x_1, x_2)) = x_1 + x_2
   POL(c23(x_1)) = x_1
   POL(c24(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2)) = x_1 + x_2
   POL(c28(x_1)) = x_1
   POL(c30(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c32(x_1)) = x_1
   POL(c33(x_1)) = x_1
   POL(c34(x_1)) = x_1
   POL(c35(x_1)) = x_1
   POL(c36(x_1)) = x_1
   POL(c37(x_1)) = x_1
   POL(c38(x_1)) = x_1
   POL(c39(x_1)) = x_1
   POL(c41(x_1)) = x_1
   POL(c42(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1

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

(18)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
S tuples:
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
K tuples:
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
Defined Rule Symbols:none

Defined Pair Symbols:   F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, G_5'_2, 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, G_1'_2

Compound Symbols:   c17_1, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c26_2, c28_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c41_1, c42_1, c18_1


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

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(F_1'(x_1)) = 0
   POL(F_1''(x_1)) = [1]
   POL(F_2'(x_1)) = 0
   POL(F_2''(x_1)) = [1]
   POL(F_3'(x_1)) = 0
   POL(F_3''(x_1)) = [1] + x_1
   POL(F_4'(x_1)) = [1]
   POL(F_4''(x_1)) = [1] + x_1
   POL(G_1'(x_1, x_2)) = 0
   POL(G_1''(x_1, x_2)) = [1]
   POL(G_2'(x_1, x_2)) = 0
   POL(G_2''(x_1, x_2)) = [1]
   POL(G_3'(x_1, x_2)) = 0
   POL(G_3''(x_1, x_2)) = [1] + x_1
   POL(G_4'(x_1, x_2)) = [1]
   POL(G_4''(x_1, x_2)) = [1] + x_2
   POL(G_5'(x_1, x_2)) = x_1
   POL(G_5''(x_1, x_2)) = [1] + x_2
   POL(c17(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c19(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c22(x_1, x_2)) = x_1 + x_2
   POL(c23(x_1)) = x_1
   POL(c24(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2)) = x_1 + x_2
   POL(c28(x_1)) = x_1
   POL(c30(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c32(x_1)) = x_1
   POL(c33(x_1)) = x_1
   POL(c34(x_1)) = x_1
   POL(c35(x_1)) = x_1
   POL(c36(x_1)) = x_1
   POL(c37(x_1)) = x_1
   POL(c38(x_1)) = x_1
   POL(c39(x_1)) = x_1
   POL(c41(x_1)) = x_1
   POL(c42(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1

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

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F_1'(z0) -> c17(G_1'(z0, z0))
   F_2'(z0) -> c19(G_2'(z0, z0))
   G_2'(s(z0), z1) -> c20(F_1'(z1), G_2'(z0, z1))
   F_3'(z0) -> c21(G_3'(z0, z0))
   G_3'(s(z0), z1) -> c22(F_2'(z1), G_3'(z0, z1))
   F_4'(z0) -> c23(G_4'(z0, z0))
   G_4'(s(z0), z1) -> c24(F_3'(z1), G_4'(z0, z1))
   G_5'(s(z0), z1) -> c26(F_4'(z1), G_5'(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   G_1'(s(z0), z1) -> c18(G_1'(z0, z1))
S tuples:none
K tuples:
   G_2''(s(z0), z1) -> c32(F_1''(z1))
   G_2''(s(z0), z1) -> c33(G_2''(z0, z1))
   F_3''(z0) -> c34(G_3''(z0, z0))
   G_5''(s(z0), z1) -> c42(G_5''(z0, z1))
   F_1''(z0) -> c28(G_1''(z0, z0))
   G_5''(s(z0), z1) -> c41(F_4''(z1))
   F_4''(z0) -> c37(G_4''(z0, z0))
   F_2''(z0) -> c31(G_2''(z0, z0))
   G_4''(s(z0), z1) -> c38(F_3''(z1))
   G_4''(s(z0), z1) -> c39(G_4''(z0, z1))
   G_1''(s(z0), z1) -> c30(G_1''(z0, z1))
   G_3''(s(z0), z1) -> c35(F_2''(z1))
   G_3''(s(z0), z1) -> c36(G_3''(z0, z1))
Defined Rule Symbols:none

Defined Pair Symbols:   F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, G_5'_2, 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, G_1'_2

Compound Symbols:   c17_1, c19_1, c20_2, c21_1, c22_2, c23_1, c24_2, c26_2, c28_1, c30_1, c31_1, c32_1, c33_1, c34_1, c35_1, c36_1, c37_1, c38_1, c39_1, c41_1, c42_1, c18_1


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

(21) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(22)
BOUNDS(1, 1)

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

(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) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
F_0/0
G_1/1
f_0/0
g_1/1

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

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


The TRS R consists of the following rules:

   F_0 -> c
   F_1(z0) -> c1(G_1(z0))
   G_1(s(z0)) -> c2(F_0)
   G_1(s(z0)) -> c3(G_1(z0))
   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 -> a
   f_1(z0) -> g_1(z0)
   g_1(s(z0)) -> b(f_0, g_1(z0))
   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
----------------------------------------

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

(28)
Obligation:
Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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

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

(29) 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
----------------------------------------

(30)
Obligation:
Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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_s3_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
----------------------------------------

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

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

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

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

(32)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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_s3_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
----------------------------------------

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

(35)
BOUNDS(n^1, INF)

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

(36)
Obligation:
Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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))) -> *21_16, rt in Omega(n22_16)


Generator Equations:
gen_s14_16(0) <=> hole_s3_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
----------------------------------------

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

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

Induction Step:
G_2(gen_s14_16(+(1, +(n334_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c6(G_2(gen_s14_16(+(1, n334_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).
----------------------------------------

(38)
Obligation:
Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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))) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n334_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n334_16)


Generator Equations:
gen_s14_16(0) <=> hole_s3_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
----------------------------------------

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

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

Induction Step:
G_3(gen_s14_16(+(1, +(n1682_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c9(G_3(gen_s14_16(+(1, n1682_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).
----------------------------------------

(40)
Obligation:
Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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))) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n334_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n334_16)
G_3(gen_s14_16(+(1, n1682_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n1682_16)


Generator Equations:
gen_s14_16(0) <=> hole_s3_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
----------------------------------------

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

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

Induction Step:
G_4(gen_s14_16(+(1, +(n3466_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c12(G_4(gen_s14_16(+(1, n3466_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).
----------------------------------------

(42)
Obligation:
Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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))) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n334_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n334_16)
G_3(gen_s14_16(+(1, n1682_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n1682_16)
G_4(gen_s14_16(+(1, n3466_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n3466_16)


Generator Equations:
gen_s14_16(0) <=> hole_s3_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
----------------------------------------

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

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

Induction Step:
G_5(gen_s14_16(+(1, +(n5570_16, 1))), gen_s14_16(b)) ->_R^Omega(1)
c15(G_5(gen_s14_16(+(1, n5570_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).
----------------------------------------

(44)
Obligation:
Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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))) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n334_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n334_16)
G_3(gen_s14_16(+(1, n1682_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n1682_16)
G_4(gen_s14_16(+(1, n3466_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n3466_16)
G_5(gen_s14_16(+(1, n5570_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n5570_16)


Generator Equations:
gen_s14_16(0) <=> hole_s3_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
----------------------------------------

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

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

Induction Step:
g_1(gen_s14_16(+(1, +(n7994_16, 1)))) ->_R^Omega(0)
b(f_0, g_1(gen_s14_16(+(1, n7994_16)))) ->_R^Omega(0)
b(a, g_1(gen_s14_16(+(1, n7994_16)))) ->_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).
----------------------------------------

(46)
Obligation:
Innermost TRS:
Rules:
F_0 -> c
F_1(z0) -> c1(G_1(z0))
G_1(s(z0)) -> c2(F_0)
G_1(s(z0)) -> c3(G_1(z0))
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 -> a
f_1(z0) -> g_1(z0)
g_1(s(z0)) -> b(f_0, g_1(z0))
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 :: c
c :: c
F_1 :: s -> c1
c1 :: c2:c3 -> c1
G_1 :: 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 :: a:b
a :: a:b
f_1 :: s -> a:b
g_1 :: 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_c12_16 :: c1
hole_s3_16 :: s
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))) -> *21_16, rt in Omega(n22_16)
G_2(gen_s14_16(+(1, n334_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n334_16)
G_3(gen_s14_16(+(1, n1682_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n1682_16)
G_4(gen_s14_16(+(1, n3466_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n3466_16)
G_5(gen_s14_16(+(1, n5570_16)), gen_s14_16(b)) -> *21_16, rt in Omega(n5570_16)
g_1(gen_s14_16(+(1, n7994_16))) -> *21_16, rt in Omega(0)


Generator Equations:
gen_s14_16(0) <=> hole_s3_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