Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/AProVE_04/JFP_Ex51)

The rewrite relation of the following TRS is considered.

minus_active(0,y) → 0 (1)
mark(0) → 0 (2)
minus_active(s(x),s(y)) → minus_active(x,y) (3)
mark(s(x)) → s(mark(x)) (4)
ge_active(x,0) → true (5)
mark(minus(x,y)) → minus_active(x,y) (6)
ge_active(0,s(y)) → false (7)
mark(ge(x,y)) → ge_active(x,y) (8)
ge_active(s(x),s(y)) → ge_active(x,y) (9)
mark(div(x,y)) → div_active(mark(x),y) (10)
div_active(0,s(y)) → 0 (11)
mark(if(x,y,z)) → if_active(mark(x),y,z) (12)
div_active(s(x),s(y)) → if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0) (13)
if_active(true,x,y) → mark(x) (14)
minus_active(x,y) → minus(x,y) (15)
if_active(false,x,y) → mark(y) (16)
ge_active(x,y) → ge(x,y) (17)
if_active(x,y,z) → if(x,y,z) (18)
div_active(x,y) → div(x,y) (19)
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:
minus_active#(0,z0) → c (21)
originates from
minus_active(0,z0) → 0 (20)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
originates from
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
minus_active#(z0,z1) → c2 (25)
originates from
minus_active(z0,z1) → minus(z0,z1) (24)
mark#(0) → c3 (26)
originates from
mark(0) → 0 (2)
mark#(s(z0)) → c4(mark#(z0)) (28)
originates from
mark(s(z0)) → s(mark(z0)) (27)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
originates from
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
originates from
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
originates from
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
originates from
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active#(z0,0) → c9 (38)
originates from
ge_active(z0,0) → true (37)
ge_active#(0,s(z0)) → c10 (40)
originates from
ge_active(0,s(z0)) → false (39)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
originates from
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
ge_active#(z0,z1) → c12 (44)
originates from
ge_active(z0,z1) → ge(z0,z1) (43)
div_active#(0,s(z0)) → c13 (46)
originates from
div_active(0,s(z0)) → 0 (45)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
originates from
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active#(z0,z1) → c15 (50)
originates from
div_active(z0,z1) → div(z0,z1) (49)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
originates from
if_active(true,z0,z1) → mark(z0) (51)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
originates from
if_active(false,z0,z1) → mark(z1) (53)
if_active#(z0,z1,z2) → c18 (56)
originates from
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
Moreover, we add the following terms to the innermost strategy.
minus_active#(0,z0)
minus_active#(s(z0),s(z1))
minus_active#(z0,z1)
mark#(0)
mark#(s(z0))
mark#(minus(z0,z1))
mark#(ge(z0,z1))
mark#(div(z0,z1))
mark#(if(z0,z1,z2))
ge_active#(z0,0)
ge_active#(0,s(z0))
ge_active#(s(z0),s(z1))
ge_active#(z0,z1)
div_active#(0,s(z0))
div_active#(s(z0),s(z1))
div_active#(z0,z1)
if_active#(true,z0,z1)
if_active#(false,z0,z1)
if_active#(z0,z1,z2)

1.1 Rule Shifting

