Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/raML/dyade.raml)

The relative rewrite relation R/S is considered where R is the following TRS

*(@x,@y)	→	#mult(@x,@y)	(1)
dyade(@l1,@l2)	→	dyade#1(@l1,@l2)	(2)
dyade#1(::(@x,@xs),@l2)	→	::(mult(@x,@l2),dyade(@xs,@l2))	(3)
dyade#1(nil,@l2)	→	nil	(4)
mult(@n,@l)	→	mult#1(@l,@n)	(5)
mult#1(::(@x,@xs),@n)	→	::(*(@n,@x),mult(@n,@xs))	(6)
mult#1(nil,@n)	→	nil	(7)

and S is the following TRS.

#add(#0,@y)	→	@y	(8)
#add(#neg(#s(#0)),@y)	→	#pred(@y)	(9)
#add(#neg(#s(#s(@x))),@y)	→	#pred(#add(#pos(#s(@x)),@y))	(10)
#add(#pos(#s(#0)),@y)	→	#succ(@y)	(11)
#add(#pos(#s(#s(@x))),@y)	→	#succ(#add(#pos(#s(@x)),@y))	(12)
#mult(#0,#0)	→	#0	(13)
#mult(#0,#neg(@y))	→	#0	(14)
#mult(#0,#pos(@y))	→	#0	(15)
#mult(#neg(@x),#0)	→	#0	(16)
#mult(#neg(@x),#neg(@y))	→	#pos(#natmult(@x,@y))	(17)
#mult(#neg(@x),#pos(@y))	→	#neg(#natmult(@x,@y))	(18)
#mult(#pos(@x),#0)	→	#0	(19)
#mult(#pos(@x),#neg(@y))	→	#neg(#natmult(@x,@y))	(20)
#mult(#pos(@x),#pos(@y))	→	#pos(#natmult(@x,@y))	(21)
#natmult(#0,@y)	→	#0	(22)
#natmult(#s(@x),@y)	→	#add(#pos(@y),#natmult(@x,@y))	(23)
#pred(#0)	→	#neg(#s(#0))	(24)
#pred(#neg(#s(@x)))	→	#neg(#s(#s(@x)))	(25)
#pred(#pos(#s(#0)))	→	#0	(26)
#pred(#pos(#s(#s(@x))))	→	#pos(#s(@x))	(27)
#succ(#0)	→	#pos(#s(#0))	(28)
#succ(#neg(#s(#0)))	→	#0	(29)
#succ(#neg(#s(#s(@x))))	→	#neg(#s(@x))	(30)
#succ(#pos(#s(@x)))	→	#pos(#s(#s(@x)))	(31)

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:

*^#(z0,z1)

→

