Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/AG01/#3.5)

The rewrite relation of the following TRS is considered.

le(0,y) → true (1)
le(s(x),0) → false (2)
le(s(x),s(y)) → le(x,y) (3)
minus(x,0) → x (4)
minus(s(x),s(y)) → minus(x,y) (5)
mod(0,y) → 0 (6)
mod(s(x),0) → 0 (7)
mod(s(x),s(y)) → if_mod(le(y,x),s(x),s(y)) (8)
if_mod(true,s(x),s(y)) → mod(minus(x,y),s(y)) (9)
if_mod(false,s(x),s(y)) → s(x) (10)
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:
le#(0,z0) → c (12)
originates from
le(0,z0) → true (11)
le#(s(z0),0) → c1 (14)
originates from
le(s(z0),0) → false (13)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
originates from
le(s(z0),s(z1)) → le(z0,z1) (15)
minus#(z0,0) → c3 (18)
originates from
minus(z0,0) → z0 (17)
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
originates from
minus(s(z0),s(z1)) → minus(z0,z1) (19)
mod#(0,z0) → c5 (22)
originates from
mod(0,z0) → 0 (21)
mod#(s(z0),0) → c6 (24)
originates from
mod(s(z0),0) → 0 (23)
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
originates from
mod(s(z0),s(z1)) → if_mod(le(z1,z0),s(z0),s(z1)) (25)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
originates from
if_mod(true,s(z0),s(z1)) → mod(minus(z0,z1),s(z1)) (27)
if_mod#(false,s(z0),s(z1)) → c9 (30)
originates from
if_mod(false,s(z0),s(z1)) → s(z0) (29)
Moreover, we add the following terms to the innermost strategy.
le#(0,z0)
le#(s(z0),0)
le#(s(z0),s(z1))
minus#(z0,0)
minus#(s(z0),s(z1))
mod#(0,z0)
mod#(s(z0),0)
mod#(s(z0),s(z1))
if_mod#(true,s(z0),s(z1))
if_mod#(false,s(z0),s(z1))

1.1 Usable Rules

We remove the following rules since they are not usable.
mod(0,z0) → 0 (21)
mod(s(z0),0) → 0 (23)
mod(s(z0),s(z1)) → if_mod(le(z1,z0),s(z0),s(z1)) (25)
if_mod(true,s(z0),s(z1)) → mod(minus(z0,z1),s(z1)) (27)
if_mod(false,s(z0),s(z1)) → s(z0) (29)

1.1.1 Rule Shifting

