Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/AG01/#3.5b)

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(0,y) → 0 (4)
minus(s(x),y) → if_minus(le(s(x),y),s(x),y) (5)
if_minus(true,s(x),y) → 0 (6)
if_minus(false,s(x),y) → s(minus(x,y)) (7)
mod(0,y) → 0 (8)
mod(s(x),0) → 0 (9)
mod(s(x),s(y)) → if_mod(le(y,x),s(x),s(y)) (10)
if_mod(true,s(x),s(y)) → mod(minus(x,y),s(y)) (11)
if_mod(false,s(x),s(y)) → s(x) (12)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n3).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
le#(0,z0) → c (14)
originates from
le(0,z0) → true (13)
le#(s(z0),0) → c1 (16)
originates from
le(s(z0),0) → false (15)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
originates from
le(s(z0),s(z1)) → le(z0,z1) (17)
minus#(0,z0) → c3 (20)
originates from
minus(0,z0) → 0 (19)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
originates from
minus(s(z0),z1) → if_minus(le(s(z0),z1),s(z0),z1) (21)
if_minus#(true,s(z0),z1) → c5 (24)
originates from
if_minus(true,s(z0),z1) → 0 (23)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
originates from
if_minus(false,s(z0),z1) → s(minus(z0,z1)) (25)
mod#(0,z0) → c7 (28)
originates from
mod(0,z0) → 0 (27)
mod#(s(z0),0) → c8 (30)
originates from
mod(s(z0),0) → 0 (29)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
originates from
mod(s(z0),s(z1)) → if_mod(le(z1,z0),s(z0),s(z1)) (31)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
originates from
if_mod(true,s(z0),s(z1)) → mod(minus(z0,z1),s(z1)) (33)
if_mod#(false,s(z0),s(z1)) → c11 (36)
originates from
if_mod(false,s(z0),s(z1)) → s(z0) (35)
Moreover, we add the following terms to the innermost strategy.
le#(0,z0)
le#(s(z0),0)
le#(s(z0),s(z1))
minus#(0,z0)
minus#(s(z0),z1)
if_minus#(true,s(z0),z1)
if_minus#(false,s(z0),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 (27)
mod(s(z0),0) → 0 (29)
mod(s(z0),s(z1)) → if_mod(le(z1,z0),s(z0),s(z1)) (31)
if_mod(true,s(z0),s(z1)) → mod(minus(z0,z1),s(z1)) (33)
if_mod(false,s(z0),s(z1)) → s(z0) (35)

1.1.1 Rule Shifting

