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), 250 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 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)), 17 ms]
    (12) CdtProblem
    (13) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) BOUNDS(1, 1)
(15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(16) TRS for Loop Detection
    (17) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
    (18) BEST
        (19) proven lower bound
            (20) LowerBoundPropagationProof [FINISHED, 0 ms]
            (21) BOUNDS(n^1, INF)
        (22) 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:

   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4

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

   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(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:

   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4

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

   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)
   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4
Tuples:
   SUM'(0) -> c5
   SUM'(s(z0)) -> c6(SQR'(s(z0)), SUM'(z0))
   SUM'(s(z0)) -> c7(SUM'(z0))
   SQR'(z0) -> c8
   SUM''(0) -> c9
   SUM''(s(z0)) -> c10(SQR''(s(z0)))
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
   SQR''(z0) -> c13
S tuples:
   SUM''(0) -> c9
   SUM''(s(z0)) -> c10(SQR''(s(z0)))
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
   SQR''(z0) -> c13
K tuples:none
Defined Rule Symbols:   SUM_1, SQR_1, sum_1, sqr_1

Defined Pair Symbols:   SUM'_1, SQR'_1, SUM''_1, SQR''_1

Compound Symbols:   c5, c6_2, c7_1, c8, c9, c10_1, c11_1, c12_1, c13


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 5 trailing nodes:
   SUM''(0) -> c9
   SQR''(z0) -> c13
   SUM'(0) -> c5
   SQR'(z0) -> c8
   SUM''(s(z0)) -> c10(SQR''(s(z0)))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)
   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4
Tuples:
   SUM'(s(z0)) -> c6(SQR'(s(z0)), SUM'(z0))
   SUM'(s(z0)) -> c7(SUM'(z0))
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
S tuples:
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
K tuples:none
Defined Rule Symbols:   SUM_1, SQR_1, sum_1, sqr_1

Defined Pair Symbols:   SUM'_1, SUM''_1

Compound Symbols:   c6_2, c7_1, c11_1, c12_1


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

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)
   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4
Tuples:
   SUM'(s(z0)) -> c7(SUM'(z0))
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
   SUM'(s(z0)) -> c6(SUM'(z0))
S tuples:
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
K tuples:none
Defined Rule Symbols:   SUM_1, SQR_1, sum_1, sqr_1

Defined Pair Symbols:   SUM'_1, SUM''_1

Compound Symbols:   c7_1, c11_1, c12_1, c6_1


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

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)
   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   SUM'(s(z0)) -> c7(SUM'(z0))
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
   SUM'(s(z0)) -> c6(SUM'(z0))
S tuples:
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   SUM'_1, SUM''_1

Compound Symbols:   c7_1, c11_1, c12_1, c6_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.
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
We considered the (Usable) Rules:none
And the Tuples:
   SUM'(s(z0)) -> c7(SUM'(z0))
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
   SUM'(s(z0)) -> c6(SUM'(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(SUM'(x_1)) = x_1
   POL(SUM''(x_1)) = x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1)) = x_1
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   SUM'(s(z0)) -> c7(SUM'(z0))
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
   SUM'(s(z0)) -> c6(SUM'(z0))
S tuples:none
K tuples:
   SUM''(s(z0)) -> c11(SUM''(z0))
   SUM''(s(z0)) -> c12(SUM''(z0))
Defined Rule Symbols:none

Defined Pair Symbols:   SUM'_1, SUM''_1

Compound Symbols:   c7_1, c11_1, c12_1, c6_1


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

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

(14)
BOUNDS(1, 1)

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

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

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

   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4

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

   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)

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

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

The rewrite sequence

SUM(s(z0)) ->^+ c3(SUM(z0))

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 [ ].




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

(18)
Complex Obligation (BEST)

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

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

   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4

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

   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)

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

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

(21)
BOUNDS(n^1, INF)

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

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


The TRS R consists of the following rules:

   SUM(0) -> c
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
   SQR(z0) -> c4

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

   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)

Rewrite Strategy: INNERMOST