The rules
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[c10] = 0
[c11(x1)] = 1 · x1 + 0
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1)] = 1 · x1 + 0
[c17(x1)] = 1 · x1 + 0
[c18] = 0
[minus_active(x1, x2)] = 1 + 1 · x1 + 1 · x2
[mark(x1)] = 1
[ge_active(x1, x2)] = 0
[div_active(x1, x2)] = 1 + 1 · x1 + 1 · x2
[if_active(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[minus_active#(x1, x2)] = 0
[mark#(x1)] = 1 · x1 + 0
[ge_active#(x1, x2)] = 0
[div_active#(x1, x2)] = 0
[if_active#(x1, x2, x3)] = 1 · x2 + 0 + 1 · x3
[0] = 0
[true] = 1
[s(x1)] = 1 · x1 + 0
[false] = 1
[ge(x1, x2)] = 1 + 1 · x1 + 1 · x2
[minus(x1, x2)] = 0
[div(x1, x2)] = 1 · x1 + 0
[if(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)

1.1.1 Rule Shifting

The rules
div_active#(0,s(z0)) → c13 (46)
div_active#(z0,z1) → c15 (50)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c9] = 0
[c10] = 0
[c11(x1)] = 1 · x1 + 0
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15] = 0
[c16(x1)] = 1 · x1 + 0
[c17(x1)] = 1 · x1 + 0
[c18] = 0
[minus_active(x1, x2)] = 1 + 1 · x1 + 1 · x2
[mark(x1)] = 1
[ge_active(x1, x2)] = 0
[div_active(x1, x2)] = 1 + 1 · x1 + 1 · x2
[if_active(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[minus_active#(x1, x2)] = 0
[mark#(x1)] = 1 · x1 + 0
[ge_active#(x1, x2)] = 0
[div_active#(x1, x2)] = 1
[if_active#(x1, x2, x3)] = 1 · x2 + 0 + 1 · x3
[0] = 0
[true] = 1
[s(x1)] = 1 · x1 + 0
[false] = 1
[ge(x1, x2)] = 1 + 1 · x1 + 1 · x2
[minus(x1, x2)] = 0
[div(x1, x2)] = 1 + 1 · x1
[if(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)

1.1.1.1 Rule Shifting

The rules
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
if_active#(z0,z1,z2) → c18 (56)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
1 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
1 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
0 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 1
0 0
· x1 +
0 0
0 0
· x2
[c3] =
1 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
1 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[ge(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
1 0
0 0
+
1 0
0 0
· x1 +
2 0
0 1
· x2 +
2 0
0 1
· x3
[false] =
0 0
0 0
[s(x1)] =
0 0
2 0
+
1 0
0 0
· x1
[div(x1, x2)] =
1 0
0 0
+
1 1
0 1
· x1 +
0 0
0 0
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
1 0
0 0
+
1 1
0 1
· x1 +
0 0
0 0
· x2
[mark(x1)] =
0 0
0 0
+
2 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1 Rule Shifting

The rules
mark#(s(z0)) → c4(mark#(z0)) (28)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
0 0
3 0
+
1 4
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 0
0 0
· x1 +
1 4
0 0
· x2 +
1 4
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
4 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 4
0 0
· x1 +
0 4
0 0
· x2
[c3] =
0 0
3 0
[c4(x1)] =
3 0
0 0
+
1 4
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
0 0
0 0
+
1 2
0 1
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[ge(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
0 0
0 0
+
1 2
0 1
· x1 +
2 0
0 1
· x2 +
2 0
0 1
· x3
[false] =
0 0
0 0
[s(x1)] =
0 0
4 0
+
1 4
0 0
· x1
[div(x1, x2)] =
0 0
0 0
+
1 4
0 1
· x1 +
0 4
0 0
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
0 0
+
1 4
0 1
· x1 +
0 4
0 0
· x2
[mark(x1)] =
0 0
0 0
+
2 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1 Rule Shifting

The rules
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
2 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 2
0 0
· x1 +
0 1
0 0
· x2
[c3] =
0 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[ge(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[false] =
0 0
0 0
[s(x1)] =
0 0
2 0
+
1 0
0 0
· x1
[div(x1, x2)] =
0 0
0 0
+
1 2
0 1
· x1 +
0 2
0 0
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
0 0
+
1 2
0 1
· x1 +
0 2
0 0
· x2
[mark(x1)] =
0 0
0 0
+
1 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1.1 Rule Shifting

The rules
minus_active#(z0,z1) → c2 (25)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
1 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
0 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 1
0 0
· x1 +
0 0
0 0
· x2
[c3] =
0 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
1 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
2 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
1 0
0 0
+
1 1
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[ge(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
2 0
0 0
+
1 1
0 0
· x1 +
4 0
0 2
· x2 +
4 0
0 2
· x3
[false] =
0 0
0 0
[s(x1)] =
0 0
2 0
+
1 0
0 0
· x1
[div(x1, x2)] =
0 0
4 0
+
1 2
0 0
· x1 +
0 0
0 0
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
1 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
4 0
+
1 4
0 0
· x1 +
0 0
0 0
· x2
[mark(x1)] =
0 0
0 0
+
4 0
0 2
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
minus_active#(0,z0) → c (21)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
3 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
1 0
[mark#(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
2 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
4 0
0 0
[c9] =
0 0
2 0
[c10] =
0 0
2 0
[c13] =
0 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 4
0 0
· x1 +
0 0
0 0
· x2
[c3] =
0 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
4 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
4 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[ge(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[false] =
0 0
0 0
[s(x1)] =
0 0
2 0
+
1 2
0 0
· x1
[div(x1, x2)] =
0 0
0 0
+
1 4
0 0
· x1 +
0 0
0 1
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
4 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
0 0
+
1 4
0 0
· x1 +
0 0
0 1
· x2
[mark(x1)] =
0 0
0 0
+
1 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
mark#(0) → c3 (26)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
4 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 2
0 0
· x1 +
0 3
0 0
· x2
[c3] =
3 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
4 0
0 0
[minus_active(x1, x2)] =
4 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
0 0
0 0
+
1 2
0 0
· x1 +
1 0
0 1
· x2 +
1 1
0 1
· x3
[ge(x1, x2)] =
4 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
4 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
0 0
0 0
+
1 2
0 0
· x1 +
1 0
0 1
· x2 +
1 1
0 1
· x3
[false] =
4 0
0 0
[s(x1)] =
0 0
4 0
+
1 0
0 0
· x1
[div(x1, x2)] =
0 0
4 0
+
1 2
0 0
· x1 +
0 4
0 0
· x2
[0] =
4 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
4 0
+
1 2
0 0
· x1 +
0 4
0 0
· x2
[mark(x1)] =
4 0
0 0
+
1 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
1 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
0 0
2 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
2 0
+
0 4
0 0
· x1 +
0 0
0 0
· x2
[c3] =
0 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 1
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
2 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
0 0
0 0
+
0 2
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[ge(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
2 0
0 1
· x2 +
2 0
0 1
· x3
[false] =
0 0
0 0
[s(x1)] =
0 0
2 0
+
1 0
0 1
· x1
[div(x1, x2)] =
0 0
0 0
+
1 4
0 1
· x1 +
0 0
0 0
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 1
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
0 0
+
1 4
0 1
· x1 +
0 0
0 0
· x2
[mark(x1)] =
0 0
0 0
+
2 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(z0,z1) → c12 (44)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
1 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
0 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 1
0 0
· x1 +
0 0
0 0
· x2
[c3] =
0 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 2
0 1
· x3
[ge(x1, x2)] =
2 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
2 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
4 0
0 4
· x2 +
4 4
0 4
· x3
[false] =
0 0
0 0
[s(x1)] =
0 0
2 0
+
1 0
0 0
· x1
[div(x1, x2)] =
0 0
0 0
+
1 4
0 0
· x1 +
0 0
0 1
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
0 0
+
1 4
0 0
· x1 +
0 0
0 4
· x2
[mark(x1)] =
0 0
0 0
+
4 0
0 4
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
0 0
1 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
1 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 1
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
0 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 1
0 0
· x1 +
0 0
0 0
· x2
[c3] =
0 0
1 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
1 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 1
· x2
[c7(x1, x2)] =
0 0
1 0
+
1 2
0 1
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
1 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 2
0 1
· x3
[ge(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
1 0
0 0
+
1 0
0 0
· x1 +
4 0
0 1
· x2 +
4 2
0 1
· x3
[false] =
0 0
0 0
[s(x1)] =
0 0
2 0
+
1 0
0 0
· x1
[div(x1, x2)] =
0 0
0 0
+
1 1
0 1
· x1 +
0 0
0 0
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
0 0
+
1 4
0 1
· x1 +
0 0
0 0
· x2
[mark(x1)] =
0 0
0 0
+
4 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
4 0
[mark#(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 2
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
4 0
+
0 4
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
4 0
[c10] =
0 0
1 0
[c13] =
4 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
4 0
0 0
+
0 4
0 0
· x1 +
1 2
0 0
· x2
[c3] =
0 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 0
0 1
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
4 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[ge(x1, x2)] =
0 0
0 0
+
0 4
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
0 0
+
0 4
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 0
0 1
· x3
[false] =
0 0
0 0
[s(x1)] =
4 0
4 0
+
1 0
0 1
· x1
[div(x1, x2)] =
4 0
0 0
+
1 4
0 1
· x1 +
1 2
0 0
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
4 0
0 0
+
1 4
0 1
· x1 +
1 2
0 0
· x2
[mark(x1)] =
0 0
0 0
+
1 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1
[c] =
0 0
0 0
[c1(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c12] =
0 0
0 0
[mark#(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c8(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c14(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[if_active#(x1, x2, x3)] =
0 0
0 0
+
0 1
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[c5(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c16(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c17(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c6(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[ge_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c2] =
0 0
0 0
[c9] =
0 0
0 0
[c10] =
0 0
0 0
[c13] =
0 0
0 0
[c11(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[div_active#(x1, x2)] =
0 0
0 0
+
0 2
0 0
· x1 +
0 0
0 0
· x2
[c3] =
0 0
0 0
[c4(x1)] =
0 0
0 0
+
1 0
0 0
· x1
[c18] =
0 0
0 0
[minus_active#(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[c7(x1, x2)] =
0 0
0 0
+
1 0
0 0
· x1 +
1 0
0 0
· x2
[c15] =
0 0
0 0
[true] =
0 0
0 0
[minus_active(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[if(x1, x2, x3)] =
1 0
0 0
+
1 1
0 0
· x1 +
1 0
0 1
· x2 +
1 2
0 1
· x3
[ge(x1, x2)] =
0 0
1 0
+
1 1
0 0
· x1 +
0 0
0 0
· x2
[ge_active(x1, x2)] =
0 0
1 0
+
1 1
0 0
· x1 +
0 0
0 0
· x2
[if_active(x1, x2, x3)] =
1 0
0 0
+
1 1
0 0
· x1 +
2 0
0 1
· x2 +
2 4
0 1
· x3
[false] =
0 0
1 0
[s(x1)] =
0 0
2 0
+
1 1
0 0
· x1
[div(x1, x2)] =
0 0
0 0
+
1 2
0 1
· x1 +
0 0
0 0
· x2
[0] =
0 0
0 0
[minus(x1, x2)] =
0 0
0 0
+
0 0
0 0
· x1 +
0 0
0 0
· x2
[div_active(x1, x2)] =
0 0
0 0
+
1 2
0 1
· x1 +
0 0
0 0
· x2
[mark(x1)] =
0 0
0 0
+
2 0
0 1
· x1
which has the intended complexity. Here, only the following usable rules have been considered:
minus_active#(0,z0) → c (21)
minus_active#(s(z0),s(z1)) → c1(minus_active#(z0,z1)) (23)
minus_active#(z0,z1) → c2 (25)
mark#(0) → c3 (26)
mark#(s(z0)) → c4(mark#(z0)) (28)
mark#(minus(z0,z1)) → c5(minus_active#(z0,z1)) (30)
mark#(ge(z0,z1)) → c6(ge_active#(z0,z1)) (32)
mark#(div(z0,z1)) → c7(div_active#(mark(z0),z1),mark#(z0)) (34)
mark#(if(z0,z1,z2)) → c8(if_active#(mark(z0),z1,z2),mark#(z0)) (36)
ge_active#(z0,0) → c9 (38)
ge_active#(0,s(z0)) → c10 (40)
ge_active#(s(z0),s(z1)) → c11(ge_active#(z0,z1)) (42)
ge_active#(z0,z1) → c12 (44)
div_active#(0,s(z0)) → c13 (46)
div_active#(s(z0),s(z1)) → c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) (48)
div_active#(z0,z1) → c15 (50)
if_active#(true,z0,z1) → c16(mark#(z0)) (52)
if_active#(false,z0,z1) → c17(mark#(z1)) (54)
if_active#(z0,z1,z2) → c18 (56)
if_active(false,z0,z1) → mark(z1) (53)
ge_active(s(z0),s(z1)) → ge_active(z0,z1) (41)
minus_active(z0,z1) → minus(z0,z1) (24)
ge_active(z0,0) → true (37)
mark(0) → 0 (2)
mark(if(z0,z1,z2)) → if_active(mark(z0),z1,z2) (35)
ge_active(0,s(z0)) → false (39)
minus_active(0,z0) → 0 (20)
mark(s(z0)) → s(mark(z0)) (27)
ge_active(z0,z1) → ge(z0,z1) (43)
div_active(0,s(z0)) → 0 (45)
div_active(s(z0),s(z1)) → if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) (47)
div_active(z0,z1) → div(z0,z1) (49)
mark(minus(z0,z1)) → minus_active(z0,z1) (29)
mark(ge(z0,z1)) → ge_active(z0,z1) (31)
mark(div(z0,z1)) → div_active(mark(z0),z1) (33)
if_active(z0,z1,z2) → if(z0,z1,z2) (55)
minus_active(s(z0),s(z1)) → minus_active(z0,z1) (22)
if_active(true,z0,z1) → mark(z0) (51)

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