WORST_CASE(Omega(n^1),O(n^3))
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^3).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 292 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 6 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 1 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 115 ms]
    (12) CdtProblem
    (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 53 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 51 ms]
    (16) CdtProblem
    (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^3)), 1292 ms]
    (18) CdtProblem
    (19) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (20) BOUNDS(1, 1)
(21) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(22) TRS for Loop Detection
    (23) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
    (24) BEST
        (25) proven lower bound
            (26) LowerBoundPropagationProof [FINISHED, 0 ms]
            (27) BOUNDS(n^1, INF)
        (28) TRS for Loop Detection


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

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


The TRS R consists of the following rules:

   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))

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

   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(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^3).


The TRS R consists of the following rules:

   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))

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

   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))
Tuples:
   +''(0, z0) -> c10
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(0) -> c13
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(0, z0) -> c16
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(0, z0) -> c19
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(0) -> c22
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(0, z0) -> c25
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c28(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), MINUS''(z1))
S tuples:
   +'''(0, z0) -> c19
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(0) -> c22
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(0, z0) -> c25
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c28(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), MINUS''(z1))
K tuples:none
Defined Rule Symbols:   +'_2, MINUS_1, *'_2, +_2, minus_1, *_2

Defined Pair Symbols:   +''_2, MINUS'_1, *''_2, +'''_2, MINUS''_1, *'''_2

Compound Symbols:   c10, c11_1, c12_1, c13, c14_1, c15_1, c16, c17_2, c18_3, c19, c20_1, c21_1, c22, c23_1, c24_1, c25, c26_3, c27_4, c28_4


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 6 trailing nodes:
   MINUS''(0) -> c22
   +''(0, z0) -> c10
   *''(0, z0) -> c16
   *'''(0, z0) -> c25
   +'''(0, z0) -> c19
   MINUS'(0) -> c13

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))
Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c28(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), MINUS''(z1))
S tuples:
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c28(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), MINUS''(z1))
K tuples:none
Defined Rule Symbols:   +'_2, MINUS_1, *'_2, +_2, minus_1, *_2

Defined Pair Symbols:   +''_2, MINUS'_1, *''_2, +'''_2, MINUS''_1, *'''_2

Compound Symbols:   c11_1, c12_1, c14_1, c15_1, c17_2, c18_3, c20_1, c21_1, c23_1, c24_1, c26_3, c27_4, c28_4


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

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))
Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
S tuples:
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
K tuples:none
Defined Rule Symbols:   +'_2, MINUS_1, *'_2, +_2, minus_1, *_2

Defined Pair Symbols:   +''_2, MINUS'_1, *''_2, +'''_2, MINUS''_1, *'''_2

Compound Symbols:   c11_1, c12_1, c14_1, c15_1, c17_2, c18_3, c20_1, c21_1, c23_1, c24_1, c26_3, c27_4, c10_1


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

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
S tuples:
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
K tuples:none
Defined Rule Symbols:   *_2, +_2, minus_1

Defined Pair Symbols:   +''_2, MINUS'_1, *''_2, +'''_2, MINUS''_1, *'''_2

Compound Symbols:   c11_1, c12_1, c14_1, c15_1, c17_2, c18_3, c20_1, c21_1, c23_1, c24_1, c26_3, c27_4, c10_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.
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
We considered the (Usable) Rules:none
And the Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(*(x_1, x_2)) = [3]x_2
   POL(*''(x_1, x_2)) = 0
   POL(*'''(x_1, x_2)) = [2] + x_2
   POL(+(x_1, x_2)) = [3]
   POL(+''(x_1, x_2)) = 0
   POL(+'''(x_1, x_2)) = 0
   POL(0) = [1]
   POL(MINUS'(x_1)) = 0
   POL(MINUS''(x_1)) = [2]
   POL(c10(x_1)) = x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1)) = x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c20(x_1)) = x_1
   POL(c21(x_1)) = x_1
   POL(c23(x_1)) = x_1
   POL(c24(x_1)) = x_1
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c27(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(minus(x_1)) = [2] + [2]x_1
   POL(p(x_1)) = [2]
   POL(s(x_1)) = 0

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
S tuples:
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
K tuples:
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
Defined Rule Symbols:   *_2, +_2, minus_1

Defined Pair Symbols:   +''_2, MINUS'_1, *''_2, +'''_2, MINUS''_1, *'''_2

Compound Symbols:   c11_1, c12_1, c14_1, c15_1, c17_2, c18_3, c20_1, c21_1, c23_1, c24_1, c26_3, c27_4, c10_1


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

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   *'''(p(z0), z1) -> c10(MINUS''(z1))
We considered the (Usable) Rules:none
And the Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(*(x_1, x_2)) = [3]x_2
   POL(*''(x_1, x_2)) = 0
   POL(*'''(x_1, x_2)) = [3]
   POL(+(x_1, x_2)) = [3]
   POL(+''(x_1, x_2)) = 0
   POL(+'''(x_1, x_2)) = 0
   POL(0) = 0
   POL(MINUS'(x_1)) = 0
   POL(MINUS''(x_1)) = [1]
   POL(c10(x_1)) = x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1)) = x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c20(x_1)) = x_1
   POL(c21(x_1)) = x_1
   POL(c23(x_1)) = x_1
   POL(c24(x_1)) = x_1
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c27(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(minus(x_1)) = [2]x_1
   POL(p(x_1)) = [2]
   POL(s(x_1)) = [2]

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
S tuples:
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
K tuples:
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
Defined Rule Symbols:   *_2, +_2, minus_1

Defined Pair Symbols:   +''_2, MINUS'_1, *''_2, +'''_2, MINUS''_1, *'''_2

Compound Symbols:   c11_1, c12_1, c14_1, c15_1, c17_2, c18_3, c20_1, c21_1, c23_1, c24_1, c26_3, c27_4, c10_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.
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(*(x_1, x_2)) = [1] + x_1 + x_2
   POL(*''(x_1, x_2)) = 0
   POL(*'''(x_1, x_2)) = [1] + x_1 + x_2
   POL(+(x_1, x_2)) = [1] + x_1 + x_2
   POL(+''(x_1, x_2)) = 0
   POL(+'''(x_1, x_2)) = 0
   POL(0) = [1]
   POL(MINUS'(x_1)) = 0
   POL(MINUS''(x_1)) = x_1
   POL(c10(x_1)) = x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1)) = x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c20(x_1)) = x_1
   POL(c21(x_1)) = x_1
   POL(c23(x_1)) = x_1
   POL(c24(x_1)) = x_1
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c27(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(minus(x_1)) = [1] + x_1
   POL(p(x_1)) = [1] + x_1
   POL(s(x_1)) = [1] + x_1

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
S tuples:
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
K tuples:
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
Defined Rule Symbols:   *_2, +_2, minus_1

Defined Pair Symbols:   +''_2, MINUS'_1, *''_2, +'''_2, MINUS''_1, *'''_2

Compound Symbols:   c11_1, c12_1, c14_1, c15_1, c17_2, c18_3, c20_1, c21_1, c23_1, c24_1, c26_3, c27_4, c10_1


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

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
We considered the (Usable) Rules:
   +(s(z0), z1) -> s(+(z0, z1))
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   minus(0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   minus(s(z0)) -> p(minus(z0))
   +(p(z0), z1) -> p(+(z0, z1))
   +(0, z0) -> z0
And the Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(*(x_1, x_2)) = x_2 + x_1*x_2
   POL(*''(x_1, x_2)) = x_1*x_2
   POL(*'''(x_1, x_2)) = x_2 + x_2^2 + x_1^2*x_2 + x_2^3
   POL(+(x_1, x_2)) = x_1 + x_2
   POL(+''(x_1, x_2)) = 0
   POL(+'''(x_1, x_2)) = x_1
   POL(0) = 0
   POL(MINUS'(x_1)) = 0
   POL(MINUS''(x_1)) = x_1 + x_1^2 + x_1^3
   POL(c10(x_1)) = x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1)) = x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c20(x_1)) = x_1
   POL(c21(x_1)) = x_1
   POL(c23(x_1)) = x_1
   POL(c24(x_1)) = x_1
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c27(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(minus(x_1)) = x_1
   POL(p(x_1)) = [1] + x_1
   POL(s(x_1)) = [1] + x_1

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

(18)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))
   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
Tuples:
   +''(s(z0), z1) -> c11(+''(z0, z1))
   +''(p(z0), z1) -> c12(+''(z0, z1))
   MINUS'(s(z0)) -> c14(MINUS'(z0))
   MINUS'(p(z0)) -> c15(MINUS'(z0))
   *''(s(z0), z1) -> c17(+''(*(z0, z1), z1), *''(z0, z1))
   *''(p(z0), z1) -> c18(+''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
S tuples:none
K tuples:
   *'''(p(z0), z1) -> c10(+'''(*(z0, z1), minus(z1)))
   *'''(p(z0), z1) -> c10(*''(z0, z1))
   *'''(p(z0), z1) -> c10(MINUS'(z1))
   *'''(p(z0), z1) -> c10(MINUS''(z1))
   MINUS''(s(z0)) -> c23(MINUS''(z0))
   MINUS''(p(z0)) -> c24(MINUS''(z0))
   *'''(s(z0), z1) -> c26(+'''(*(z0, z1), z1), *''(z0, z1), *'''(z0, z1))
   *'''(p(z0), z1) -> c27(+'''(*(z0, z1), minus(z1)), *''(z0, z1), MINUS'(z1), *'''(z0, z1))
   +'''(s(z0), z1) -> c20(+'''(z0, z1))
   +'''(p(z0), z1) -> c21(+'''(z0, z1))
