Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex49_GM04_GM)

The rewrite relation of the following TRS is considered.

a__minus(0,Y)	→	0	(1)
a__minus(s(X),s(Y))	→	a__minus(X,Y)	(2)
a__geq(X,0)	→	true	(3)
a__geq(0,s(Y))	→	false	(4)
a__geq(s(X),s(Y))	→	a__geq(X,Y)	(5)
a__div(0,s(Y))	→	0	(6)
a__div(s(X),s(Y))	→	a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0)	(7)
a__if(true,X,Y)	→	mark(X)	(8)
a__if(false,X,Y)	→	mark(Y)	(9)
mark(minus(X1,X2))	→	a__minus(X1,X2)	(10)
mark(geq(X1,X2))	→	a__geq(X1,X2)	(11)
mark(div(X1,X2))	→	a__div(mark(X1),X2)	(12)
mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(13)
mark(0)	→	0	(14)
mark(s(X))	→	s(mark(X))	(15)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
a__minus(X1,X2)	→	minus(X1,X2)	(18)
a__geq(X1,X2)	→	geq(X1,X2)	(19)
a__div(X1,X2)	→	div(X1,X2)	(20)
a__if(X1,X2,X3)	→	if(X1,X2,X3)	(21)

The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n²).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:

a__minus^#(0,z0)

→

(23)

originates from

a__minus(0,z0)

→

(22)

a__minus^#(s(z0),s(z1))

→

c1(a__minus^#(z0,z1))

(25)

originates from

a__minus(s(z0),s(z1))

→

a__minus(z0,z1)

(24)

a__minus^#(z0,z1)

→

(27)

originates from

a__minus(z0,z1)

→

minus(z0,z1)

(26)

a__geq^#(z0,0)

→

(29)

originates from

a__geq(z0,0)

→

true

(28)

a__geq^#(0,s(z0))

→

(31)

originates from

a__geq(0,s(z0))

→

false

(30)

a__geq^#(s(z0),s(z1))

→

c5(a__geq^#(z0,z1))

(33)

originates from

a__geq(s(z0),s(z1))

→

a__geq(z0,z1)

(32)

a__geq^#(z0,z1)

→

(35)

originates from

a__geq(z0,z1)

→

geq(z0,z1)

(34)

a__div^#(0,s(z0))

→

(37)

originates from

a__div(0,s(z0))

→

(36)

a__div^#(s(z0),s(z1))

→

c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))

(39)

originates from

a__div(s(z0),s(z1))

→

a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)

(38)

a__div^#(z0,z1)

→

(41)

originates from

a__div(z0,z1)

→

div(z0,z1)

(40)

a__if^#(true,z0,z1)

→

