Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Der95/11)

The rewrite relation of the following TRS is considered.

D(t) → 1 (1)
D(constant) → 0 (2)
D(+(x,y)) → +(D(x),D(y)) (3)
D(*(x,y)) → +(*(y,D(x)),*(x,D(y))) (4)
D(-(x,y)) → -(D(x),D(y)) (5)
D(minus(x)) → minus(D(x)) (6)
D(div(x,y)) → -(div(D(x),y),div(*(x,D(y)),pow(y,2))) (7)
D(ln(x)) → div(D(x),x) (8)
D(pow(x,y)) → +(*(*(y,pow(x,-(y,1))),D(x)),*(*(pow(x,y),ln(x)),D(y))) (9)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
D#(t) → c (10)
originates from
D(t) → 1 (1)
D#(constant) → c1 (11)
originates from
D(constant) → 0 (2)
D#(+(z0,z1)) → c2(D#(z0),D#(z1)) (13)
originates from
D(+(z0,z1)) → +(D(z0),D(z1)) (12)
D#(*(z0,z1)) → c3(D#(z0),D#(z1)) (15)
originates from
D(*(z0,z1)) → +(*(z1,D(z0)),*(z0,D(z1))) (14)
D#(-(z0,z1)) → c4(D#(z0),D#(z1)) (17)
originates from
D(-(z0,z1)) → -(D(z0),D(z1)) (16)
D#(minus(z0)) → c5(D#(z0)) (19)
originates from
D(minus(z0)) → minus(D(z0)) (18)
D#(div(z0,z1)) → c6(D#(z0),D#(z1)) (21)
originates from
D(div(z0,z1)) → -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2))) (20)
D#(ln(z0)) → c7(D#(z0)) (23)
originates from
D(ln(z0)) → div(D(z0),z0) (22)
D#(pow(z0,z1)) → c8(D#(z0),D#(z1)) (25)
originates from
D(pow(z0,z1)) → +(*(*(z1,pow(z0,-(z1,1))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) (24)
Moreover, we add the following terms to the innermost strategy.
D#(t)
D#(constant)
D#(+(z0,z1))
D#(*(z0,z1))
D#(-(z0,z1))
D#(minus(z0))
D#(div(z0,z1))
D#(ln(z0))
D#(pow(z0,z1))

1.1 Usable Rules

We remove the following rules since they are not usable.
D(t) → 1 (1)
D(constant) → 0 (2)
D(+(z0,z1)) → +(D(z0),D(z1)) (12)
D(*(z0,z1)) → +(*(z1,D(z0)),*(z0,D(z1))) (14)
D(-(z0,z1)) → -(D(z0),D(z1)) (16)
D(minus(z0)) → minus(D(z0)) (18)
D(div(z0,z1)) → -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2))) (20)
D(ln(z0)) → div(D(z0),z0) (22)
D(pow(z0,z1)) → +(*(*(z1,pow(z0,-(z1,1))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) (24)

1.1.1 Rule Shifting

The rules
D#(t) → c (10)
D#(constant) → c1 (11)
D#(+(z0,z1)) → c2(D#(z0),D#(z1)) (13)
D#(*(z0,z1)) → c3(D#(z0),D#(z1)) (15)
D#(-(z0,z1)) → c4(D#(z0),D#(z1)) (17)
D#(minus(z0)) → c5(D#(z0)) (19)
D#(div(z0,z1)) → c6(D#(z0),D#(z1)) (21)
D#(ln(z0)) → c7(D#(z0)) (23)
D#(pow(z0,z1)) → c8(D#(z0),D#(z1)) (25)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c5(x1)] = 1 · x1 + 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1)] = 1 · x1 + 0
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[D#(x1)] = 2 · x1 + 0
[t] = 3
[constant] = 3
[+(x1, x2)] = 2 + 1 · x1 + 1 · x2
[*(x1, x2)] = 3 + 1 · x1 + 1 · x2
[-(x1, x2)] = 2 + 1 · x1 + 1 · x2
[minus(x1)] = 3 + 1 · x1
[div(x1, x2)] = 3 + 1 · x1 + 1 · x2
[ln(x1)] = 3 + 1 · x1
[pow(x1, x2)] = 2 + 1 · x1 + 1 · x2
which has the intended complexity. Here, only the following usable rules have been considered:
D#(t) → c (10)
D#(constant) → c1 (11)
D#(+(z0,z1)) → c2(D#(z0),D#(z1)) (13)
D#(*(z0,z1)) → c3(D#(z0),D#(z1)) (15)
D#(-(z0,z1)) → c4(D#(z0),D#(z1)) (17)
D#(minus(z0)) → c5(D#(z0)) (19)
D#(div(z0,z1)) → c6(D#(z0),D#(z1)) (21)
D#(ln(z0)) → c7(D#(z0)) (23)
D#(pow(z0,z1)) → c8(D#(z0),D#(z1)) (25)

1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).