WORST_CASE(?,O(n^1))
proof of input_k7ctx4OSzD.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxTRS
(9) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(10) CpxTRS
(11) CpxTrsMatchBoundsProof [FINISHED, 4 ms]
(12) BOUNDS(1, n^1)


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

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


The TRS R consists of the following rules:

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

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   sum(0) -> 0
   sum(s(z0)) -> +(sqr(s(z0)), sum(z0))
   sum(s(z0)) -> +(*(s(z0), s(z0)), sum(z0))
   sqr(z0) -> *(z0, z0)
Tuples:
   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
S tuples:
   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
K tuples:none
Defined Rule Symbols:   sum_1, sqr_1

Defined Pair Symbols:   SUM_1, SQR_1

Compound Symbols:   c, c1_1, c2_1, c3_1, c4


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 3 trailing nodes:
   SQR(z0) -> c4
   SUM(s(z0)) -> c1(SQR(s(z0)))
   SUM(0) -> c

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

(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)
Tuples:
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
S tuples:
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
K tuples:none
Defined Rule Symbols:   sum_1, sqr_1

Defined Pair Symbols:   SUM_1

Compound Symbols:   c2_1, c3_1


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

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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
S tuples:
   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   SUM_1

Compound Symbols:   c2_1, c3_1


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

(7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))

S is empty.
Rewrite Strategy: INNERMOST
----------------------------------------

(9) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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


The TRS R consists of the following rules:

   SUM(s(z0)) -> c2(SUM(z0))
   SUM(s(z0)) -> c3(SUM(z0))

S is empty.
Rewrite Strategy: INNERMOST
----------------------------------------

(11) CpxTrsMatchBoundsProof (FINISHED)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1. 
The certificate found is represented by the following graph.

"[43, 44, 45, 46]
{(43,44,[SUM_1|0]), (43,45,[c2_1|1]), (43,46,[c3_1|1]), (44,44,[s_1|0, c2_1|0, c3_1|0]), (45,44,[SUM_1|1]), (45,45,[c2_1|1]), (45,46,[c3_1|1]), (46,44,[SUM_1|1]), (46,45,[c2_1|1]), (46,46,[c3_1|1])}"
----------------------------------------

(12)
BOUNDS(1, n^1)