c10(mark^#(z0))

(43)

originates from

a__if(true,z0,z1)

→

mark(z0)

(42)

a__if^#(false,z0,z1)

→

c11(mark^#(z1))

(45)

originates from

a__if(false,z0,z1)

→

mark(z1)

(44)

a__if^#(z0,z1,z2)

→

c12

(47)

originates from

a__if(z0,z1,z2)

→

if(z0,z1,z2)

(46)

mark^#(minus(z0,z1))

→

c13(a__minus^#(z0,z1))

(49)

originates from

mark(minus(z0,z1))

→

a__minus(z0,z1)

(48)

mark^#(geq(z0,z1))

→

c14(a__geq^#(z0,z1))

(51)

originates from

mark(geq(z0,z1))

→

a__geq(z0,z1)

(50)

mark^#(div(z0,z1))

→

c15(a__div^#(mark(z0),z1),mark^#(z0))

(53)

originates from

mark(div(z0,z1))

→

a__div(mark(z0),z1)

(52)

mark^#(if(z0,z1,z2))

→

c16(a__if^#(mark(z0),z1,z2),mark^#(z0))

(55)

originates from

mark(if(z0,z1,z2))

→

a__if(mark(z0),z1,z2)

(54)

mark^#(0)

→

c17

(56)

originates from

mark(0)

→

(14)

mark^#(s(z0))

→

c18(mark^#(z0))

(58)

originates from

mark(s(z0))

→

s(mark(z0))

(57)

mark^#(true)

→

c19

(59)

originates from

mark(true)

→

true

(16)

mark^#(false)

→

c20

(60)

originates from

mark(false)

→

false

(17)

Moreover, we add the following terms to the innermost strategy.

a__minus^#(0,z0)

a__minus^#(s(z0),s(z1))

a__minus^#(z0,z1)

a__geq^#(z0,0)

a__geq^#(0,s(z0))

a__geq^#(s(z0),s(z1))

a__geq^#(z0,z1)

a__div^#(0,s(z0))

a__div^#(s(z0),s(z1))

a__div^#(z0,z1)

a__if^#(true,z0,z1)

a__if^#(false,z0,z1)

a__if^#(z0,z1,z2)

mark^#(minus(z0,z1))

mark^#(geq(z0,z1))

mark^#(div(z0,z1))

mark^#(if(z0,z1,z2))

mark^#(0)

mark^#(s(z0))

mark^#(true)

mark^#(false)

1.1 Rule Shifting

The rules

a__div^#(0,s(z0))	→	c7	(37)
a__div^#(z0,z1)	→	c9	(41)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11(x₁)]	=	1 · x₁ + 0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[a__minus(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__geq(x₁, x₂)]	=	0
[a__div(x₁, x₂)]	=	1 + 1 · x₂
[a__if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[mark(x₁)]	=	1 + 1 · x₁
[a__minus^#(x₁, x₂)]	=	0
[a__geq^#(x₁, x₂)]	=	0
[a__div^#(x₁, x₂)]	=	1
[a__if^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃
[mark^#(x₁)]	=	1 · x₁ + 0
[minus(x₁, x₂)]	=	0
[geq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[div(x₁, x₂)]	=	1 + 1 · x₁
[if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[0]	=	0
[s(x₁)]	=	1 · x₁ + 0
[true]	=	0
[false]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)

1.1.1 Rule Shifting

The rules

mark^#(false)

→

c20

(60)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11(x₁)]	=	1 · x₁ + 0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[a__minus(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__geq(x₁, x₂)]	=	0
[a__div(x₁, x₂)]	=	1 + 1 · x₂
[a__if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[mark(x₁)]	=	1 + 1 · x₁
[a__minus^#(x₁, x₂)]	=	0
[a__geq^#(x₁, x₂)]	=	0
[a__div^#(x₁, x₂)]	=	0
[a__if^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃
[mark^#(x₁)]	=	1 · x₁ + 0
[minus(x₁, x₂)]	=	0
[geq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[div(x₁, x₂)]	=	1 · x₁ + 0
[if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[0]	=	0
[s(x₁)]	=	1 · x₁ + 0
[true]	=	0
[false]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)

1.1.1.1 Rule Shifting

The rules

mark^#(true)

→

c19

(59)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11(x₁)]	=	1 · x₁ + 0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[a__minus(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[a__geq(x₁, x₂)]	=	0
[a__div(x₁, x₂)]	=	3
[a__if(x₁, x₂, x₃)]	=	3 + 3 · x₁ + 3 · x₂ + 3 · x₃
[mark(x₁)]	=	3 · x₁ + 0
[a__minus^#(x₁, x₂)]	=	0
[a__geq^#(x₁, x₂)]	=	0
[a__div^#(x₁, x₂)]	=	0
[a__if^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃
[mark^#(x₁)]	=	1 · x₁ + 0
[minus(x₁, x₂)]	=	0
[geq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[div(x₁, x₂)]	=	1 · x₁ + 0
[if(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 1 · x₃
[0]	=	0
[s(x₁)]	=	1 · x₁ + 0
[true]	=	1
[false]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)

1.1.1.1.1 Rule Shifting

The rules

a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(0)	→	c17	(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

[a__geq^#(x₁, x₂)]

0	0
2	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
1	0

1	0
0	0

· x₁

[c12]

1	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

1	0
0	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
1	0

[c20]

1	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	1
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

1	0
0	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
1	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
1	0

[mark^#(x₁)]

1	0
0	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	4
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
2	0

[c4]

0	0
2	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

1	0
0	0

1	2
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[a__if(x₁, x₂, x₃)]

1	0
0	0

1	4
0	0

· x₁ +

2	0
0	1

· x₂ +

2	0
0	1

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
2	0

1	0
0	0

· x₁

[div(x₁, x₂)]

1	0
0	0

1	4
0	1

· x₁ +

0	0
0	0

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

1	0
0	0

1	4
0	1

· x₁ +

0	0
0	0

· x₂

[mark(x₁)]

0	0
0	0

2	0
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1 Rule Shifting

The rules

a__minus^#(0,z0)

→

(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

[a__geq^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

0	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	1
0	0

· x₂

[c17]

0	0
2	0

[a__if^#(x₁, x₂, x₃)]

0	0
0	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

0	0
2	0

[c2]

1	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
2	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
2	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	2
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
0	0

[c4]

0	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

2	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

4	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[a__if(x₁, x₂, x₃)]

4	0
0	0

1	0
0	0

· x₁ +

2	0
0	2

· x₂ +

2	0
0	2

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
2	0

1	0
0	0

· x₁

[div(x₁, x₂)]

0	0
4	0

1	4
0	0

· x₁ +

0	0
0	0

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
4	0

1	4
0	0

· x₁ +

0	0
0	0

· x₂

[mark(x₁)]

0	0
0	0

2	0
0	2

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1 Rule Shifting

The rules

a__minus^#(z0,z1)

→

(27)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

0	0
2	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

0	0
2	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

0	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
0	0

[c18(x₁)]

0	0
0	0

1	1
0	0

· x₁

[a__minus^#(x₁, x₂)]

2	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

2	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	1

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	2
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
0	0

[c4]

0	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

2	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[a__if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
2	0

1	1
0	0

· x₁

[div(x₁, x₂)]

0	0
0	0

1	2
0	0

· x₁ +

0	0
0	1

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

2	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
0	0

1	2
0	0

· x₁ +

0	0
0	1

· x₂

[mark(x₁)]

0	0
0	0

1	0
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__minus^#(s(z0),s(z1))

→

c1(a__minus^#(z0,z1))

(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

[a__geq^#(x₁, x₂)]

0	0
0	0

0	0
0	1

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

4	0
0	0

1	0
0	0

· x₁

[c12]

0	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
1	0

[a__if^#(x₁, x₂, x₃)]

0	0
0	0

0	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

0	0
1	0

[c2]

1	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
1	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

2	0
0	0

0	3
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

2	0
0	0

[mark^#(x₁)]

0	0
1	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

1	0
0	0

1	2
0	0

· x₁ +

1	1
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	4
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
0	0

[c4]

0	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	1

· x₁ +

1	1
0	0

· x₂

[a__minus(x₁, x₂)]

4	0
0	0

0	3
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	1
0	1

· x₃

[a__if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

2	0
0	1

· x₂ +

2	1
0	1

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
2	0

1	2
0	1

· x₁

[div(x₁, x₂)]

1	0
0	0

1	4
0	1

· x₁ +

0	0
0	0

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

2	0
0	0

0	3
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

1	0
0	0

1	4
0	1

· x₁ +

0	0
0	0

· x₂

[mark(x₁)]

0	0
0	0

2	0
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__if^#(true,z0,z1)

→

c10(mark^#(z0))

(43)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

1	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

1	0
0	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

0	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

1	0
0	0

1	0
0	0

· x₁

[c19]

0	0
0	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	1
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
0	0

[c4]

0	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

1	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	4
0	1

· x₃

[a__if(x₁, x₂, x₃)]

1	0
0	0

1	0
0	0

· x₁ +

4	0
0	4

· x₂ +

4	4
0	4

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
4	0

1	0
0	0

· x₁

[div(x₁, x₂)]

0	0
4	0

1	4
0	0

· x₁ +

0	0
0	1

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
4	0

1	4
0	0

· x₁ +

0	0
0	3

· x₂

[mark(x₁)]

0	0
0	0

4	0
0	4

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

mark^#(s(z0))

→

c18(mark^#(z0))

(58)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

0	0
2	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

0	0
2	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

2	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

2	0
0	0

[c18(x₁)]

1	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

2	0
0	0

1	1
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	2
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
0	0

[c4]

0	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

3	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

2	0
0	0

[geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

0	0
0	0

1	3
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[a__if(x₁, x₂, x₃)]

0	0
0	0

1	4
0	0

· x₁ +

3	0
0	1

· x₂ +

3	0
0	1

· x₃

[false]

2	0
0	0

[s(x₁)]

2	0
4	0

1	0
0	0

· x₁

[div(x₁, x₂)]

0	0
0	0

1	2
0	1

· x₁ +

0	0
0	0

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

2	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

2	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
0	0

1	3
0	1

· x₁ +

0	0
0	0

· x₂

[mark(x₁)]

2	0
0	0

3	0
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__if^#(false,z0,z1)

→

c11(mark^#(z1))

(45)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

1	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

1	0
0	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

0	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
0	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	1

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	2
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
0	0

[c4]

0	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	2
0	0

· x₂

[a__minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

2	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	2
0	1

· x₃

[a__if(x₁, x₂, x₃)]

4	0
0	0

1	0
0	0

· x₁ +

2	0
0	1

· x₂ +

2	2
0	1

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
2	0

1	0
0	0

· x₁

[div(x₁, x₂)]

0	0
2	0

1	4
0	0

· x₁ +

0	0
0	0

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

2	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
2	0

1	4
0	0

· x₁ +

0	0
0	0

· x₂

[mark(x₁)]

3	0
0	0

2	0
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__if^#(z0,z1,z2)

→

c12

(47)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

0	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

1	0
0	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

0	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
0	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

4	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	4
0	0

· x₁ +

0	2
0	0

· x₂

[c3]

0	0
0	0

[c4]

0	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

1	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[a__if(x₁, x₂, x₃)]

1	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
2	0

1	0
0	0

· x₁

[div(x₁, x₂)]

0	0
0	0

1	4
0	1

· x₁ +

0	4
0	1

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
0	0

1	4
0	1

· x₁ +

0	4
0	1

· x₂

[mark(x₁)]

0	0
0	0

1	0
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__geq^#(z0,z1)

→

(35)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

0	0
2	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

0	0
2	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

0	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
0	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

4	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	4
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

1	0
0	0

[c4]

1	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	1

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[a__if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

2	0
0	1

· x₂ +

2	0
0	1

· x₃

[false]

0	0
0	0

[s(x₁)]

3	0
2	0

1	0
0	0

· x₁

[div(x₁, x₂)]

0	0
0	0

1	4
0	0

· x₁ +

0	0
0	1

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
0	0

1	4
0	0

· x₁ +

0	0
0	1

· x₂

[mark(x₁)]

0	0
0	0

2	0
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__geq^#(z0,0)

→

(29)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

0	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

0	0
0	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
0	0

[c20]

0	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
0	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	1
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
0	0

[c4]

1	0
0	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[a__if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

2	0
0	1

· x₂ +

2	0
0	1

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
1	0

1	0
0	0

· x₁

[div(x₁, x₂)]

0	0
3	0

1	1
0	1

· x₁ +

0	0
0	0

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

1	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
3	0

1	1
0	1

· x₁ +

0	0
0	0

· x₂

[mark(x₁)]

0	0
0	0

2	0
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__geq^#(0,s(z0))

→

(31)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

1	0
2	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

0	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

0	0
0	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
2	0

[c20]

0	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
0	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	2
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

1	0
2	0

[c4]

0	0
2	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

3	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
4	0

[geq(x₁, x₂)]

2	0
4	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	1

· x₂ +

1	0
0	1

· x₃

[a__if(x₁, x₂, x₃)]

0	0
0	0

1	0
0	0

· x₁ +

2	0
0	2

· x₂ +

2	0
0	2

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
2	0

1	0
0	0

· x₁

[div(x₁, x₂)]

0	0
0	0

1	4
0	0

· x₁ +

0	0
0	1

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

3	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

2	0
4	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
0	0

1	4
0	0

· x₁ +

0	0
0	2

· x₂

[mark(x₁)]

0	0
0	0

2	0
0	2

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__geq^#(s(z0),s(z1))

→

c5(a__geq^#(z0,z1))

(33)

are strictly oriented by the following linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the rationals with delta = 1

[a__geq^#(x₁, x₂)]

0	0
4	0

0	4
0	0

· x₁ +

0	0
0	0

· x₂

[c1(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c12]

0	0
0	0

[c5(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c16(x₁, x₂)]

1	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c17]

0	0
0	0

[a__if^#(x₁, x₂, x₃)]

0	0
0	0

0	0
0	0

· x₁ +

1	0
0	0

· x₂ +

1	0
0	0

· x₃

[c6]

0	0
4	0

[c20]

0	0
0	0

[c2]

0	0
0	0

[c9]

0	0
0	0

[c13(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c11(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c19]

0	0
0	0

[c18(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__minus^#(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[c7]

0	0
0	0

[c]

0	0
0	0

[mark^#(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c8(x₁, x₂)]

0	0
0	0

1	0
0	0

· x₁ +

1	0
0	0

· x₂

[c14(x₁)]

0	0
0	0

1	0
0	0

· x₁

[c10(x₁)]

0	0
0	0

1	0
0	0

· x₁

[a__div^#(x₁, x₂)]

0	0
0	0

0	4
0	0

· x₁ +

0	0
0	0

· x₂

[c3]

0	0
4	0

[c4]

0	0
4	0

[c15(x₁, x₂)]

0	0
0	0

1	0
0	1

· x₁ +

1	0
0	0

· x₂

[a__minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[true]

0	0
0	0

[geq(x₁, x₂)]

0	0
0	0

0	4
0	0

· x₁ +

0	0
0	0

· x₂

[if(x₁, x₂, x₃)]

1	0
0	0

1	2
0	0

· x₁ +

1	0
0	1

· x₂ +

1	4
0	1

· x₃

[a__if(x₁, x₂, x₃)]

1	0
0	0

1	2
0	0

· x₁ +

2	1
0	1

· x₂ +

2	4
0	1

· x₃

[false]

0	0
0	0

[s(x₁)]

0	0
2	0

1	0
0	1

· x₁

[div(x₁, x₂)]

0	0
0	0

1	4
0	1

· x₁ +

0	0
0	0

· x₂

[0]

0	0
0	0

[minus(x₁, x₂)]

0	0
0	0

0	0
0	0

· x₁ +

0	0
0	0

· x₂

[a__geq(x₁, x₂)]

0	0
0	0

0	4
0	0

· x₁ +

0	0
0	0

· x₂

[a__div(x₁, x₂)]

0	0
0	0

1	4
0	1

· x₁ +

0	0
0	0

· x₂

[mark(x₁)]

0	0
0	0

2	1
0	1

· x₁

which has the intended complexity. Here, only the following usable rules have been considered:

a__minus^#(0,z0)	→	c	(23)
a__minus^#(s(z0),s(z1))	→	c1(a__minus^#(z0,z1))	(25)
a__minus^#(z0,z1)	→	c2	(27)
a__geq^#(z0,0)	→	c3	(29)
a__geq^#(0,s(z0))	→	c4	(31)
a__geq^#(s(z0),s(z1))	→	c5(a__geq^#(z0,z1))	(33)
a__geq^#(z0,z1)	→	c6	(35)
a__div^#(0,s(z0))	→	c7	(37)
a__div^#(s(z0),s(z1))	→	c8(a__if^#(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),a__geq^#(z0,z1))	(39)
a__div^#(z0,z1)	→	c9	(41)
a__if^#(true,z0,z1)	→	c10(mark^#(z0))	(43)
a__if^#(false,z0,z1)	→	c11(mark^#(z1))	(45)
a__if^#(z0,z1,z2)	→	c12	(47)
mark^#(minus(z0,z1))	→	c13(a__minus^#(z0,z1))	(49)
mark^#(geq(z0,z1))	→	c14(a__geq^#(z0,z1))	(51)
mark^#(div(z0,z1))	→	c15(a__div^#(mark(z0),z1),mark^#(z0))	(53)
mark^#(if(z0,z1,z2))	→	c16(a__if^#(mark(z0),z1,z2),mark^#(z0))	(55)
mark^#(0)	→	c17	(56)
mark^#(s(z0))	→	c18(mark^#(z0))	(58)
mark^#(true)	→	c19	(59)
mark^#(false)	→	c20	(60)
mark(geq(z0,z1))	→	a__geq(z0,z1)	(50)
a__geq(s(z0),s(z1))	→	a__geq(z0,z1)	(32)
mark(if(z0,z1,z2))	→	a__if(mark(z0),z1,z2)	(54)
mark(0)	→	0	(14)
a__if(false,z0,z1)	→	mark(z1)	(44)
a__div(z0,z1)	→	div(z0,z1)	(40)
a__if(z0,z1,z2)	→	if(z0,z1,z2)	(46)
a__if(true,z0,z1)	→	mark(z0)	(42)
a__geq(0,s(z0))	→	false	(30)
mark(true)	→	true	(16)
mark(false)	→	false	(17)
mark(s(z0))	→	s(mark(z0))	(57)
a__div(0,s(z0))	→	0	(36)
a__minus(s(z0),s(z1))	→	a__minus(z0,z1)	(24)
a__minus(z0,z1)	→	minus(z0,z1)	(26)
mark(minus(z0,z1))	→	a__minus(z0,z1)	(48)
a__minus(0,z0)	→	0	(22)
a__geq(z0,0)	→	true	(28)
mark(div(z0,z1))	→	a__div(mark(z0),z1)	(52)
a__geq(z0,z1)	→	geq(z0,z1)	(34)
a__div(s(z0),s(z1))	→	a__if(a__geq(z0,z1),s(div(minus(z0,z1),s(z1))),0)	(38)

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