c24(#mult^#(z0,z1))

(33)

originates from

*(z0,z1)

→

#mult(z0,z1)

(32)

dyade^#(z0,z1)

→

c25(dyade#1^#(z0,z1))

(35)

originates from

dyade(z0,z1)

→

dyade#1(z0,z1)

(34)

dyade#1^#(::(z0,z1),z2)

→

c26(mult^#(z0,z2),dyade^#(z1,z2))

(37)

originates from

dyade#1(::(z0,z1),z2)

→

::(mult(z0,z2),dyade(z1,z2))

(36)

dyade#1^#(nil,z0)

→

c27

(39)

originates from

dyade#1(nil,z0)

→

nil

(38)

mult^#(z0,z1)

→

c28(mult#1^#(z1,z0))

(41)

originates from

mult(z0,z1)

→

mult#1(z1,z0)

(40)

mult#1^#(::(z0,z1),z2)

→

c29(*^#(z2,z0),mult^#(z2,z1))

(43)

originates from

mult#1(::(z0,z1),z2)

→

::(*(z2,z0),mult(z2,z1))

(42)

mult#1^#(nil,z0)

→

c30

(45)

originates from

mult#1(nil,z0)

→

nil

(44)

#add^#(#0,z0)

→

(47)

originates from

#add(#0,z0)

→

(46)

#add^#(#neg(#s(#0)),z0)

→

c1(#pred^#(z0))

(49)

originates from

#add(#neg(#s(#0)),z0)

→

#pred(z0)

(48)

#add^#(#neg(#s(#s(z0))),z1)

→

c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))

(51)

originates from

#add(#neg(#s(#s(z0))),z1)

→

#pred(#add(#pos(#s(z0)),z1))

(50)

#add^#(#pos(#s(#0)),z0)

→

c3(#succ^#(z0))

(53)

originates from

#add(#pos(#s(#0)),z0)

→

#succ(z0)

(52)

#add^#(#pos(#s(#s(z0))),z1)

→

c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))

(55)

originates from

#add(#pos(#s(#s(z0))),z1)

→

#succ(#add(#pos(#s(z0)),z1))

(54)

#mult^#(#0,#0)

→

(56)

originates from

#mult(#0,#0)

→

(13)

#mult^#(#0,#neg(z0))

→

(58)

originates from

#mult(#0,#neg(z0))

→

(57)

#mult^#(#0,#pos(z0))

→

(60)

originates from

#mult(#0,#pos(z0))

→

(59)

#mult^#(#neg(z0),#0)

→

(62)

originates from

#mult(#neg(z0),#0)

→

(61)

#mult^#(#neg(z0),#neg(z1))

→

c9(#natmult^#(z0,z1))

(64)

originates from

#mult(#neg(z0),#neg(z1))

→

#pos(#natmult(z0,z1))

(63)

#mult^#(#neg(z0),#pos(z1))

→

c10(#natmult^#(z0,z1))

(66)

originates from

#mult(#neg(z0),#pos(z1))

→

#neg(#natmult(z0,z1))

(65)

#mult^#(#pos(z0),#0)

→

c11

(68)

originates from

#mult(#pos(z0),#0)

→

(67)

#mult^#(#pos(z0),#neg(z1))

→

c12(#natmult^#(z0,z1))

(70)

originates from

#mult(#pos(z0),#neg(z1))

→

#neg(#natmult(z0,z1))

(69)

#mult^#(#pos(z0),#pos(z1))

→

c13(#natmult^#(z0,z1))

(72)

originates from

#mult(#pos(z0),#pos(z1))

→

#pos(#natmult(z0,z1))

(71)

#natmult^#(#0,z0)

→

c14

(74)

originates from

#natmult(#0,z0)

→

(73)

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

→

c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))

(76)

originates from

#natmult(#s(z0),z1)

→

#add(#pos(z1),#natmult(z0,z1))

(75)

#pred^#(#0)

→

c16

(77)

originates from

#pred(#0)

→

#neg(#s(#0))

(24)

#pred^#(#neg(#s(z0)))

→

c17

(79)

originates from

#pred(#neg(#s(z0)))

→

#neg(#s(#s(z0)))

(78)

#pred^#(#pos(#s(#0)))

→

c18

(80)

originates from

#pred(#pos(#s(#0)))

→

(26)

#pred^#(#pos(#s(#s(z0))))

→

c19

(82)

originates from

#pred(#pos(#s(#s(z0))))

→

#pos(#s(z0))

(81)

#succ^#(#0)

→

c20

(83)

originates from

#succ(#0)

→

#pos(#s(#0))

(28)

#succ^#(#neg(#s(#0)))

→

c21

(84)

originates from

#succ(#neg(#s(#0)))

→

(29)

#succ^#(#neg(#s(#s(z0))))

→

c22

(86)

originates from

#succ(#neg(#s(#s(z0))))

→

#neg(#s(z0))

(85)

#succ^#(#pos(#s(z0)))

→

c23

(88)

originates from

#succ(#pos(#s(z0)))

→

#pos(#s(#s(z0)))

(87)

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

#add^#(#0,z0)

#add^#(#neg(#s(#0)),z0)

#add^#(#neg(#s(#s(z0))),z1)

#add^#(#pos(#s(#0)),z0)

#add^#(#pos(#s(#s(z0))),z1)

#mult^#(#0,#0)

#mult^#(#0,#neg(z0))

#mult^#(#0,#pos(z0))

#mult^#(#neg(z0),#0)

#mult^#(#neg(z0),#neg(z1))

#mult^#(#neg(z0),#pos(z1))

#mult^#(#pos(z0),#0)

#mult^#(#pos(z0),#neg(z1))

#mult^#(#pos(z0),#pos(z1))

#natmult^#(#0,z0)

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

#pred^#(#0)

#pred^#(#neg(#s(z0)))

#pred^#(#pos(#s(#0)))

#pred^#(#pos(#s(#s(z0))))

#succ^#(#0)

#succ^#(#neg(#s(#0)))

#succ^#(#neg(#s(#s(z0))))

#succ^#(#pos(#s(z0)))

*^#(z0,z1)

dyade^#(z0,z1)

dyade#1^#(::(z0,z1),z2)

dyade#1^#(nil,z0)

mult^#(z0,z1)

mult#1^#(::(z0,z1),z2)

mult#1^#(nil,z0)

1.1 Usable Rules

We remove the following rules since they are not usable.

#add(#0,z0)	→	z0	(46)
#add(#neg(#s(#0)),z0)	→	#pred(z0)	(48)
#add(#neg(#s(#s(z0))),z1)	→	#pred(#add(#pos(#s(z0)),z1))	(50)
#mult(#0,#0)	→	#0	(13)
#mult(#0,#neg(z0))	→	#0	(57)
#mult(#0,#pos(z0))	→	#0	(59)
#mult(#neg(z0),#0)	→	#0	(61)
#mult(#neg(z0),#neg(z1))	→	#pos(#natmult(z0,z1))	(63)
#mult(#neg(z0),#pos(z1))	→	#neg(#natmult(z0,z1))	(65)
#mult(#pos(z0),#0)	→	#0	(67)
#mult(#pos(z0),#neg(z1))	→	#neg(#natmult(z0,z1))	(69)
#mult(#pos(z0),#pos(z1))	→	#pos(#natmult(z0,z1))	(71)
#pred(#0)	→	#neg(#s(#0))	(24)
#pred(#neg(#s(z0)))	→	#neg(#s(#s(z0)))	(78)
#pred(#pos(#s(#0)))	→	#0	(26)
#pred(#pos(#s(#s(z0))))	→	#pos(#s(z0))	(81)
*(z0,z1)	→	#mult(z0,z1)	(32)
dyade(z0,z1)	→	dyade#1(z0,z1)	(34)
dyade#1(::(z0,z1),z2)	→	::(mult(z0,z2),dyade(z1,z2))	(36)
dyade#1(nil,z0)	→	nil	(38)
mult(z0,z1)	→	mult#1(z1,z0)	(40)
mult#1(::(z0,z1),z2)	→	::(*(z2,z0),mult(z2,z1))	(42)
mult#1(nil,z0)	→	nil	(44)

1.1.1 Rule Shifting

The rules

dyade#1^#(nil,z0)	→	c27	(39)
mult#1^#(nil,z0)	→	c30	(45)

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

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25(x₁)]	=	1 · x₁ + 0
[c26(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[dyade^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[dyade#1^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[mult^#(x₁, x₂)]	=	1 + 1 · x₁
[mult#1^#(x₁, x₂)]	=	1 + 1 · x₂
[#0]	=	0
[#s(x₁)]	=	0
[#pos(x₁)]	=	0
[#neg(x₁)]	=	1
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0

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

#add^#(#0,z0)	→	c	(47)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(49)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(51)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(53)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(55)
#mult^#(#0,#0)	→	c5	(56)
#mult^#(#0,#neg(z0))	→	c6	(58)
#mult^#(#0,#pos(z0))	→	c7	(60)
#mult^#(#neg(z0),#0)	→	c8	(62)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(64)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(66)
#mult^#(#pos(z0),#0)	→	c11	(68)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(70)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(72)
#natmult^#(#0,z0)	→	c14	(74)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(76)
#pred^#(#0)	→	c16	(77)
#pred^#(#neg(#s(z0)))	→	c17	(79)
#pred^#(#pos(#s(#0)))	→	c18	(80)
#pred^#(#pos(#s(#s(z0))))	→	c19	(82)
#succ^#(#0)	→	c20	(83)
#succ^#(#neg(#s(#0)))	→	c21	(84)
#succ^#(#neg(#s(#s(z0))))	→	c22	(86)
#succ^#(#pos(#s(z0)))	→	c23	(88)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(33)
dyade^#(z0,z1)	→	c25(dyade#1^#(z0,z1))	(35)
dyade#1^#(::(z0,z1),z2)	→	c26(mult^#(z0,z2),dyade^#(z1,z2))	(37)
dyade#1^#(nil,z0)	→	c27	(39)
mult^#(z0,z1)	→	c28(mult#1^#(z1,z0))	(41)
mult#1^#(::(z0,z1),z2)	→	c29(*^#(z2,z0),mult^#(z2,z1))	(43)
mult#1^#(nil,z0)	→	c30	(45)

1.1.1.1 Rule Shifting

The rules

dyade#1^#(::(z0,z1),z2)

→

c26(mult^#(z0,z2),dyade^#(z1,z2))

(37)

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

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25(x₁)]	=	1 · x₁ + 0
[c26(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[dyade^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[dyade#1^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[mult^#(x₁, x₂)]	=	1 · x₁ + 0
[mult#1^#(x₁, x₂)]	=	1 · x₂ + 0
[#0]	=	0
[#s(x₁)]	=	0
[#pos(x₁)]	=	0
[#neg(x₁)]	=	1
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0

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

#add^#(#0,z0)	→	c	(47)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(49)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(51)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(53)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(55)
#mult^#(#0,#0)	→	c5	(56)
#mult^#(#0,#neg(z0))	→	c6	(58)
#mult^#(#0,#pos(z0))	→	c7	(60)
#mult^#(#neg(z0),#0)	→	c8	(62)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(64)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(66)
#mult^#(#pos(z0),#0)	→	c11	(68)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(70)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(72)
#natmult^#(#0,z0)	→	c14	(74)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(76)
#pred^#(#0)	→	c16	(77)
#pred^#(#neg(#s(z0)))	→	c17	(79)
#pred^#(#pos(#s(#0)))	→	c18	(80)
#pred^#(#pos(#s(#s(z0))))	→	c19	(82)
#succ^#(#0)	→	c20	(83)
#succ^#(#neg(#s(#0)))	→	c21	(84)
#succ^#(#neg(#s(#s(z0))))	→	c22	(86)
#succ^#(#pos(#s(z0)))	→	c23	(88)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(33)
dyade^#(z0,z1)	→	c25(dyade#1^#(z0,z1))	(35)
dyade#1^#(::(z0,z1),z2)	→	c26(mult^#(z0,z2),dyade^#(z1,z2))	(37)
dyade#1^#(nil,z0)	→	c27	(39)
mult^#(z0,z1)	→	c28(mult#1^#(z1,z0))	(41)
mult#1^#(::(z0,z1),z2)	→	c29(*^#(z2,z0),mult^#(z2,z1))	(43)
mult#1^#(nil,z0)	→	c30	(45)

1.1.1.1.1 Rule Shifting

The rules

dyade^#(z0,z1)

→

c25(dyade#1^#(z0,z1))

(35)

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

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25(x₁)]	=	1 · x₁ + 0
[c26(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#add^#(x₁, x₂)]	=	1 · x₁ + 0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[dyade^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[dyade#1^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[mult^#(x₁, x₂)]	=	1 · x₁ + 0
[mult#1^#(x₁, x₂)]	=	1 · x₂ + 0
[#0]	=	0
[#s(x₁)]	=	0
[#pos(x₁)]	=	0
[#neg(x₁)]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0

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

#add^#(#0,z0)	→	c	(47)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(49)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(51)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(53)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(55)
#mult^#(#0,#0)	→	c5	(56)
#mult^#(#0,#neg(z0))	→	c6	(58)
#mult^#(#0,#pos(z0))	→	c7	(60)
#mult^#(#neg(z0),#0)	→	c8	(62)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(64)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(66)
#mult^#(#pos(z0),#0)	→	c11	(68)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(70)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(72)
#natmult^#(#0,z0)	→	c14	(74)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(76)
#pred^#(#0)	→	c16	(77)
#pred^#(#neg(#s(z0)))	→	c17	(79)
#pred^#(#pos(#s(#0)))	→	c18	(80)
#pred^#(#pos(#s(#s(z0))))	→	c19	(82)
#succ^#(#0)	→	c20	(83)
#succ^#(#neg(#s(#0)))	→	c21	(84)
#succ^#(#neg(#s(#s(z0))))	→	c22	(86)
#succ^#(#pos(#s(z0)))	→	c23	(88)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(33)
dyade^#(z0,z1)	→	c25(dyade#1^#(z0,z1))	(35)
dyade#1^#(::(z0,z1),z2)	→	c26(mult^#(z0,z2),dyade^#(z1,z2))	(37)
dyade#1^#(nil,z0)	→	c27	(39)
mult^#(z0,z1)	→	c28(mult#1^#(z1,z0))	(41)
mult#1^#(::(z0,z1),z2)	→	c29(*^#(z2,z0),mult^#(z2,z1))	(43)
mult#1^#(nil,z0)	→	c30	(45)

1.1.1.1.1.1 Rule Shifting

The rules

*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(33)
mult#1^#(::(z0,z1),z2)	→	c29(*^#(z2,z0),mult^#(z2,z1))	(43)

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

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25(x₁)]	=	1 · x₁ + 0
[c26(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#add(x₁, x₂)]	=	1 · x₁ · x₁ + 0
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	2 + 2 · x₁ · x₁
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	1 · x₂ + 0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	1 + 2 · x₂ + 1 · x₁ · x₂
[dyade^#(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[dyade#1^#(x₁, x₂)]	=	2 · x₂ · x₂ + 0 + 2 · x₁ · x₂ + 2 · x₁ · x₁
[mult^#(x₁, x₂)]	=	2 · x₁ + 0 + 2 · x₂ + 2 · x₁ · x₂ + 1 · x₁ · x₁
[mult#1^#(x₁, x₂)]	=	2 · x₁ + 0 + 1 · x₂ · x₂ + 2 · x₁ · x₂
[#0]	=	0
[#s(x₁)]	=	2
[#pos(x₁)]	=	2
[#neg(x₁)]	=	0
[::(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[nil]	=	0

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

#add^#(#0,z0)	→	c	(47)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(49)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(51)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(53)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(55)
#mult^#(#0,#0)	→	c5	(56)
#mult^#(#0,#neg(z0))	→	c6	(58)
#mult^#(#0,#pos(z0))	→	c7	(60)
#mult^#(#neg(z0),#0)	→	c8	(62)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(64)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(66)
#mult^#(#pos(z0),#0)	→	c11	(68)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(70)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(72)
#natmult^#(#0,z0)	→	c14	(74)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(76)
#pred^#(#0)	→	c16	(77)
#pred^#(#neg(#s(z0)))	→	c17	(79)
#pred^#(#pos(#s(#0)))	→	c18	(80)
#pred^#(#pos(#s(#s(z0))))	→	c19	(82)
#succ^#(#0)	→	c20	(83)
#succ^#(#neg(#s(#0)))	→	c21	(84)
#succ^#(#neg(#s(#s(z0))))	→	c22	(86)
#succ^#(#pos(#s(z0)))	→	c23	(88)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(33)
dyade^#(z0,z1)	→	c25(dyade#1^#(z0,z1))	(35)
dyade#1^#(::(z0,z1),z2)	→	c26(mult^#(z0,z2),dyade^#(z1,z2))	(37)
dyade#1^#(nil,z0)	→	c27	(39)
mult^#(z0,z1)	→	c28(mult#1^#(z1,z0))	(41)
mult#1^#(::(z0,z1),z2)	→	c29(*^#(z2,z0),mult^#(z2,z1))	(43)
mult#1^#(nil,z0)	→	c30	(45)

1.1.1.1.1.1.1 Rule Shifting

The rules

mult^#(z0,z1)

→

c28(mult#1^#(z1,z0))

(41)

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

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25(x₁)]	=	1 · x₁ + 0
[c26(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#add(x₁, x₂)]	=	1 · x₁ · x₁ + 0
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	2 + 1 · x₁ · x₂ + 2 · x₁ · x₁
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	1
[#natmult^#(x₁, x₂)]	=	1
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	1
[dyade^#(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₂ · x₂ + 2 · x₁ · x₂
[dyade#1^#(x₁, x₂)]	=	2 · x₁ + 0 + 1 · x₂ + 2 · x₂ · x₂ + 2 · x₁ · x₂
[mult^#(x₁, x₂)]	=	1 + 2 · x₂
[mult#1^#(x₁, x₂)]	=	2 · x₁ + 0
[#0]	=	1
[#s(x₁)]	=	2
[#pos(x₁)]	=	2
[#neg(x₁)]	=	0
[::(x₁, x₂)]	=	2 + 1 · x₂
[nil]	=	0

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

#add^#(#0,z0)	→	c	(47)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(49)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(51)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(53)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(55)
#mult^#(#0,#0)	→	c5	(56)
#mult^#(#0,#neg(z0))	→	c6	(58)
#mult^#(#0,#pos(z0))	→	c7	(60)
#mult^#(#neg(z0),#0)	→	c8	(62)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(64)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(66)
#mult^#(#pos(z0),#0)	→	c11	(68)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(70)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(72)
#natmult^#(#0,z0)	→	c14	(74)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(76)
#pred^#(#0)	→	c16	(77)
#pred^#(#neg(#s(z0)))	→	c17	(79)
#pred^#(#pos(#s(#0)))	→	c18	(80)
#pred^#(#pos(#s(#s(z0))))	→	c19	(82)
#succ^#(#0)	→	c20	(83)
#succ^#(#neg(#s(#0)))	→	c21	(84)
#succ^#(#neg(#s(#s(z0))))	→	c22	(86)
#succ^#(#pos(#s(z0)))	→	c23	(88)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(33)
dyade^#(z0,z1)	→	c25(dyade#1^#(z0,z1))	(35)
dyade#1^#(::(z0,z1),z2)	→	c26(mult^#(z0,z2),dyade^#(z1,z2))	(37)
dyade#1^#(nil,z0)	→	c27	(39)
mult^#(z0,z1)	→	c28(mult#1^#(z1,z0))	(41)
mult#1^#(::(z0,z1),z2)	→	c29(*^#(z2,z0),mult^#(z2,z1))	(43)
mult#1^#(nil,z0)	→	c30	(45)

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