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), 551 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 42 ms]
    (10) CdtProblem
    (11) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) BOUNDS(1, 1)
(13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(14) TRS for Loop Detection
    (15) DecreasingLoopProof [LOWER BOUND(ID), 15 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) TRS for Loop Detection


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

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


The TRS R consists of the following rules:

   FST(0, z0) -> c
   FST(s(z0), cons(z1, z2)) -> c1(ACTIVATE(z0))
   FST(s(z0), cons(z1, z2)) -> c2(ACTIVATE(z2))
   FST(z0, z1) -> c3
   FROM(z0) -> c4
   FROM(z0) -> c5
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ACTIVATE(z0))
   ADD(z0, z1) -> c8
   LEN(nil) -> c9
   LEN(cons(z0, z1)) -> c10(ACTIVATE(z1))
   LEN(z0) -> c11
   ACTIVATE(n__fst(z0, z1)) -> c12(FST(z0, z1))
   ACTIVATE(n__from(z0)) -> c13(FROM(z0))
   ACTIVATE(n__add(z0, z1)) -> c14(ADD(z0, z1))
   ACTIVATE(n__len(z0)) -> c15(LEN(z0))
   ACTIVATE(z0) -> c16

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

   fst(0, z0) -> nil
   fst(s(z0), cons(z1, z2)) -> cons(z1, n__fst(activate(z0), activate(z2)))
   fst(z0, z1) -> n__fst(z0, z1)
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(n__add(activate(z0), z1))
   add(z0, z1) -> n__add(z0, z1)
   len(nil) -> 0
   len(cons(z0, z1)) -> s(n__len(activate(z1)))
   len(z0) -> n__len(z0)
   activate(n__fst(z0, z1)) -> fst(z0, z1)
   activate(n__from(z0)) -> from(z0)
   activate(n__add(z0, z1)) -> add(z0, z1)
   activate(n__len(z0)) -> len(z0)
   activate(z0) -> z0

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:

   FST(0, z0) -> c
   FST(s(z0), cons(z1, z2)) -> c1(ACTIVATE(z0))
   FST(s(z0), cons(z1, z2)) -> c2(ACTIVATE(z2))
   FST(z0, z1) -> c3
   FROM(z0) -> c4
   FROM(z0) -> c5
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ACTIVATE(z0))
   ADD(z0, z1) -> c8
   LEN(nil) -> c9
   LEN(cons(z0, z1)) -> c10(ACTIVATE(z1))
   LEN(z0) -> c11
   ACTIVATE(n__fst(z0, z1)) -> c12(FST(z0, z1))
   ACTIVATE(n__from(z0)) -> c13(FROM(z0))
   ACTIVATE(n__add(z0, z1)) -> c14(ADD(z0, z1))
   ACTIVATE(n__len(z0)) -> c15(LEN(z0))
   ACTIVATE(z0) -> c16

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

   fst(0, z0) -> nil
   fst(s(z0), cons(z1, z2)) -> cons(z1, n__fst(activate(z0), activate(z2)))
   fst(z0, z1) -> n__fst(z0, z1)
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(n__add(activate(z0), z1))
   add(z0, z1) -> n__add(z0, z1)
   len(nil) -> 0
   len(cons(z0, z1)) -> s(n__len(activate(z1)))
   len(z0) -> n__len(z0)
   activate(n__fst(z0, z1)) -> fst(z0, z1)
   activate(n__from(z0)) -> from(z0)
   activate(n__add(z0, z1)) -> add(z0, z1)
   activate(n__len(z0)) -> len(z0)
   activate(z0) -> z0

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fst(0, z0) -> nil
   fst(s(z0), cons(z1, z2)) -> cons(z1, n__fst(activate(z0), activate(z2)))
   fst(z0, z1) -> n__fst(z0, z1)
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(n__add(activate(z0), z1))
   add(z0, z1) -> n__add(z0, z1)
   len(nil) -> 0
   len(cons(z0, z1)) -> s(n__len(activate(z1)))
   len(z0) -> n__len(z0)
   activate(n__fst(z0, z1)) -> fst(z0, z1)
   activate(n__from(z0)) -> from(z0)
   activate(n__add(z0, z1)) -> add(z0, z1)
   activate(n__len(z0)) -> len(z0)
   activate(z0) -> z0
   FST(0, z0) -> c
   FST(s(z0), cons(z1, z2)) -> c1(ACTIVATE(z0))
   FST(s(z0), cons(z1, z2)) -> c2(ACTIVATE(z2))
   FST(z0, z1) -> c3
   FROM(z0) -> c4
   FROM(z0) -> c5
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ACTIVATE(z0))
   ADD(z0, z1) -> c8
   LEN(nil) -> c9
   LEN(cons(z0, z1)) -> c10(ACTIVATE(z1))
   LEN(z0) -> c11
   ACTIVATE(n__fst(z0, z1)) -> c12(FST(z0, z1))
   ACTIVATE(n__from(z0)) -> c13(FROM(z0))
   ACTIVATE(n__add(z0, z1)) -> c14(ADD(z0, z1))
   ACTIVATE(n__len(z0)) -> c15(LEN(z0))
   ACTIVATE(z0) -> c16
