Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/2.16)

The rewrite relation of the following TRS is considered.

f(0) → 1 (1)
f(s(x)) → g(x,s(x)) (2)
g(0,y) → y (3)
g(s(x),y) → g(x,+(y,s(x))) (4)
+(x,0) → x (5)
+(x,s(y)) → s(+(x,y)) (6)
g(s(x),y) → g(x,s(+(y,x))) (7)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n2).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
f#(0) → c (8)
originates from
f(0) → 1 (1)
f#(s(z0)) → c1(g#(z0,s(z0))) (10)
originates from
f(s(z0)) → g(z0,s(z0)) (9)
g#(0,z0) → c2 (12)
originates from
g(0,z0) → z0 (11)
g#(s(z0),z1) → c3(g#(z0,+(z1,s(z0))),+#(z1,s(z0))) (14)
originates from
g(s(z0),z1) → g(z0,+(z1,s(z0))) (13)
g#(s(z0),z1) → c4(g#(z0,s(+(z1,z0))),+#(z1,z0)) (16)
originates from
g(s(z0),z1) → g(z0,s(+(z1,z0))) (15)
+#(z0,0) → c5 (18)
originates from
+(z0,0) → z0 (17)
+#(z0,s(z1)) → c6(+#(z0,z1)) (20)
originates from
+(z0,s(z1)) → s(+(z0,z1)) (19)
Moreover, we add the following terms to the innermost strategy.
f#(0)
f#(s(z0))
g#(0,z0)
g#(s(z0),z1)
g#(s(z0),z1)
+#(z0,0)
+#(z0,s(z1))

1.1 Usable Rules

We remove the following rules since they are not usable.
f(0) → 1 (1)
f(s(z0)) → g(z0,s(z0)) (9)
g(0,z0) → z0 (11)
g(s(z0),z1) → g(z0,+(z1,s(z0))) (13)
g(s(z0),z1) → g(z0,s(+(z1,z0))) (15)

1.1.1 Rule Shifting

The rules
f#(0) → c (8)
f#(s(z0)) → c1(g#(z0,s(z0))) (10)
g#(s(z0),z1) → c3(g#(z0,+(z1,s(z0))),+#(z1,s(z0))) (14)
g#(s(z0),z1) → c4(g#(z0,s(+(z1,z0))),+#(z1,z0)) (16)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[+(x1, x2)] = 3 · x1 + 0
[f#(x1)] = 1 + 3 · x1
[g#(x1, x2)] = 3 · x1 + 0
[+#(x1, x2)] = 0
[s(x1)] = 2 + 1 · x1
[0] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
f#(0) → c (8)
f#(s(z0)) → c1(g#(z0,s(z0))) (10)
g#(0,z0) → c2 (12)
g#(s(z0),z1) → c3(g#(z0,+(z1,s(z0))),+#(z1,s(z0))) (14)
g#(s(z0),z1) → c4(g#(z0,s(+(z1,z0))),+#(z1,z0)) (16)
+#(z0,0) → c5 (18)
+#(z0,s(z1)) → c6(+#(z0,z1)) (20)

1.1.1.1 Rule Shifting

The rules
g#(0,z0) → c2 (12)
+#(z0,0) → c5 (18)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[+(x1, x2)] = 1 + 1 · x1 + 1 · x2
[f#(x1)] = 1 + 1 · x1
[g#(x1, x2)] = 1 + 1 · x1
[+#(x1, x2)] = 1
[s(x1)] = 1 + 1 · x1
[0] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
f#(0) → c (8)
f#(s(z0)) → c1(g#(z0,s(z0))) (10)
g#(0,z0) → c2 (12)
g#(s(z0),z1) → c3(g#(z0,+(z1,s(z0))),+#(z1,s(z0))) (14)
g#(s(z0),z1) → c4(g#(z0,s(+(z1,z0))),+#(z1,z0)) (16)
+#(z0,0) → c5 (18)
+#(z0,s(z1)) → c6(+#(z0,z1)) (20)

1.1.1.1.1 Rule Shifting

The rules
+#(z0,s(z1)) → c6(+#(z0,z1)) (20)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[+(x1, x2)] = 2 + 2 · x2 · x2
[f#(x1)] = 2 · x1 + 0 + 1 · x1 · x1
[g#(x1, x2)] = 1 · x1 + 0 + 1 · x1 · x1
[+#(x1, x2)] = 1 · x2 + 0
[s(x1)] = 2 + 1 · x1
[0] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
f#(0) → c (8)
f#(s(z0)) → c1(g#(z0,s(z0))) (10)
g#(0,z0) → c2 (12)
g#(s(z0),z1) → c3(g#(z0,+(z1,s(z0))),+#(z1,s(z0))) (14)
g#(s(z0),z1) → c4(g#(z0,s(+(z1,z0))),+#(z1,z0)) (16)
+#(z0,0) → c5 (18)
+#(z0,s(z1)) → c6(+#(z0,z1)) (20)

1.1.1.1.1.1 R is empty

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