The rules
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
if_mod#(false,s(z0),s(z1)) → c11 (36)
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, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7] = 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11] = 0
[le(x1, x2)] = 1 · x2 + 0
[minus(x1, x2)] = 1 + 1 · x2
[if_minus(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 0
[if_minus#(x1, x2, x3)] = 1 · x2 + 0
[mod#(x1, x2)] = 1 + 1 · x2
[if_mod#(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[0] = 0
[s(x1)] = 0
[false] = 0
[true] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (16)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
minus#(0,z0) → c3 (20)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
if_minus#(true,s(z0),z1) → c5 (24)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
if_mod#(false,s(z0),s(z1)) → c11 (36)

1.1.1.1 Rule Shifting

The rules
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
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, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7] = 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11] = 0
[le(x1, x2)] = 1 · x2 + 0
[minus(x1, x2)] = 1 · x1 + 0
[if_minus(x1, x2, x3)] = 1 · x2 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 0
[if_minus#(x1, x2, x3)] = 0
[mod#(x1, x2)] = 1 · x1 + 0
[if_mod#(x1, x2, x3)] = 1 · x2 + 0
[0] = 0
[s(x1)] = 1 + 1 · x1
[false] = 1
[true] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (16)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
minus#(0,z0) → c3 (20)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
if_minus#(true,s(z0),z1) → c5 (24)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
if_mod#(false,s(z0),s(z1)) → c11 (36)
minus(s(z0),z1) → if_minus(le(s(z0),z1),s(z0),z1) (21)
if_minus(false,s(z0),z1) → s(minus(z0,z1)) (25)
if_minus(true,s(z0),z1) → 0 (23)
minus(0,z0) → 0 (19)

1.1.1.1.1 Rule Shifting

The rules
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
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, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7] = 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11] = 0
[le(x1, x2)] = 1 · x2 + 0
[minus(x1, x2)] = 1 · x1 + 0
[if_minus(x1, x2, x3)] = 1 · x2 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 0
[if_minus#(x1, x2, x3)] = 0
[mod#(x1, x2)] = 1 + 1 · x1
[if_mod#(x1, x2, x3)] = 1 · x2 + 0
[0] = 0
[s(x1)] = 1 + 1 · x1
[false] = 1
[true] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (16)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
minus#(0,z0) → c3 (20)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
if_minus#(true,s(z0),z1) → c5 (24)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
if_mod#(false,s(z0),s(z1)) → c11 (36)
minus(s(z0),z1) → if_minus(le(s(z0),z1),s(z0),z1) (21)
if_minus(false,s(z0),z1) → s(minus(z0,z1)) (25)
if_minus(true,s(z0),z1) → 0 (23)
minus(0,z0) → 0 (19)

1.1.1.1.1.1 Rule Shifting

The rules
minus#(0,z0) → c3 (20)
if_minus#(true,s(z0),z1) → c5 (24)
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, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7] = 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11] = 0
[le(x1, x2)] = 1 · x2 + 0
[minus(x1, x2)] = 1 · x1 + 0
[if_minus(x1, x2, x3)] = 1 · x2 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 1
[if_minus#(x1, x2, x3)] = 1
[mod#(x1, x2)] = 1 · x1 + 0
[if_mod#(x1, x2, x3)] = 1 · x2 + 0
[0] = 0
[s(x1)] = 1 + 1 · x1
[false] = 1
[true] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (16)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
minus#(0,z0) → c3 (20)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
if_minus#(true,s(z0),z1) → c5 (24)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
if_mod#(false,s(z0),s(z1)) → c11 (36)
minus(s(z0),z1) → if_minus(le(s(z0),z1),s(z0),z1) (21)
if_minus(false,s(z0),z1) → s(minus(z0,z1)) (25)
if_minus(true,s(z0),z1) → 0 (23)
minus(0,z0) → 0 (19)

1.1.1.1.1.1.1 Rule Shifting

The rules
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
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, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7] = 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11] = 0
[le(x1, x2)] = 0
[minus(x1, x2)] = 1 · x1 + 0
[if_minus(x1, x2, x3)] = 1 · x2 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 1 · x1 + 0
[if_minus#(x1, x2, x3)] = 1 · x2 + 0
[mod#(x1, x2)] = 2 · x2 + 0 + 1 · x2 · x2 + 1 · x1 · x1
[if_mod#(x1, x2, x3)] = 2 · x3 + 0 + 1 · x3 · x3 + 1 · x2 · x2
[0] = 0
[s(x1)] = 1 + 1 · x1
[false] = 0
[true] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (16)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
minus#(0,z0) → c3 (20)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
if_minus#(true,s(z0),z1) → c5 (24)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
if_mod#(false,s(z0),s(z1)) → c11 (36)
minus(s(z0),z1) → if_minus(le(s(z0),z1),s(z0),z1) (21)
if_minus(false,s(z0),z1) → s(minus(z0,z1)) (25)
if_minus(true,s(z0),z1) → 0 (23)
minus(0,z0) → 0 (19)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
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, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7] = 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11] = 0
[le(x1, x2)] = 0
[minus(x1, x2)] = 1 · x1 + 0
[if_minus(x1, x2, x3)] = 1 · x2 + 0
[le#(x1, x2)] = 0
[minus#(x1, x2)] = 1 + 2 · x1
[if_minus#(x1, x2, x3)] = 2 · x2 + 0
[mod#(x1, x2)] = 1 · x1 · x1 + 0
[if_mod#(x1, x2, x3)] = 1 · x2 · x2 + 0
[0] = 0
[s(x1)] = 2 + 1 · x1
[false] = 0
[true] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (16)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
minus#(0,z0) → c3 (20)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
if_minus#(true,s(z0),z1) → c5 (24)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
if_mod#(false,s(z0),s(z1)) → c11 (36)
minus(s(z0),z1) → if_minus(le(s(z0),z1),s(z0),z1) (21)
if_minus(false,s(z0),z1) → s(minus(z0,z1)) (25)
if_minus(true,s(z0),z1) → 0 (23)
minus(0,z0) → 0 (19)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (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, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7] = 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11] = 0
[le(x1, x2)] = 0
[minus(x1, x2)] = 1 · x1 + 0
[if_minus(x1, x2, x3)] = 1 · x2 + 0
[le#(x1, x2)] = 1
[minus#(x1, x2)] = 2 + 2 · x1
[if_minus#(x1, x2, x3)] = 2 · x2 + 0
[mod#(x1, x2)] = 2 + 2 · x1 + 2 · x1 · x2 + 2 · x1 · x1
[if_mod#(x1, x2, x3)] = 2 · x2 · x3 + 0 + 2 · x2 · x2
[0] = 0
[s(x1)] = 2 + 1 · x1
[false] = 0
[true] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (16)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
minus#(0,z0) → c3 (20)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
if_minus#(true,s(z0),z1) → c5 (24)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
if_mod#(false,s(z0),s(z1)) → c11 (36)
minus(s(z0),z1) → if_minus(le(s(z0),z1),s(z0),z1) (21)
if_minus(false,s(z0),z1) → s(minus(z0,z1)) (25)
if_minus(true,s(z0),z1) → 0 (23)
minus(0,z0) → 0 (19)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
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, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7] = 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11] = 0
[le(x1, x2)] = 0
[minus(x1, x2)] = 1 · x1 + 0
[if_minus(x1, x2, x3)] = 1 · x2 + 0
[le#(x1, x2)] = 1 + 1 · x1
[minus#(x1, x2)] = 1 + 1 · x1 + 1 · x1 · x1
[if_minus#(x1, x2, x3)] = 1 · x2 · x2 + 0
[mod#(x1, x2)] = 1 · x1 + 0 + 1 · x2 + 1 · x1 · x2 + 1 · x1 · x1 · x1
[if_mod#(x1, x2, x3)] = 1 · x2 + 0 + 1 · x2 · x3 + 1 · x2 · x2 · x2
[0] = 0
[s(x1)] = 1 + 1 · x1
[false] = 0
[true] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
le#(0,z0) → c (14)
le#(s(z0),0) → c1 (16)
le#(s(z0),s(z1)) → c2(le#(z0,z1)) (18)
minus#(0,z0) → c3 (20)
minus#(s(z0),z1) → c4(if_minus#(le(s(z0),z1),s(z0),z1),le#(s(z0),z1)) (22)
if_minus#(true,s(z0),z1) → c5 (24)
if_minus#(false,s(z0),z1) → c6(minus#(z0,z1)) (26)
mod#(0,z0) → c7 (28)
mod#(s(z0),0) → c8 (30)
mod#(s(z0),s(z1)) → c9(if_mod#(le(z1,z0),s(z0),s(z1)),le#(z1,z0)) (32)
if_mod#(true,s(z0),s(z1)) → c10(mod#(minus(z0,z1),s(z1)),minus#(z0,z1)) (34)
if_mod#(false,s(z0),s(z1)) → c11 (36)
minus(s(z0),z1) → if_minus(le(s(z0),z1),s(z0),z1) (21)
if_minus(false,s(z0),z1) → s(minus(z0,z1)) (25)
if_minus(true,s(z0),z1) → 0 (23)
minus(0,z0) → 0 (19)

1.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).