Tuples:
   FST'(0, z0) -> c17
   FST'(s(z0), cons(z1, z2)) -> c18(ACTIVATE'(z0), ACTIVATE'(z2))
   FST'(z0, z1) -> c19
   FROM'(z0) -> c20
   FROM'(z0) -> c21
   ADD'(0, z0) -> c22
   ADD'(s(z0), z1) -> c23(ACTIVATE'(z0))
   ADD'(z0, z1) -> c24
   LEN'(nil) -> c25
   LEN'(cons(z0, z1)) -> c26(ACTIVATE'(z1))
   LEN'(z0) -> c27
   ACTIVATE'(n__fst(z0, z1)) -> c28(FST'(z0, z1))
   ACTIVATE'(n__from(z0)) -> c29(FROM'(z0))
   ACTIVATE'(n__add(z0, z1)) -> c30(ADD'(z0, z1))
   ACTIVATE'(n__len(z0)) -> c31(LEN'(z0))
   ACTIVATE'(z0) -> c32
   FST''(0, z0) -> c33
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   FST''(z0, z1) -> c36
   FROM''(z0) -> c37
   FROM''(z0) -> c38
   ADD''(0, z0) -> c39
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   ADD''(z0, z1) -> c41
   LEN''(nil) -> c42
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   LEN''(z0) -> c44
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__from(z0)) -> c46(FROM''(z0))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
   ACTIVATE''(z0) -> c49
S tuples:
   FST''(0, z0) -> c33
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   FST''(z0, z1) -> c36
   FROM''(z0) -> c37
   FROM''(z0) -> c38
   ADD''(0, z0) -> c39
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   ADD''(z0, z1) -> c41
   LEN''(nil) -> c42
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   LEN''(z0) -> c44
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__from(z0)) -> c46(FROM''(z0))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
   ACTIVATE''(z0) -> c49
K tuples:none
Defined Rule Symbols:   FST_2, FROM_1, ADD_2, LEN_1, ACTIVATE_1, fst_2, from_1, add_2, len_1, activate_1

Defined Pair Symbols:   FST'_2, FROM'_1, ADD'_2, LEN'_1, ACTIVATE'_1, FST''_2, FROM''_1, ADD''_2, LEN''_1, ACTIVATE''_1

Compound Symbols:   c17, c18_2, c19, c20, c21, c22, c23_1, c24, c25, c26_1, c27, c28_1, c29_1, c30_1, c31_1, c32, c33, c34_1, c35_1, c36, c37, c38, c39, c40_1, c41, c42, c43_1, c44, c45_1, c46_1, c47_1, c48_1, c49


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 20 trailing nodes:
   ADD'(0, z0) -> c22
   ADD''(z0, z1) -> c41
   FROM''(z0) -> c38
   LEN'(nil) -> c25
   FST'(0, z0) -> c17
   FST''(0, z0) -> c33
   LEN''(nil) -> c42
   ADD'(z0, z1) -> c24
   ACTIVATE'(n__from(z0)) -> c29(FROM'(z0))
   ADD''(0, z0) -> c39
   LEN'(z0) -> c27
   FROM'(z0) -> c20
   FROM''(z0) -> c37
   FST'(z0, z1) -> c19
   ACTIVATE''(z0) -> c49
   ACTIVATE''(n__from(z0)) -> c46(FROM''(z0))
   ACTIVATE'(z0) -> c32
   LEN''(z0) -> c44
   FROM'(z0) -> c21
   FST''(z0, z1) -> c36

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fst(0, z0) -> nil
   fst(s(z0), cons(z1, z2)) -> cons(z1, n__fst(activate(z0), activate(z2)))
   fst(z0, z1) -> n__fst(z0, z1)
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(n__add(activate(z0), z1))
   add(z0, z1) -> n__add(z0, z1)
   len(nil) -> 0
   len(cons(z0, z1)) -> s(n__len(activate(z1)))
   len(z0) -> n__len(z0)
   activate(n__fst(z0, z1)) -> fst(z0, z1)
   activate(n__from(z0)) -> from(z0)
   activate(n__add(z0, z1)) -> add(z0, z1)
   activate(n__len(z0)) -> len(z0)
   activate(z0) -> z0
   FST(0, z0) -> c
   FST(s(z0), cons(z1, z2)) -> c1(ACTIVATE(z0))
   FST(s(z0), cons(z1, z2)) -> c2(ACTIVATE(z2))
   FST(z0, z1) -> c3
   FROM(z0) -> c4
   FROM(z0) -> c5
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ACTIVATE(z0))
   ADD(z0, z1) -> c8
   LEN(nil) -> c9
   LEN(cons(z0, z1)) -> c10(ACTIVATE(z1))
   LEN(z0) -> c11
   ACTIVATE(n__fst(z0, z1)) -> c12(FST(z0, z1))
   ACTIVATE(n__from(z0)) -> c13(FROM(z0))
   ACTIVATE(n__add(z0, z1)) -> c14(ADD(z0, z1))
   ACTIVATE(n__len(z0)) -> c15(LEN(z0))
   ACTIVATE(z0) -> c16