Defined Rule Symbols:   *_2, +_2, minus_1

Defined Pair Symbols:   +''_2, MINUS'_1, *''_2, +'''_2, MINUS''_1, *'''_2

Compound Symbols:   c11_1, c12_1, c14_1, c15_1, c17_2, c18_3, c20_1, c21_1, c23_1, c24_1, c26_3, c27_4, c10_1


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

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

(20)
BOUNDS(1, 1)

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

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

(22)
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^3).


The TRS R consists of the following rules:

   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))

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

   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))

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

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

The rewrite sequence

+'(s(z0), z1) ->^+ c1(+'(z0, z1))

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

The pumping substitution is [z0 / s(z0)].

The result substitution is [ ].




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

(24)
Complex Obligation (BEST)

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

(25)
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^3).


The TRS R consists of the following rules:

   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))

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

   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))

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

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

(27)
BOUNDS(n^1, INF)

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

(28)
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^3).


The TRS R consists of the following rules:

   +'(0, z0) -> c
   +'(s(z0), z1) -> c1(+'(z0, z1))
   +'(p(z0), z1) -> c2(+'(z0, z1))
   MINUS(0) -> c3
   MINUS(s(z0)) -> c4(MINUS(z0))
   MINUS(p(z0)) -> c5(MINUS(z0))
   *'(0, z0) -> c6
   *'(s(z0), z1) -> c7(+'(*(z0, z1), z1), *'(z0, z1))
   *'(p(z0), z1) -> c8(+'(*(z0, z1), minus(z1)), *'(z0, z1))
   *'(p(z0), z1) -> c9(+'(*(z0, z1), minus(z1)), MINUS(z1))

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

   +(0, z0) -> z0
   +(s(z0), z1) -> s(+(z0, z1))
   +(p(z0), z1) -> p(+(z0, z1))
   minus(0) -> 0
   minus(s(z0)) -> p(minus(z0))
   minus(p(z0)) -> s(minus(z0))
   *(0, z0) -> 0
   *(s(z0), z1) -> +(*(z0, z1), z1)
   *(p(z0), z1) -> +(*(z0, z1), minus(z1))

Rewrite Strategy: INNERMOST