Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/2.13)

The rewrite relation of the following TRS is considered.

double(0) → 0 (1)
double(s(x)) → s(s(double(x))) (2)
+(x,0) → x (3)
+(x,s(y)) → s(+(x,y)) (4)
+(s(x),y) → s(+(x,y)) (5)
double(x) → +(x,x) (6)
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:
double#(0) → c (7)
originates from
double(0) → 0 (1)
double#(s(z0)) → c1(double#(z0)) (9)
originates from
double(s(z0)) → s(s(double(z0))) (8)
double#(z0) → c2(+#(z0,z0)) (11)
originates from
double(z0) → +(z0,z0) (10)
+#(z0,0) → c3 (13)
originates from
+(z0,0) → z0 (12)
+#(z0,s(z1)) → c4(+#(z0,z1)) (15)
originates from
+(z0,s(z1)) → s(+(z0,z1)) (14)
+#(s(z0),z1) → c5(+#(z0,z1)) (17)
originates from
+(s(z0),z1) → s(+(z0,z1)) (16)
Moreover, we add the following terms to the innermost strategy.
double#(0)
double#(s(z0))
double#(z0)
+#(z0,0)
+#(z0,s(z1))
+#(s(z0),z1)

1.1 Usable Rules

We remove the following rules since they are not usable.
double(0) → 0 (1)
double(s(z0)) → s(s(double(z0))) (8)
double(z0) → +(z0,z0) (10)
+(z0,0) → z0 (12)
+(z0,s(z1)) → s(+(z0,z1)) (14)
+(s(z0),z1) → s(+(z0,z1)) (16)

1.1.1 Rule Shifting

The rules
double#(0) → c (7)
double#(s(z0)) → c1(double#(z0)) (9)
double#(z0) → c2(+#(z0,z0)) (11)
+#(s(z0),z1) → c5(+#(z0,z1)) (17)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1)] = 1 · x1 + 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5(x1)] = 1 · x1 + 0
[double#(x1)] = 1 + 1 · x1
[+#(x1, x2)] = 1 · x1 + 0
[0] = 1
[s(x1)] = 1 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
double#(0) → c (7)
double#(s(z0)) → c1(double#(z0)) (9)
double#(z0) → c2(+#(z0,z0)) (11)
+#(z0,0) → c3 (13)
+#(z0,s(z1)) → c4(+#(z0,z1)) (15)
+#(s(z0),z1) → c5(+#(z0,z1)) (17)

1.1.1.1 Rule Shifting

The rules
+#(z0,0) → c3 (13)
+#(z0,s(z1)) → c4(+#(z0,z1)) (15)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1)] = 1 · x1 + 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5(x1)] = 1 · x1 + 0
[double#(x1)] = 1 + 1 · x1
[+#(x1, x2)] = 1 + 1 · x2
[0] = 0
[s(x1)] = 1 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
double#(0) → c (7)
double#(s(z0)) → c1(double#(z0)) (9)
double#(z0) → c2(+#(z0,z0)) (11)
+#(z0,0) → c3 (13)
+#(z0,s(z1)) → c4(+#(z0,z1)) (15)
+#(s(z0),z1) → c5(+#(z0,z1)) (17)

1.1.1.1.1 R is empty

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