Tuples:
   FST'(s(z0), cons(z1, z2)) -> c18(ACTIVATE'(z0), ACTIVATE'(z2))
   ADD'(s(z0), z1) -> c23(ACTIVATE'(z0))
   LEN'(cons(z0, z1)) -> c26(ACTIVATE'(z1))
   ACTIVATE'(n__fst(z0, z1)) -> c28(FST'(z0, z1))
   ACTIVATE'(n__add(z0, z1)) -> c30(ADD'(z0, z1))
   ACTIVATE'(n__len(z0)) -> c31(LEN'(z0))
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
S tuples:
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
K tuples:none
Defined Rule Symbols:   FST_2, FROM_1, ADD_2, LEN_1, ACTIVATE_1, fst_2, from_1, add_2, len_1, activate_1

Defined Pair Symbols:   FST'_2, ADD'_2, LEN'_1, ACTIVATE'_1, FST''_2, ADD''_2, LEN''_1, ACTIVATE''_1

Compound Symbols:   c18_2, c23_1, c26_1, c28_1, c30_1, c31_1, c34_1, c35_1, c40_1, c43_1, c45_1, c47_1, c48_1


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   fst(0, z0) -> nil
   fst(s(z0), cons(z1, z2)) -> cons(z1, n__fst(activate(z0), activate(z2)))
   fst(z0, z1) -> n__fst(z0, z1)
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(n__add(activate(z0), z1))
   add(z0, z1) -> n__add(z0, z1)
   len(nil) -> 0
   len(cons(z0, z1)) -> s(n__len(activate(z1)))
   len(z0) -> n__len(z0)
   activate(n__fst(z0, z1)) -> fst(z0, z1)
   activate(n__from(z0)) -> from(z0)
   activate(n__add(z0, z1)) -> add(z0, z1)
   activate(n__len(z0)) -> len(z0)
   activate(z0) -> z0
   FST(0, z0) -> c
   FST(s(z0), cons(z1, z2)) -> c1(ACTIVATE(z0))
   FST(s(z0), cons(z1, z2)) -> c2(ACTIVATE(z2))
   FST(z0, z1) -> c3
   FROM(z0) -> c4
   FROM(z0) -> c5
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ACTIVATE(z0))
   ADD(z0, z1) -> c8
   LEN(nil) -> c9
   LEN(cons(z0, z1)) -> c10(ACTIVATE(z1))
   LEN(z0) -> c11
   ACTIVATE(n__fst(z0, z1)) -> c12(FST(z0, z1))
   ACTIVATE(n__from(z0)) -> c13(FROM(z0))
   ACTIVATE(n__add(z0, z1)) -> c14(ADD(z0, z1))
   ACTIVATE(n__len(z0)) -> c15(LEN(z0))
   ACTIVATE(z0) -> c16

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   FST'(s(z0), cons(z1, z2)) -> c18(ACTIVATE'(z0), ACTIVATE'(z2))
   ADD'(s(z0), z1) -> c23(ACTIVATE'(z0))
   LEN'(cons(z0, z1)) -> c26(ACTIVATE'(z1))
   ACTIVATE'(n__fst(z0, z1)) -> c28(FST'(z0, z1))
   ACTIVATE'(n__add(z0, z1)) -> c30(ADD'(z0, z1))
   ACTIVATE'(n__len(z0)) -> c31(LEN'(z0))
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
S tuples:
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   FST'_2, ADD'_2, LEN'_1, ACTIVATE'_1, FST''_2, ADD''_2, LEN''_1, ACTIVATE''_1