The rules
mod#(s(z0),0) → c6 (24)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
if_mod#(false,s(z0),s(z1)) → c9 (30)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[le(x1, x2)] = 1 + 1 · x1 + 1 · x2
[minus(x1, x2)] = 1 · x1 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 0
[mod#(x1, x2)] = 1 · x1 + 0
[if_mod#(x1, x2, x3)] = 1 · x2 + 0
[0] = 0
[s(x1)] = 1 + 1 · x1
[true] = 1
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (12)
le#(s(z0),0) → c1 (14)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
minus#(z0,0) → c3 (18)
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
mod#(0,z0) → c5 (22)
mod#(s(z0),0) → c6 (24)
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
if_mod#(false,s(z0),s(z1)) → c9 (30)
minus(s(z0),s(z1)) → minus(z0,z1) (19)
minus(z0,0) → z0 (17)

1.1.1.1 Rule Shifting

The rules
mod#(0,z0) → c5 (22)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[le(x1, x2)] = 0
[minus(x1, x2)] = 1 · x1 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 0
[mod#(x1, x2)] = 1 · x1 + 0
[if_mod#(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2
[0] = 1
[s(x1)] = 1 · x1 + 0
[true] = 0
[false] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (12)
le#(s(z0),0) → c1 (14)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
minus#(z0,0) → c3 (18)
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
mod#(0,z0) → c5 (22)
mod#(s(z0),0) → c6 (24)
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
if_mod#(false,s(z0),s(z1)) → c9 (30)
le(s(z0),s(z1)) → le(z0,z1) (15)
le(s(z0),0) → false (13)
le(0,z0) → true (11)
minus(s(z0),s(z1)) → minus(z0,z1) (19)
minus(z0,0) → z0 (17)

1.1.1.1.1 Rule Shifting

The rules
le#(0,z0) → c (12)
le#(s(z0),0) → c1 (14)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[le(x1, x2)] = 1 + 1 · x1 + 1 · x2
[minus(x1, x2)] = 1 · x1 + 0
[le#(x1, x2)] = 1
[minus#(x1, x2)] = 0
[mod#(x1, x2)] = 1 + 1 · x1
[if_mod#(x1, x2, x3)] = 1 · x2 + 0
[0] = 1
[s(x1)] = 1 + 1 · x1
[true] = 1
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (12)
le#(s(z0),0) → c1 (14)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
minus#(z0,0) → c3 (18)
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
mod#(0,z0) → c5 (22)
mod#(s(z0),0) → c6 (24)
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
if_mod#(false,s(z0),s(z1)) → c9 (30)
minus(s(z0),s(z1)) → minus(z0,z1) (19)
minus(z0,0) → z0 (17)

1.1.1.1.1.1 Rule Shifting

The rules
minus#(z0,0) → c3 (18)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[le(x1, x2)] = 1
[minus(x1, x2)] = 1 · x1 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 1
[mod#(x1, x2)] = 1 + 1 · x1
[if_mod#(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2
[0] = 1
[s(x1)] = 1 + 1 · x1
[true] = 1
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (12)
le#(s(z0),0) → c1 (14)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
minus#(z0,0) → c3 (18)
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
mod#(0,z0) → c5 (22)
mod#(s(z0),0) → c6 (24)
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
if_mod#(false,s(z0),s(z1)) → c9 (30)
le(s(z0),s(z1)) → le(z0,z1) (15)
le(s(z0),0) → false (13)
le(0,z0) → true (11)
minus(s(z0),s(z1)) → minus(z0,z1) (19)
minus(z0,0) → z0 (17)

1.1.1.1.1.1.1 Rule Shifting

The rules
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[le(x1, x2)] = 0
[minus(x1, x2)] = 1 · x1 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 0
[mod#(x1, x2)] = 1 + 1 · x1
[if_mod#(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2
[0] = 1
[s(x1)] = 1 + 1 · x1
[true] = 0
[false] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (12)
le#(s(z0),0) → c1 (14)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
minus#(z0,0) → c3 (18)
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
mod#(0,z0) → c5 (22)
mod#(s(z0),0) → c6 (24)
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
if_mod#(false,s(z0),s(z1)) → c9 (30)
le(s(z0),s(z1)) → le(z0,z1) (15)
le(s(z0),0) → false (13)
le(0,z0) → true (11)
minus(s(z0),s(z1)) → minus(z0,z1) (19)
minus(z0,0) → z0 (17)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[le(x1, x2)] = 0
[minus(x1, x2)] = 1 · x1 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 2 + 1 · x1
[mod#(x1, x2)] = 2 + 1 · x1 · x1
[if_mod#(x1, x2, x3)] = 1 · x2 · x2 + 0
[0] = 0
[s(x1)] = 2 + 1 · x1
[true] = 0
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (12)
le#(s(z0),0) → c1 (14)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
minus#(z0,0) → c3 (18)
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
mod#(0,z0) → c5 (22)
mod#(s(z0),0) → c6 (24)
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
if_mod#(false,s(z0),s(z1)) → c9 (30)
minus(s(z0),s(z1)) → minus(z0,z1) (19)
minus(z0,0) → z0 (17)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[le(x1, x2)] = 0
[minus(x1, x2)] = 1 · x1 + 0
[le#(x1, x2)] = 1 · x2 + 0
[minus#(x1, x2)] = 0
[mod#(x1, x2)] = 1 · x1 + 0 + 1 · x1 · x1
[if_mod#(x1, x2, x3)] = 1 · x2 · x2 + 0
[0] = 0
[s(x1)] = 1 + 1 · x1
[true] = 0
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (12)
le#(s(z0),0) → c1 (14)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (16)
minus#(z0,0) → c3 (18)
minus#(s(z0),s(z1)) → c4(minus#(z0,z1)) (20)
mod#(0,z0) → c5 (22)
mod#(s(z0),0) → c6 (24)
mod#(s(z0),s(z1)) → c7(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (26)
if_mod#(true,s(z0),s(z1)) → c8(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (28)
if_mod#(false,s(z0),s(z1)) → c9 (30)
minus(s(z0),s(z1)) → minus(z0,z1) (19)
minus(z0,0) → z0 (17)

1.1.1.1.1.1.1.1.1.1 R is empty

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