Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/MYNAT_nosorts_FR)

The rewrite relation of the following TRS is considered.

and(tt,X) → activate(X) (1)
plus(N,0) → N (2)
plus(N,s(M)) → s(plus(N,M)) (3)
x(N,0) → 0 (4)
x(N,s(M)) → plus(x(N,M),N) (5)
activate(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(n2).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
and#(tt,z0) → c(activate#(z0)) (8)
originates from
and(tt,z0) → activate(z0) (7)
plus#(z0,0) → c1 (10)
originates from
plus(z0,0) → z0 (9)
plus#(z0,s(z1)) → c2(plus#(z0,z1)) (12)
originates from
plus(z0,s(z1)) → s(plus(z0,z1)) (11)
x#(z0,0) → c3 (14)
originates from
x(z0,0) → 0 (13)
x#(z0,s(z1)) → c4(plus#(x(z0,z1),z0),x#(z0,z1)) (16)
originates from
x(z0,s(z1)) → plus(x(z0,z1),z0) (15)
activate#(z0) → c5 (18)
originates from
activate(z0) → z0 (17)
Moreover, we add the following terms to the innermost strategy.
and#(tt,z0)
plus#(z0,0)
plus#(z0,s(z1))
x#(z0,0)
x#(z0,s(z1))
activate#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.
and(tt,z0) → activate(z0) (7)
activate(z0) → z0 (17)

1.1.1 Rule Shifting

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

1.1.1.1 Rule Shifting

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

1.1.1.1.1 Rule Shifting

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

1.1.1.1.1.1 R is empty

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