Compound Symbols:   c18_2, c23_1, c26_1, c28_1, c30_1, c31_1, c34_1, c35_1, c40_1, c43_1, c45_1, c47_1, c48_1


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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
We considered the (Usable) Rules:none
And the Tuples:
   FST'(s(z0), cons(z1, z2)) -> c18(ACTIVATE'(z0), ACTIVATE'(z2))
   ADD'(s(z0), z1) -> c23(ACTIVATE'(z0))
   LEN'(cons(z0, z1)) -> c26(ACTIVATE'(z1))
   ACTIVATE'(n__fst(z0, z1)) -> c28(FST'(z0, z1))
   ACTIVATE'(n__add(z0, z1)) -> c30(ADD'(z0, z1))
   ACTIVATE'(n__len(z0)) -> c31(LEN'(z0))
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(ACTIVATE'(x_1)) = [1] + x_1
   POL(ACTIVATE''(x_1)) = [1] + x_1
   POL(ADD'(x_1, x_2)) = [1] + x_1 + x_2
   POL(ADD''(x_1, x_2)) = [1] + x_1 + x_2
   POL(FST'(x_1, x_2)) = x_1 + x_2
   POL(FST''(x_1, x_2)) = [1] + x_1 + x_2
   POL(LEN'(x_1)) = [1] + x_1
   POL(LEN''(x_1)) = [1] + x_1
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c23(x_1)) = x_1
   POL(c26(x_1)) = x_1
   POL(c28(x_1)) = x_1
   POL(c30(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c34(x_1)) = x_1
   POL(c35(x_1)) = x_1
   POL(c40(x_1)) = x_1
   POL(c43(x_1)) = x_1
   POL(c45(x_1)) = x_1
   POL(c47(x_1)) = x_1
   POL(c48(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_2
   POL(n__add(x_1, x_2)) = [1] + x_1 + x_2
   POL(n__fst(x_1, x_2)) = [1] + x_1 + x_2
   POL(n__len(x_1)) = [1] + x_1
   POL(s(x_1)) = [1] + x_1

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   FST'(s(z0), cons(z1, z2)) -> c18(ACTIVATE'(z0), ACTIVATE'(z2))
   ADD'(s(z0), z1) -> c23(ACTIVATE'(z0))
   LEN'(cons(z0, z1)) -> c26(ACTIVATE'(z1))
   ACTIVATE'(n__fst(z0, z1)) -> c28(FST'(z0, z1))
   ACTIVATE'(n__add(z0, z1)) -> c30(ADD'(z0, z1))
   ACTIVATE'(n__len(z0)) -> c31(LEN'(z0))
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
S tuples:none
K tuples:
   FST''(s(z0), cons(z1, z2)) -> c34(ACTIVATE''(z0))
   FST''(s(z0), cons(z1, z2)) -> c35(ACTIVATE''(z2))
   ADD''(s(z0), z1) -> c40(ACTIVATE''(z0))
   LEN''(cons(z0, z1)) -> c43(ACTIVATE''(z1))
   ACTIVATE''(n__fst(z0, z1)) -> c45(FST''(z0, z1))
   ACTIVATE''(n__add(z0, z1)) -> c47(ADD''(z0, z1))
   ACTIVATE''(n__len(z0)) -> c48(LEN''(z0))
Defined Rule Symbols:none

Defined Pair Symbols:   FST'_2, ADD'_2, LEN'_1, ACTIVATE'_1, FST''_2, ADD''_2, LEN''_1, ACTIVATE''_1

Compound Symbols:   c18_2, c23_1, c26_1, c28_1, c30_1, c31_1, c34_1, c35_1, c40_1, c43_1, c45_1, c47_1, c48_1


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

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

(12)
BOUNDS(1, 1)

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

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

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

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


The TRS R consists of the following rules:

   FST(0, z0) -> c
   FST(s(z0), cons(z1, z2)) -> c1(ACTIVATE(z0))
   FST(s(z0), cons(z1, z2)) -> c2(ACTIVATE(z2))
   FST(z0, z1) -> c3
   FROM(z0) -> c4
   FROM(z0) -> c5
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ACTIVATE(z0))
   ADD(z0, z1) -> c8
   LEN(nil) -> c9
   LEN(cons(z0, z1)) -> c10(ACTIVATE(z1))
   LEN(z0) -> c11
   ACTIVATE(n__fst(z0, z1)) -> c12(FST(z0, z1))
   ACTIVATE(n__from(z0)) -> c13(FROM(z0))
   ACTIVATE(n__add(z0, z1)) -> c14(ADD(z0, z1))
   ACTIVATE(n__len(z0)) -> c15(LEN(z0))
   ACTIVATE(z0) -> c16

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

   fst(0, z0) -> nil
   fst(s(z0), cons(z1, z2)) -> cons(z1, n__fst(activate(z0), activate(z2)))
   fst(z0, z1) -> n__fst(z0, z1)
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(n__add(activate(z0), z1))
   add(z0, z1) -> n__add(z0, z1)
   len(nil) -> 0
   len(cons(z0, z1)) -> s(n__len(activate(z1)))
   len(z0) -> n__len(z0)
   activate(n__fst(z0, z1)) -> fst(z0, z1)
   activate(n__from(z0)) -> from(z0)
   activate(n__add(z0, z1)) -> add(z0, z1)
   activate(n__len(z0)) -> len(z0)
   activate(z0) -> z0

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

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

