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), 310 ms]
(2) CpxRelTRS
(3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(4) CpxTRS
    (5) CpxTrsMatchBoundsTAProof [FINISHED, 53 ms]
    (6) BOUNDS(1, n^1)
(7) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(8) TRS for Loop Detection
    (9) DecreasingLoopProof [LOWER BOUND(ID), 5 ms]
    (10) BEST
        (11) proven lower bound
            (12) LowerBoundPropagationProof [FINISHED, 0 ms]
            (13) BOUNDS(n^1, INF)
        (14) 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:

   F(0) -> c
   F(s(0)) -> c1
   F(s(0)) -> c2(F(0))
   F(+(z0, s(0))) -> c3(F(z0))
   F(+(z0, z1)) -> c4(F(z0))
   F(+(z0, z1)) -> c5(F(z1))

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

   f(0) -> s(0)
   f(s(0)) -> s(s(0))
   f(s(0)) -> *(s(s(0)), f(0))
   f(+(z0, s(0))) -> +(s(s(0)), f(z0))
   f(+(z0, z1)) -> *(f(z0), f(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) -> c
   F(s(0)) -> c1
   F(s(0)) -> c2(F(0))
   F(+(z0, s(0))) -> c3(F(z0))
   F(+(z0, z1)) -> c4(F(z0))
   F(+(z0, z1)) -> c5(F(z1))

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

   f(0) -> s(0)
   f(s(0)) -> s(s(0))
   f(s(0)) -> *(s(s(0)), f(0))
   f(+(z0, s(0))) -> +(s(s(0)), f(z0))
   f(+(z0, z1)) -> *(f(z0), f(z1))

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

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

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

   F(0) -> c
   F(s(0)) -> c1
   F(s(0)) -> c2(F(0))
   F(+(z0, s(0))) -> c3(F(z0))
   F(+(z0, z1)) -> c4(F(z0))
   F(+(z0, z1)) -> c5(F(z1))
   f(0) -> s(0)
   f(s(0)) -> s(s(0))
   f(s(0)) -> *(s(s(0)), f(0))
   f(+(z0, s(0))) -> +(s(s(0)), f(z0))
   f(+(z0, z1)) -> *(f(z0), f(z1))

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

(5) CpxTrsMatchBoundsTAProof (FINISHED)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2. 

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: 
final states : [1, 2]
transitions: 
00() -> 0
c0() -> 0
s0(0) -> 0
c10() -> 0
c20(0) -> 0
+0(0, 0) -> 0
c30(0) -> 0
c40(0) -> 0
c50(0) -> 0
*0(0, 0) -> 0
F0(0) -> 1
f0(0) -> 2
c1() -> 1
c11() -> 1
01() -> 4
F1(4) -> 3
c21(3) -> 1
F1(0) -> 5
c31(5) -> 1
F1(0) -> 6
c41(6) -> 1
F1(0) -> 7
c51(7) -> 1
01() -> 8
s1(8) -> 2
s1(8) -> 9
s1(9) -> 2
s1(9) -> 10
01() -> 12
f1(12) -> 11
*1(10, 11) -> 2
s1(9) -> 13
f1(0) -> 14
+1(13, 14) -> 2
f1(0) -> 15
f1(0) -> 16
*1(15, 16) -> 2
c1() -> 5
c1() -> 6
c1() -> 7
c2() -> 3
c11() -> 5
c11() -> 6
c11() -> 7
c21(3) -> 5
c21(3) -> 6
c21(3) -> 7
c31(5) -> 5
c31(5) -> 6
c31(5) -> 7
c41(6) -> 5
c41(6) -> 6
c41(6) -> 7
c51(7) -> 5
c51(7) -> 6
c51(7) -> 7
s1(8) -> 14
s1(8) -> 15
s1(8) -> 16
02() -> 17
s2(17) -> 11
s1(9) -> 14
s1(9) -> 15
s1(9) -> 16
*1(10, 11) -> 14
*1(10, 11) -> 15
*1(10, 11) -> 16
+1(13, 14) -> 14
+1(13, 14) -> 15
+1(13, 14) -> 16
*1(15, 16) -> 14
*1(15, 16) -> 15
*1(15, 16) -> 16

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

(6)
BOUNDS(1, n^1)

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

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

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

   F(0) -> c
   F(s(0)) -> c1
   F(s(0)) -> c2(F(0))
   F(+(z0, s(0))) -> c3(F(z0))
   F(+(z0, z1)) -> c4(F(z0))
   F(+(z0, z1)) -> c5(F(z1))

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

   f(0) -> s(0)
   f(s(0)) -> s(s(0))
   f(s(0)) -> *(s(s(0)), f(0))
   f(+(z0, s(0))) -> +(s(s(0)), f(z0))
   f(+(z0, z1)) -> *(f(z0), f(z1))

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

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

The rewrite sequence

F(+(z0, s(0))) ->^+ c3(F(z0))

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

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

The result substitution is [ ].




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

(10)
Complex Obligation (BEST)

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

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

   F(0) -> c
   F(s(0)) -> c1
   F(s(0)) -> c2(F(0))
   F(+(z0, s(0))) -> c3(F(z0))
   F(+(z0, z1)) -> c4(F(z0))
   F(+(z0, z1)) -> c5(F(z1))

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

   f(0) -> s(0)
   f(s(0)) -> s(s(0))
   f(s(0)) -> *(s(s(0)), f(0))
   f(+(z0, s(0))) -> +(s(s(0)), f(z0))
   f(+(z0, z1)) -> *(f(z0), f(z1))

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

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

(13)
BOUNDS(n^1, INF)

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

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

   F(0) -> c
   F(s(0)) -> c1
   F(s(0)) -> c2(F(0))
   F(+(z0, s(0))) -> c3(F(z0))
   F(+(z0, z1)) -> c4(F(z0))
   F(+(z0, z1)) -> c5(F(z1))

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

   f(0) -> s(0)
   f(s(0)) -> s(s(0))
   f(s(0)) -> *(s(s(0)), f(0))
   f(+(z0, s(0))) -> +(s(s(0)), f(z0))
   f(+(z0, z1)) -> *(f(z0), f(z1))

Rewrite Strategy: INNERMOST