Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Rubio_04/wst99)

The rewrite relation of the following TRS is considered.

din(der(plus(X,Y)))	→	u21(din(der(X)),X,Y)	(1)
u21(dout(DX),X,Y)	→	u22(din(der(Y)),X,Y,DX)	(2)
u22(dout(DY),X,Y,DX)	→	dout(plus(DX,DY))	(3)
din(der(times(X,Y)))	→	u31(din(der(X)),X,Y)	(4)
u31(dout(DX),X,Y)	→	u32(din(der(Y)),X,Y,DX)	(5)
u32(dout(DY),X,Y,DX)	→	dout(plus(times(X,DY),times(Y,DX)))	(6)
din(der(der(X)))	→	u41(din(der(X)),X)	(7)
u41(dout(DX),X)	→	u42(din(der(DX)),X,DX)	(8)
u42(dout(DDX),X,DX)	→	dout(DDX)	(9)

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:

din^#(der(plus(z0,z1)))

→

c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))

(11)

originates from

din(der(plus(z0,z1)))

→

u21(din(der(z0)),z0,z1)

(10)

din^#(der(times(z0,z1)))

→

c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))

(13)

originates from

din(der(times(z0,z1)))

→

u31(din(der(z0)),z0,z1)

(12)

din^#(der(der(z0)))

→

c2(u41^#(din(der(z0)),z0),din^#(der(z0)))

(15)

originates from

din(der(der(z0)))

→

u41(din(der(z0)),z0)

(14)

u21^#(dout(z0),z1,z2)

→

c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))

(17)

originates from

u21(dout(z0),z1,z2)

→

u22(din(der(z2)),z1,z2,z0)

(16)

u22^#(dout(z0),z1,z2,z3)

→

(19)

originates from

u22(dout(z0),z1,z2,z3)

→

dout(plus(z3,z0))

(18)

u31^#(dout(z0),z1,z2)

→

c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))

(21)

originates from

u31(dout(z0),z1,z2)

→

u32(din(der(z2)),z1,z2,z0)

(20)

u32^#(dout(z0),z1,z2,z3)

→

(23)

originates from

u32(dout(z0),z1,z2,z3)

→

dout(plus(times(z1,z0),times(z2,z3)))

(22)

u41^#(dout(z0),z1)

→

c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))

(25)

originates from

u41(dout(z0),z1)

→

u42(din(der(z0)),z1,z0)

(24)

u42^#(dout(z0),z1,z2)

→

(27)

originates from

u42(dout(z0),z1,z2)

→

dout(z0)

(26)

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

din^#(der(plus(z0,z1)))

din^#(der(times(z0,z1)))

din^#(der(der(z0)))

u21^#(dout(z0),z1,z2)

u22^#(dout(z0),z1,z2,z3)

u31^#(dout(z0),z1,z2)

u32^#(dout(z0),z1,z2,z3)

u41^#(dout(z0),z1)

u42^#(dout(z0),z1,z2)

1.1 Rule Shifting

The rules