The rewrite sequence

ACTIVATE(n__add(s(z01_2), z1)) ->^+ c14(c7(ACTIVATE(z01_2)))

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

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

The result substitution is [ ].




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

(16)
Complex Obligation (BEST)

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

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

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


The TRS R consists of the following rules:

   FST(0, z0) -> c
   FST(s(z0), cons(z1, z2)) -> c1(ACTIVATE(z0))
   FST(s(z0), cons(z1, z2)) -> c2(ACTIVATE(z2))
   FST(z0, z1) -> c3
   FROM(z0) -> c4
   FROM(z0) -> c5
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ACTIVATE(z0))
   ADD(z0, z1) -> c8
   LEN(nil) -> c9
   LEN(cons(z0, z1)) -> c10(ACTIVATE(z1))
   LEN(z0) -> c11
   ACTIVATE(n__fst(z0, z1)) -> c12(FST(z0, z1))
   ACTIVATE(n__from(z0)) -> c13(FROM(z0))
   ACTIVATE(n__add(z0, z1)) -> c14(ADD(z0, z1))
   ACTIVATE(n__len(z0)) -> c15(LEN(z0))
   ACTIVATE(z0) -> c16

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

   fst(0, z0) -> nil
   fst(s(z0), cons(z1, z2)) -> cons(z1, n__fst(activate(z0), activate(z2)))
   fst(z0, z1) -> n__fst(z0, z1)
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(n__add(activate(z0), z1))
   add(z0, z1) -> n__add(z0, z1)
   len(nil) -> 0
   len(cons(z0, z1)) -> s(n__len(activate(z1)))
   len(z0) -> n__len(z0)
   activate(n__fst(z0, z1)) -> fst(z0, z1)
   activate(n__from(z0)) -> from(z0)
   activate(n__add(z0, z1)) -> add(z0, z1)
   activate(n__len(z0)) -> len(z0)
   activate(z0) -> z0

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

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

(19)
BOUNDS(n^1, INF)

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

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

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


The TRS R consists of the following rules:

   FST(0, z0) -> c
   FST(s(z0), cons(z1, z2)) -> c1(ACTIVATE(z0))
   FST(s(z0), cons(z1, z2)) -> c2(ACTIVATE(z2))
   FST(z0, z1) -> c3
   FROM(z0) -> c4
   FROM(z0) -> c5
   ADD(0, z0) -> c6
   ADD(s(z0), z1) -> c7(ACTIVATE(z0))
   ADD(z0, z1) -> c8
   LEN(nil) -> c9
   LEN(cons(z0, z1)) -> c10(ACTIVATE(z1))
   LEN(z0) -> c11
   ACTIVATE(n__fst(z0, z1)) -> c12(FST(z0, z1))
   ACTIVATE(n__from(z0)) -> c13(FROM(z0))
   ACTIVATE(n__add(z0, z1)) -> c14(ADD(z0, z1))
   ACTIVATE(n__len(z0)) -> c15(LEN(z0))
   ACTIVATE(z0) -> c16

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

   fst(0, z0) -> nil
   fst(s(z0), cons(z1, z2)) -> cons(z1, n__fst(activate(z0), activate(z2)))
   fst(z0, z1) -> n__fst(z0, z1)
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(n__add(activate(z0), z1))
   add(z0, z1) -> n__add(z0, z1)
   len(nil) -> 0
   len(cons(z0, z1)) -> s(n__len(activate(z1)))
   len(z0) -> n__len(z0)
   activate(n__fst(z0, z1)) -> fst(z0, z1)
   activate(n__from(z0)) -> from(z0)
   activate(n__add(z0, z1)) -> add(z0, z1)
   activate(n__len(z0)) -> len(z0)
   activate(z0) -> z0

Rewrite Strategy: INNERMOST