u21^#(dout(z0),z1,z2)	→	c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(17)
u22^#(dout(z0),z1,z2,z3)	→	c4	(19)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[din(x₁)]	=	0
[u21(x₁, x₂, x₃)]	=	3 · x₁ + 0
[u22(x₁,...,x₄)]	=	1 + 3 · x₁ + 3 · x₄
[u31(x₁, x₂, x₃)]	=	1 · x₁ + 0
[u32(x₁,...,x₄)]	=	3 · x₁ + 0 + 1 · x₄
[u41(x₁, x₂)]	=	2 · x₁ + 0
[u42(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₃
[din^#(x₁)]	=	3 · x₁ + 0
[u21^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[u22^#(x₁,...,x₄)]	=	1 + 1 · x₄
[u31^#(x₁, x₂, x₃)]	=	0
[u32^#(x₁,...,x₄)]	=	0
[u41^#(x₁, x₂)]	=	0
[u42^#(x₁, x₂, x₃)]	=	0
[der(x₁)]	=	0
[plus(x₁, x₂)]	=	1 + 1 · x₂
[times(x₁, x₂)]	=	2
[dout(x₁)]	=	3 + 1 · x₁

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

din^#(der(plus(z0,z1)))	→	c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))	(11)
din^#(der(times(z0,z1)))	→	c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))	(13)
din^#(der(der(z0)))	→	c2(u41^#(din(der(z0)),z0),din^#(der(z0)))	(15)
u21^#(dout(z0),z1,z2)	→	c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(17)
u22^#(dout(z0),z1,z2,z3)	→	c4	(19)
u31^#(dout(z0),z1,z2)	→	c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(21)
u32^#(dout(z0),z1,z2,z3)	→	c6	(23)
u41^#(dout(z0),z1)	→	c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))	(25)
u42^#(dout(z0),z1,z2)	→	c8	(27)
u32(dout(z0),z1,z2,z3)	→	dout(plus(times(z1,z0),times(z2,z3)))	(22)
din(der(times(z0,z1)))	→	u31(din(der(z0)),z0,z1)	(12)
u22(dout(z0),z1,z2,z3)	→	dout(plus(z3,z0))	(18)
u31(dout(z0),z1,z2)	→	u32(din(der(z2)),z1,z2,z0)	(20)
u41(dout(z0),z1)	→	u42(din(der(z0)),z1,z0)	(24)
din(der(plus(z0,z1)))	→	u21(din(der(z0)),z0,z1)	(10)
u42(dout(z0),z1,z2)	→	dout(z0)	(26)
u21(dout(z0),z1,z2)	→	u22(din(der(z2)),z1,z2,z0)	(16)
din(der(der(z0)))	→	u41(din(der(z0)),z0)	(14)

1.1.1 Rule Shifting

The rules

u42^#(dout(z0),z1,z2)

→

(27)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[din(x₁)]	=	0
[u21(x₁, x₂, x₃)]	=	2 · x₁ + 0
[u22(x₁,...,x₄)]	=	2
[u31(x₁, x₂, x₃)]	=	2 · x₁ + 0
[u32(x₁,...,x₄)]	=	2 + 1 · x₁
[u41(x₁, x₂)]	=	1 · x₁ + 0
[u42(x₁, x₂, x₃)]	=	2
[din^#(x₁)]	=	3 · x₁ + 0
[u21^#(x₁, x₂, x₃)]	=	0
[u22^#(x₁,...,x₄)]	=	0
[u31^#(x₁, x₂, x₃)]	=	0
[u32^#(x₁,...,x₄)]	=	0
[u41^#(x₁, x₂)]	=	0
[u42^#(x₁, x₂, x₃)]	=	2 · x₁ + 0
[der(x₁)]	=	0
[plus(x₁, x₂)]	=	0
[times(x₁, x₂)]	=	0
[dout(x₁)]	=	2

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

din^#(der(plus(z0,z1)))	→	c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))	(11)
din^#(der(times(z0,z1)))	→	c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))	(13)
din^#(der(der(z0)))	→	c2(u41^#(din(der(z0)),z0),din^#(der(z0)))	(15)
u21^#(dout(z0),z1,z2)	→	c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(17)
u22^#(dout(z0),z1,z2,z3)	→	c4	(19)
u31^#(dout(z0),z1,z2)	→	c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(21)
u32^#(dout(z0),z1,z2,z3)	→	c6	(23)
u41^#(dout(z0),z1)	→	c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))	(25)
u42^#(dout(z0),z1,z2)	→	c8	(27)
u32(dout(z0),z1,z2,z3)	→	dout(plus(times(z1,z0),times(z2,z3)))	(22)
din(der(times(z0,z1)))	→	u31(din(der(z0)),z0,z1)	(12)
u22(dout(z0),z1,z2,z3)	→	dout(plus(z3,z0))	(18)
u31(dout(z0),z1,z2)	→	u32(din(der(z2)),z1,z2,z0)	(20)
u41(dout(z0),z1)	→	u42(din(der(z0)),z1,z0)	(24)
din(der(plus(z0,z1)))	→	u21(din(der(z0)),z0,z1)	(10)
u42(dout(z0),z1,z2)	→	dout(z0)	(26)
u21(dout(z0),z1,z2)	→	u22(din(der(z2)),z1,z2,z0)	(16)
din(der(der(z0)))	→	u41(din(der(z0)),z0)	(14)

1.1.1.1 Rule Shifting

The rules

u41^#(dout(z0),z1)

→

c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))

(25)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[din(x₁)]	=	0
[u21(x₁, x₂, x₃)]	=	0
[u22(x₁,...,x₄)]	=	1 · x₁ + 0
[u31(x₁, x₂, x₃)]	=	0
[u32(x₁,...,x₄)]	=	1 · x₁ + 0
[u41(x₁, x₂)]	=	0
[u42(x₁, x₂, x₃)]	=	1 · x₁ + 0
[din^#(x₁)]	=	1 · x₁ + 0
[u21^#(x₁, x₂, x₃)]	=	0
[u22^#(x₁,...,x₄)]	=	1 · x₁ + 0
[u31^#(x₁, x₂, x₃)]	=	0
[u32^#(x₁,...,x₄)]	=	0
[u41^#(x₁, x₂)]	=	1 · x₁ + 0
[u42^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[der(x₁)]	=	0
[plus(x₁, x₂)]	=	1
[times(x₁, x₂)]	=	0
[dout(x₁)]	=	1

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

din^#(der(plus(z0,z1)))	→	c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))	(11)
din^#(der(times(z0,z1)))	→	c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))	(13)
din^#(der(der(z0)))	→	c2(u41^#(din(der(z0)),z0),din^#(der(z0)))	(15)
u21^#(dout(z0),z1,z2)	→	c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(17)
u22^#(dout(z0),z1,z2,z3)	→	c4	(19)
u31^#(dout(z0),z1,z2)	→	c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(21)
u32^#(dout(z0),z1,z2,z3)	→	c6	(23)
u41^#(dout(z0),z1)	→	c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))	(25)
u42^#(dout(z0),z1,z2)	→	c8	(27)
u32(dout(z0),z1,z2,z3)	→	dout(plus(times(z1,z0),times(z2,z3)))	(22)
din(der(times(z0,z1)))	→	u31(din(der(z0)),z0,z1)	(12)
u22(dout(z0),z1,z2,z3)	→	dout(plus(z3,z0))	(18)
u31(dout(z0),z1,z2)	→	u32(din(der(z2)),z1,z2,z0)	(20)
u41(dout(z0),z1)	→	u42(din(der(z0)),z1,z0)	(24)
din(der(plus(z0,z1)))	→	u21(din(der(z0)),z0,z1)	(10)
u42(dout(z0),z1,z2)	→	dout(z0)	(26)
u21(dout(z0),z1,z2)	→	u22(din(der(z2)),z1,z2,z0)	(16)
din(der(der(z0)))	→	u41(din(der(z0)),z0)	(14)

1.1.1.1.1 Rule Shifting

The rules

u32^#(dout(z0),z1,z2,z3)

→

(23)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[din(x₁)]	=	0
[u21(x₁, x₂, x₃)]	=	1 · x₁ + 0
[u22(x₁,...,x₄)]	=	1
[u31(x₁, x₂, x₃)]	=	0
[u32(x₁,...,x₄)]	=	1 · x₁ + 0
[u41(x₁, x₂)]	=	0
[u42(x₁, x₂, x₃)]	=	1 · x₁ + 0
[din^#(x₁)]	=	1 · x₁ + 0
[u21^#(x₁, x₂, x₃)]	=	0
[u22^#(x₁,...,x₄)]	=	1 · x₁ + 0
[u31^#(x₁, x₂, x₃)]	=	0
[u32^#(x₁,...,x₄)]	=	1 · x₁ + 0
[u41^#(x₁, x₂)]	=	0
[u42^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[der(x₁)]	=	0
[plus(x₁, x₂)]	=	1
[times(x₁, x₂)]	=	0
[dout(x₁)]	=	1

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

din^#(der(plus(z0,z1)))	→	c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))	(11)
din^#(der(times(z0,z1)))	→	c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))	(13)
din^#(der(der(z0)))	→	c2(u41^#(din(der(z0)),z0),din^#(der(z0)))	(15)
u21^#(dout(z0),z1,z2)	→	c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(17)
u22^#(dout(z0),z1,z2,z3)	→	c4	(19)
u31^#(dout(z0),z1,z2)	→	c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(21)
u32^#(dout(z0),z1,z2,z3)	→	c6	(23)
u41^#(dout(z0),z1)	→	c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))	(25)
u42^#(dout(z0),z1,z2)	→	c8	(27)
u32(dout(z0),z1,z2,z3)	→	dout(plus(times(z1,z0),times(z2,z3)))	(22)
din(der(times(z0,z1)))	→	u31(din(der(z0)),z0,z1)	(12)
u22(dout(z0),z1,z2,z3)	→	dout(plus(z3,z0))	(18)
u31(dout(z0),z1,z2)	→	u32(din(der(z2)),z1,z2,z0)	(20)
u41(dout(z0),z1)	→	u42(din(der(z0)),z1,z0)	(24)
din(der(plus(z0,z1)))	→	u21(din(der(z0)),z0,z1)	(10)
u42(dout(z0),z1,z2)	→	dout(z0)	(26)
u21(dout(z0),z1,z2)	→	u22(din(der(z2)),z1,z2,z0)	(16)
din(der(der(z0)))	→	u41(din(der(z0)),z0)	(14)

1.1.1.1.1.1 Rule Shifting

The rules

u31^#(dout(z0),z1,z2)

→

c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))

(21)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[din(x₁)]	=	0
[u21(x₁, x₂, x₃)]	=	0
[u22(x₁,...,x₄)]	=	1 · x₁ + 0
[u31(x₁, x₂, x₃)]	=	0
[u32(x₁,...,x₄)]	=	1 · x₁ + 0
[u41(x₁, x₂)]	=	1 · x₁ + 0
[u42(x₁, x₂, x₃)]	=	1
[din^#(x₁)]	=	1 · x₁ + 0
[u21^#(x₁, x₂, x₃)]	=	0
[u22^#(x₁,...,x₄)]	=	1 · x₁ + 0
[u31^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[u32^#(x₁,...,x₄)]	=	1 · x₁ + 0
[u41^#(x₁, x₂)]	=	0
[u42^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[der(x₁)]	=	0
[plus(x₁, x₂)]	=	1
[times(x₁, x₂)]	=	0
[dout(x₁)]	=	1

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

din^#(der(plus(z0,z1)))	→	c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))	(11)
din^#(der(times(z0,z1)))	→	c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))	(13)
din^#(der(der(z0)))	→	c2(u41^#(din(der(z0)),z0),din^#(der(z0)))	(15)
u21^#(dout(z0),z1,z2)	→	c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(17)
u22^#(dout(z0),z1,z2,z3)	→	c4	(19)
u31^#(dout(z0),z1,z2)	→	c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(21)
u32^#(dout(z0),z1,z2,z3)	→	c6	(23)
u41^#(dout(z0),z1)	→	c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))	(25)
u42^#(dout(z0),z1,z2)	→	c8	(27)
u32(dout(z0),z1,z2,z3)	→	dout(plus(times(z1,z0),times(z2,z3)))	(22)
din(der(times(z0,z1)))	→	u31(din(der(z0)),z0,z1)	(12)
u22(dout(z0),z1,z2,z3)	→	dout(plus(z3,z0))	(18)
u31(dout(z0),z1,z2)	→	u32(din(der(z2)),z1,z2,z0)	(20)
u41(dout(z0),z1)	→	u42(din(der(z0)),z1,z0)	(24)
din(der(plus(z0,z1)))	→	u21(din(der(z0)),z0,z1)	(10)
u42(dout(z0),z1,z2)	→	dout(z0)	(26)
u21(dout(z0),z1,z2)	→	u22(din(der(z2)),z1,z2,z0)	(16)
din(der(der(z0)))	→	u41(din(der(z0)),z0)	(14)

1.1.1.1.1.1.1 Rule Shifting

The rules

din^#(der(plus(z0,z1)))	→	c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))	(11)
din^#(der(times(z0,z1)))	→	c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))	(13)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[din(x₁)]	=	0
[u21(x₁, x₂, x₃)]	=	1 · x₁ + 0
[u22(x₁,...,x₄)]	=	2 + 2 · x₁ · x₄ + 2 · x₁ · x₁
[u31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₁ · x₃ + 1 · x₁ · x₁ + 2 · x₂ · x₁
[u32(x₁,...,x₄)]	=	1 · x₂ + 0 + 2 · x₂ · x₄ + 2 · x₁ · x₁
[u41(x₁, x₂)]	=	0
[u42(x₁, x₂, x₃)]	=	2 · x₁ + 0
[din^#(x₁)]	=	1 · x₁ + 0
[u21^#(x₁, x₂, x₃)]	=	2 · x₁ · x₃ + 0
[u22^#(x₁,...,x₄)]	=	1 · x₃ · x₄ + 0
[u31^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[u32^#(x₁,...,x₄)]	=	0
[u41^#(x₁, x₂)]	=	1 · x₁ · x₁ + 0
[u42^#(x₁, x₂, x₃)]	=	2
[der(x₁)]	=	1 · x₁ + 0
[plus(x₁, x₂)]	=	2 + 1 · x₁
[times(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[dout(x₁)]	=	2 + 1 · x₁

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

din^#(der(plus(z0,z1)))	→	c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))	(11)
din^#(der(times(z0,z1)))	→	c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))	(13)
din^#(der(der(z0)))	→	c2(u41^#(din(der(z0)),z0),din^#(der(z0)))	(15)
u21^#(dout(z0),z1,z2)	→	c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(17)
u22^#(dout(z0),z1,z2,z3)	→	c4	(19)
u31^#(dout(z0),z1,z2)	→	c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(21)
u32^#(dout(z0),z1,z2,z3)	→	c6	(23)
u41^#(dout(z0),z1)	→	c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))	(25)
u42^#(dout(z0),z1,z2)	→	c8	(27)
u32(dout(z0),z1,z2,z3)	→	dout(plus(times(z1,z0),times(z2,z3)))	(22)
din(der(times(z0,z1)))	→	u31(din(der(z0)),z0,z1)	(12)
u22(dout(z0),z1,z2,z3)	→	dout(plus(z3,z0))	(18)
u31(dout(z0),z1,z2)	→	u32(din(der(z2)),z1,z2,z0)	(20)
u41(dout(z0),z1)	→	u42(din(der(z0)),z1,z0)	(24)
din(der(plus(z0,z1)))	→	u21(din(der(z0)),z0,z1)	(10)
u42(dout(z0),z1,z2)	→	dout(z0)	(26)
u21(dout(z0),z1,z2)	→	u22(din(der(z2)),z1,z2,z0)	(16)
din(der(der(z0)))	→	u41(din(der(z0)),z0)	(14)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

din^#(der(der(z0)))

→

c2(u41^#(din(der(z0)),z0),din^#(der(z0)))

(15)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[din(x₁)]	=	0
[u21(x₁, x₂, x₃)]	=	0
[u22(x₁,...,x₄)]	=	2 · x₁ + 0 + 2 · x₁ · x₄
[u31(x₁, x₂, x₃)]	=	2 · x₁ + 0 + 2 · x₁ · x₃ + 2 · x₁ · x₁ + 2 · x₂ · x₁
[u32(x₁,...,x₄)]	=	2 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 2 · x₄ + 2 · x₄ · x₄
[u41(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₁ · x₁
[u42(x₁, x₂, x₃)]	=	2 · x₁ + 0 + 2 · x₃
[din^#(x₁)]	=	2 · x₁ + 0 + 1 · x₁ · x₁
[u21^#(x₁, x₂, x₃)]	=	2 · x₁ + 0 + 2 · x₃ + 1 · x₃ · x₃ + 2 · x₁ · x₃ + 1 · x₁ · x₁
[u22^#(x₁,...,x₄)]	=	1 · x₃ · x₄ + 0
[u31^#(x₁, x₂, x₃)]	=	2 · x₃ + 0 + 1 · x₃ · x₃ + 2 · x₁ · x₃ + 2 · x₁ · x₁
[u32^#(x₁,...,x₄)]	=	2 · x₄ + 0 + 1 · x₃ · x₄
[u41^#(x₁, x₂)]	=	2 · x₂ + 0 + 2 · x₁ · x₁
[u42^#(x₁, x₂, x₃)]	=	2 · x₂ + 0 + 1 · x₃ · x₃
[der(x₁)]	=	2 + 1 · x₁
[plus(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[times(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[dout(x₁)]	=	2 + 1 · x₁

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

din^#(der(plus(z0,z1)))	→	c(u21^#(din(der(z0)),z0,z1),din^#(der(z0)))	(11)
din^#(der(times(z0,z1)))	→	c1(u31^#(din(der(z0)),z0,z1),din^#(der(z0)))	(13)
din^#(der(der(z0)))	→	c2(u41^#(din(der(z0)),z0),din^#(der(z0)))	(15)
u21^#(dout(z0),z1,z2)	→	c3(u22^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(17)
u22^#(dout(z0),z1,z2,z3)	→	c4	(19)
u31^#(dout(z0),z1,z2)	→	c5(u32^#(din(der(z2)),z1,z2,z0),din^#(der(z2)))	(21)
u32^#(dout(z0),z1,z2,z3)	→	c6	(23)
u41^#(dout(z0),z1)	→	c7(u42^#(din(der(z0)),z1,z0),din^#(der(z0)))	(25)
u42^#(dout(z0),z1,z2)	→	c8	(27)
u32(dout(z0),z1,z2,z3)	→	dout(plus(times(z1,z0),times(z2,z3)))	(22)
din(der(times(z0,z1)))	→	u31(din(der(z0)),z0,z1)	(12)
u22(dout(z0),z1,z2,z3)	→	dout(plus(z3,z0))	(18)
u31(dout(z0),z1,z2)	→	u32(din(der(z2)),z1,z2,z0)	(20)
u41(dout(z0),z1)	→	u42(din(der(z0)),z1,z0)	(24)
din(der(plus(z0,z1)))	→	u21(din(der(z0)),z0,z1)	(10)
u42(dout(z0),z1,z2)	→	dout(z0)	(26)
u21(dout(z0),z1,z2)	→	u22(din(der(z2)),z1,z2,z0)	(16)
din(der(der(z0)))	→	u41(din(der(z0)),z0)	(14)

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