Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/raML/clevermmult.raml)

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

*(@x,@y)	→	#mult(@x,@y)	(1)
+(@x,@y)	→	#add(@x,@y)	(2)
computeLine(@line,@m,@acc)	→	computeLine#1(@line,@acc,@m)	(3)
computeLine#1(::(@x,@xs),@acc,@m)	→	computeLine#2(@m,@acc,@x,@xs)	(4)
computeLine#1(nil,@acc,@m)	→	@acc	(5)
computeLine#2(::(@l,@ls),@acc,@x,@xs)	→	computeLine(@xs,@ls,lineMult(@x,@l,@acc))	(6)
computeLine#2(nil,@acc,@x,@xs)	→	nil	(7)
lineMult(@n,@l1,@l2)	→	lineMult#1(@l1,@l2,@n)	(8)
lineMult#1(::(@x,@xs),@l2,@n)	→	lineMult#2(@l2,@n,@x,@xs)	(9)
lineMult#1(nil,@l2,@n)	→	nil	(10)
lineMult#2(::(@y,@ys),@n,@x,@xs)	→	::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys))	(11)
lineMult#2(nil,@n,@x,@xs)	→	::(*(@x,@n),lineMult(@n,@xs,nil))	(12)
matrixMult(@m1,@m2)	→	matrixMult#1(@m1,@m2)	(13)
matrixMult#1(::(@l,@ls),@m2)	→	::(computeLine(@l,@m2,nil),matrixMult(@ls,@m2))	(14)
matrixMult#1(nil,@m2)	→	nil	(15)

and S is the following TRS.

#add(#0,@y)	→	@y	(16)
#add(#neg(#s(#0)),@y)	→	#pred(@y)	(17)
#add(#neg(#s(#s(@x))),@y)	→	#pred(#add(#pos(#s(@x)),@y))	(18)
#add(#pos(#s(#0)),@y)	→	#succ(@y)	(19)
#add(#pos(#s(#s(@x))),@y)	→	#succ(#add(#pos(#s(@x)),@y))	(20)
#mult(#0,#0)	→	#0	(21)
#mult(#0,#neg(@y))	→	#0	(22)
#mult(#0,#pos(@y))	→	#0	(23)
#mult(#neg(@x),#0)	→	#0	(24)
#mult(#neg(@x),#neg(@y))	→	#pos(#natmult(@x,@y))	(25)
#mult(#neg(@x),#pos(@y))	→	#neg(#natmult(@x,@y))	(26)
#mult(#pos(@x),#0)	→	#0	(27)
#mult(#pos(@x),#neg(@y))	→	#neg(#natmult(@x,@y))	(28)
#mult(#pos(@x),#pos(@y))	→	#pos(#natmult(@x,@y))	(29)
#natmult(#0,@y)	→	#0	(30)
#natmult(#s(@x),@y)	→	#add(#pos(@y),#natmult(@x,@y))	(31)
#pred(#0)	→	#neg(#s(#0))	(32)
#pred(#neg(#s(@x)))	→	#neg(#s(#s(@x)))	(33)
#pred(#pos(#s(#0)))	→	#0	(34)
#pred(#pos(#s(#s(@x))))	→	#pos(#s(@x))	(35)
#succ(#0)	→	#pos(#s(#0))	(36)
#succ(#neg(#s(#0)))	→	#0	(37)
#succ(#neg(#s(#s(@x))))	→	#neg(#s(@x))	(38)
#succ(#pos(#s(@x)))	→	#pos(#s(#s(@x)))	(39)

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

(41)

originates from

*(z0,z1)

→

#mult(z0,z1)

(40)

+^#(z0,z1)

→

c25(#add^#(z0,z1))

(43)

originates from

+(z0,z1)

→

#add(z0,z1)

(42)

computeLine^#(z0,z1,z2)

→

c26(computeLine#1^#(z0,z2,z1))

(45)

originates from

computeLine(z0,z1,z2)

→

computeLine#1(z0,z2,z1)

(44)

computeLine#1^#(::(z0,z1),z2,z3)

→

c27(computeLine#2^#(z3,z2,z0,z1))

(47)

originates from

computeLine#1(::(z0,z1),z2,z3)

→

computeLine#2(z3,z2,z0,z1)

(46)

computeLine#1^#(nil,z0,z1)

→

c28

(49)

originates from

computeLine#1(nil,z0,z1)

→

(48)

computeLine#2^#(::(z0,z1),z2,z3,z4)

→

c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))

(51)

originates from

computeLine#2(::(z0,z1),z2,z3,z4)

→

computeLine(z4,z1,lineMult(z3,z0,z2))

(50)

computeLine#2^#(nil,z0,z1,z2)

→

c30

(53)

originates from

computeLine#2(nil,z0,z1,z2)

→

nil

(52)

lineMult^#(z0,z1,z2)

→

c31(lineMult#1^#(z1,z2,z0))

(55)

originates from

lineMult(z0,z1,z2)

→

lineMult#1(z1,z2,z0)

(54)

lineMult#1^#(::(z0,z1),z2,z3)

→

c32(lineMult#2^#(z2,z3,z0,z1))

(57)

originates from

lineMult#1(::(z0,z1),z2,z3)

→

lineMult#2(z2,z3,z0,z1)

(56)

lineMult#1^#(nil,z0,z1)

→

c33

(59)

originates from

lineMult#1(nil,z0,z1)

→

nil

(58)

lineMult#2^#(::(z0,z1),z2,z3,z4)

→

c34(+^#(*(z3,z2),z0),*^#(z3,z2),lineMult^#(z2,z4,z1))

(61)

originates from

lineMult#2(::(z0,z1),z2,z3,z4)

→

::(+(*(z3,z2),z0),lineMult(z2,z4,z1))

(60)

lineMult#2^#(nil,z0,z1,z2)

→

c35(*^#(z1,z0),lineMult^#(z0,z2,nil))

(63)

originates from

lineMult#2(nil,z0,z1,z2)

→

::(*(z1,z0),lineMult(z0,z2,nil))

(62)

matrixMult^#(z0,z1)

→

c36(matrixMult#1^#(z0,z1))

(65)

originates from

matrixMult(z0,z1)

→

matrixMult#1(z0,z1)

(64)

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

→

c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))

(67)

originates from

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

→

::(computeLine(z0,z2,nil),matrixMult(z1,z2))

(66)

matrixMult#1^#(nil,z0)

→

c38

(69)

originates from

matrixMult#1(nil,z0)

→

nil

(68)

#add^#(#0,z0)

→

(71)

originates from

#add(#0,z0)

→

(70)

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

→

c1(#pred^#(z0))

(73)

originates from

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

→

#pred(z0)

(72)

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

→

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

(75)

originates from

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

→

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

(74)

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

→

c3(#succ^#(z0))

(77)

originates from

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

→

#succ(z0)

(76)

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

→

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

(79)

originates from

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

→

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

(78)

#mult^#(#0,#0)

→

(80)

originates from

#mult(#0,#0)

→

(21)

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

→

(82)

originates from

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

→

(81)

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

→

(84)

originates from

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

→

(83)

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

→

(86)

originates from

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

→

(85)

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

→

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

(88)

originates from

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

→

#pos(#natmult(z0,z1))

(87)

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

→

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

(90)

originates from

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

→

#neg(#natmult(z0,z1))

(89)

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

→

c11

(92)

originates from

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

→

(91)

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

→

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

(94)

originates from

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

→

#neg(#natmult(z0,z1))

(93)

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

→

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

(96)

originates from

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

→

#pos(#natmult(z0,z1))

(95)

#natmult^#(#0,z0)

→

c14

(98)

originates from

#natmult(#0,z0)

→

(97)

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

→

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

(100)

originates from

#natmult(#s(z0),z1)

→

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

(99)

#pred^#(#0)

→

c16

(101)

originates from

#pred(#0)

→

#neg(#s(#0))

(32)

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

→

c17

(103)

originates from

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

→

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

(102)

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

→

c18

(104)

originates from

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

→

(34)

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

→

c19

(106)

originates from

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

→

#pos(#s(z0))

(105)

#succ^#(#0)

→

c20

(107)

originates from

#succ(#0)

→

#pos(#s(#0))

(36)

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

→

c21

(108)

originates from

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

→

(37)

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

→

c22

(110)

originates from

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

→

#neg(#s(z0))

(109)

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

→

c23

(112)

originates from

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

→

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

(111)

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)

+^#(z0,z1)

computeLine^#(z0,z1,z2)

computeLine#1^#(::(z0,z1),z2,z3)

computeLine#1^#(nil,z0,z1)

computeLine#2^#(::(z0,z1),z2,z3,z4)

computeLine#2^#(nil,z0,z1,z2)

lineMult^#(z0,z1,z2)

lineMult#1^#(::(z0,z1),z2,z3)

lineMult#1^#(nil,z0,z1)

lineMult#2^#(::(z0,z1),z2,z3,z4)

lineMult#2^#(nil,z0,z1,z2)

matrixMult^#(z0,z1)

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

matrixMult#1^#(nil,z0)

1.1 Usable Rules

We remove the following rules since they are not usable.

computeLine(z0,z1,z2)	→	computeLine#1(z0,z2,z1)	(44)
computeLine#1(::(z0,z1),z2,z3)	→	computeLine#2(z3,z2,z0,z1)	(46)
computeLine#1(nil,z0,z1)	→	z0	(48)
computeLine#2(::(z0,z1),z2,z3,z4)	→	computeLine(z4,z1,lineMult(z3,z0,z2))	(50)
computeLine#2(nil,z0,z1,z2)	→	nil	(52)
matrixMult(z0,z1)	→	matrixMult#1(z0,z1)	(64)
matrixMult#1(::(z0,z1),z2)	→	::(computeLine(z0,z2,nil),matrixMult(z1,z2))	(66)
matrixMult#1(nil,z0)	→	nil	(68)

1.1.1 Rule Shifting

The rules

matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	2
[#succ(x₁)]	=	2
[#natmult(x₁, x₂)]	=	3 · x₁ + 0
[lineMult(x₁, x₂, x₃)]	=	3 + 3 · x₁ + 3 · x₂ + 3 · x₃
[lineMult#1(x₁, x₂, x₃)]	=	3 + 3 · x₁ + 3 · x₂ + 3 · x₃
[lineMult#2(x₁,...,x₄)]	=	3 + 3 · x₁ + 3 · x₂ + 3 · x₃ + 3 · x₄
[+(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[*(x₁, x₂)]	=	0
[#mult(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[#pred(x₁)]	=	3
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	0
[computeLine#1^#(x₁, x₂, x₃)]	=	0
[computeLine#2^#(x₁,...,x₄)]	=	0
[lineMult^#(x₁, x₂, x₃)]	=	0
[lineMult#1^#(x₁, x₂, x₃)]	=	0
[lineMult#2^#(x₁,...,x₄)]	=	0
[matrixMult^#(x₁, x₂)]	=	3 + 2 · x₁ + 3 · x₂
[matrixMult#1^#(x₁, x₂)]	=	2 · x₁ + 0 + 3 · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[::(x₁, x₂)]	=	2 + 1 · x₂
[nil]	=	2

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

#add^#(#0,z0)	→	c	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1 Rule Shifting

The rules

computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)

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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	0
[#succ(x₁)]	=	1 + 1 · x₁
[#natmult(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lineMult(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[lineMult#1(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[lineMult#2(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[+(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[*(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#mult(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#pred(x₁)]	=	1 + 1 · x₁
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[computeLine#1^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[computeLine#2^#(x₁,...,x₄)]	=	1 + 1 · x₃ + 1 · x₄
[lineMult^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[lineMult#1^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[lineMult#2^#(x₁,...,x₄)]	=	1 · x₂ + 0
[matrixMult^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[matrixMult#1^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(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	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1.1 Rule Shifting

The rules

computeLine#1^#(::(z0,z1),z2,z3)

→

c27(computeLine#2^#(z3,z2,z0,z1))

(47)

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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	1 + 1 · x₂
[#succ(x₁)]	=	0
[#natmult(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lineMult(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[lineMult#1(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[lineMult#2(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[+(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[*(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#mult(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#pred(x₁)]	=	1 + 1 · x₁
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[computeLine#1^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[computeLine#2^#(x₁,...,x₄)]	=	1 · x₃ + 0 + 1 · x₄
[lineMult^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[lineMult#1^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[lineMult#2^#(x₁,...,x₄)]	=	1 · x₂ + 0
[matrixMult^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[matrixMult#1^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(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	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1.1.1 Rule Shifting

The rules

computeLine#1^#(nil,z0,z1)

→

c28

(49)

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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	1 · x₂ + 0
[#succ(x₁)]	=	1 + 1 · x₁
[#natmult(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lineMult(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[lineMult#1(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[lineMult#2(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[+(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[*(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#mult(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#pred(x₁)]	=	1 + 1 · x₁
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[computeLine#1^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[computeLine#2^#(x₁,...,x₄)]	=	1 · x₃ + 0 + 1 · x₄
[lineMult^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[lineMult#1^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[lineMult#2^#(x₁,...,x₄)]	=	1 · x₂ + 0
[matrixMult^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[matrixMult#1^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[::(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[nil]	=	1

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

#add^#(#0,z0)	→	c	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1.1.1.1 Rule Shifting

The rules

computeLine^#(z0,z1,z2)

→

c26(computeLine#1^#(z0,z2,z1))

(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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	0
[#succ(x₁)]	=	1 + 1 · x₁
[#natmult(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lineMult(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[lineMult#1(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[lineMult#2(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[+(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[*(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#mult(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#pred(x₁)]	=	1 + 1 · x₁
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	1 + 1 · x₁
[computeLine#1^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[computeLine#2^#(x₁,...,x₄)]	=	1 + 1 · x₃ + 1 · x₄
[lineMult^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[lineMult#1^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[lineMult#2^#(x₁,...,x₄)]	=	1 · x₂ + 0
[matrixMult^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[matrixMult#1^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(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	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

lineMult#1^#(nil,z0,z1)

→

c33

(59)

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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	0
[#succ(x₁)]	=	3
[#natmult(x₁, x₂)]	=	3 · x₁ + 0
[lineMult(x₁, x₂, x₃)]	=	3 + 3 · x₁ + 3 · x₂ + 2 · x₃
[lineMult#1(x₁, x₂, x₃)]	=	3 + 3 · x₁ + 3 · x₂ + 3 · x₃
[lineMult#2(x₁,...,x₄)]	=	3 + 3 · x₁ + 3 · x₂ + 3 · x₃ + 3 · x₄
[+(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[*(x₁, x₂)]	=	0
[#mult(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[#pred(x₁)]	=	3
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	2 · x₁ + 0
[computeLine#1^#(x₁, x₂, x₃)]	=	2 · x₁ + 0
[computeLine#2^#(x₁,...,x₄)]	=	2 + 2 · x₄
[lineMult^#(x₁, x₂, x₃)]	=	1
[lineMult#1^#(x₁, x₂, x₃)]	=	1
[lineMult#2^#(x₁,...,x₄)]	=	1
[matrixMult^#(x₁, x₂)]	=	2 + 2 · x₁ + 3 · x₂
[matrixMult#1^#(x₁, x₂)]	=	2 · x₁ + 0 + 3 · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(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	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

lineMult#1^#(::(z0,z1),z2,z3)

→

c32(lineMult#2^#(z2,z3,z0,z1))

(57)

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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	0
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	0
[lineMult(x₁, x₂, x₃)]	=	0
[lineMult#1(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[lineMult#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₄ · x₄ + 1 · x₃ · x₄ + 1 · x₂ · x₄ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[+(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 2 · x₁ · x₁
[*(x₁, x₂)]	=	0
[#mult(x₁, x₂)]	=	1
[#pred(x₁)]	=	1
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	1 · x₂ · x₁ + 0
[computeLine#1^#(x₁, x₂, x₃)]	=	1 · x₁ · x₃ + 0
[computeLine#2^#(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₁ · x₄
[lineMult^#(x₁, x₂, x₃)]	=	1 · x₂ + 0
[lineMult#1^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[lineMult#2^#(x₁,...,x₄)]	=	1 · x₄ + 0
[matrixMult^#(x₁, x₂)]	=	2 · x₂ · x₂ + 0 + 1 · x₁ · x₂
[matrixMult#1^#(x₁, x₂)]	=	2 · x₂ · x₂ + 0 + 1 · x₁ · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(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	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)

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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	0
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	0
[lineMult(x₁, x₂, x₃)]	=	0
[lineMult#1(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[lineMult#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₄ · x₄ + 1 · x₃ · x₄ + 1 · x₂ · x₄ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[+(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[*(x₁, x₂)]	=	0
[#mult(x₁, x₂)]	=	1
[#pred(x₁)]	=	1
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	1
[computeLine^#(x₁, x₂, x₃)]	=	2 · x₂ · x₁ + 0
[computeLine#1^#(x₁, x₂, x₃)]	=	2 · x₁ · x₃ + 0
[computeLine#2^#(x₁,...,x₄)]	=	2 · x₁ + 0 + 2 · x₁ · x₄
[lineMult^#(x₁, x₂, x₃)]	=	2 · x₂ + 0
[lineMult#1^#(x₁, x₂, x₃)]	=	2 · x₁ + 0
[lineMult#2^#(x₁,...,x₄)]	=	2 + 2 · x₄
[matrixMult^#(x₁, x₂)]	=	2 · x₂ · x₂ + 0 + 2 · x₁ · x₂
[matrixMult#1^#(x₁, x₂)]	=	2 · x₂ · x₂ + 0 + 2 · x₁ · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(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	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

lineMult^#(z0,z1,z2)

→

c31(lineMult#1^#(z1,z2,z0))

(55)

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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	0
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	1
[lineMult(x₁, x₂, x₃)]	=	0
[lineMult#1(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[lineMult#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₄ · x₄ + 1 · x₃ · x₄ + 1 · x₂ · x₄ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[+(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂ + 2 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[*(x₁, x₂)]	=	2 · x₂ + 0 + 2 · x₂ · x₂
[#mult(x₁, x₂)]	=	2 · x₂ + 0 + 2 · x₂ · x₂
[#pred(x₁)]	=	1
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	0
[#natmult^#(x₁, x₂)]	=	0
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ · x₁
[computeLine#1^#(x₁, x₂, x₃)]	=	2 · x₁ · x₃ + 0
[computeLine#2^#(x₁,...,x₄)]	=	2 · x₁ + 0 + 2 · x₁ · x₄
[lineMult^#(x₁, x₂, x₃)]	=	1 + 1 · x₂
[lineMult#1^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[lineMult#2^#(x₁,...,x₄)]	=	1 + 1 · x₄
[matrixMult^#(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[matrixMult#1^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[#0]	=	0
[#neg(x₁)]	=	1
[#pos(x₁)]	=	1 + 1 · x₁
[#s(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	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

*^#(z0,z1)

→

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

(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₁)]	=	1 · x₁ + 0
[c27(x₁)]	=	1 · x₁ + 0
[c28]	=	0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[c31(x₁)]	=	1 · x₁ + 0
[c32(x₁)]	=	1 · x₁ + 0
[c33]	=	0
[c34(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c35(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c36(x₁)]	=	1 · x₁ + 0
[c37(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c38]	=	0
[#add(x₁, x₂)]	=	0
[#succ(x₁)]	=	1
[#natmult(x₁, x₂)]	=	0
[lineMult(x₁, x₂, x₃)]	=	0
[lineMult#1(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[lineMult#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₄ · x₄ + 1 · x₃ · x₄ + 1 · x₂ · x₄ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[+(x₁, x₂)]	=	1 + 2 · x₁ + 1 · x₂ + 2 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[*(x₁, x₂)]	=	0
[#mult(x₁, x₂)]	=	1
[#pred(x₁)]	=	1
[#add^#(x₁, x₂)]	=	0
[#mult^#(x₁, x₂)]	=	1
[#natmult^#(x₁, x₂)]	=	1
[#pred^#(x₁)]	=	0
[#succ^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	2
[+^#(x₁, x₂)]	=	0
[computeLine^#(x₁, x₂, x₃)]	=	2 · x₂ + 0
[computeLine#1^#(x₁, x₂, x₃)]	=	2 · x₃ + 0
[computeLine#2^#(x₁,...,x₄)]	=	2 · x₁ + 0
[lineMult^#(x₁, x₂, x₃)]	=	1 · x₂ + 0
[lineMult#1^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[lineMult#2^#(x₁,...,x₄)]	=	2 + 1 · x₄
[matrixMult^#(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂ · x₂ + 1 · x₁ · x₂
[matrixMult#1^#(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂ · x₂ + 1 · x₁ · x₂
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(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	(71)
#add^#(#neg(#s(#0)),z0)	→	c1(#pred^#(z0))	(73)
#add^#(#neg(#s(#s(z0))),z1)	→	c2(#pred^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(75)
#add^#(#pos(#s(#0)),z0)	→	c3(#succ^#(z0))	(77)
#add^#(#pos(#s(#s(z0))),z1)	→	c4(#succ^#(#add(#pos(#s(z0)),z1)),#add^#(#pos(#s(z0)),z1))	(79)
#mult^#(#0,#0)	→	c5	(80)
#mult^#(#0,#neg(z0))	→	c6	(82)
#mult^#(#0,#pos(z0))	→	c7	(84)
#mult^#(#neg(z0),#0)	→	c8	(86)
#mult^#(#neg(z0),#neg(z1))	→	c9(#natmult^#(z0,z1))	(88)
#mult^#(#neg(z0),#pos(z1))	→	c10(#natmult^#(z0,z1))	(90)
#mult^#(#pos(z0),#0)	→	c11	(92)
#mult^#(#pos(z0),#neg(z1))	→	c12(#natmult^#(z0,z1))	(94)
#mult^#(#pos(z0),#pos(z1))	→	c13(#natmult^#(z0,z1))	(96)
#natmult^#(#0,z0)	→	c14	(98)
#natmult^#(#s(z0),z1)	→	c15(#add^#(#pos(z1),#natmult(z0,z1)),#natmult^#(z0,z1))	(100)
#pred^#(#0)	→	c16	(101)
#pred^#(#neg(#s(z0)))	→	c17	(103)
#pred^#(#pos(#s(#0)))	→	c18	(104)
#pred^#(#pos(#s(#s(z0))))	→	c19	(106)
#succ^#(#0)	→	c20	(107)
#succ^#(#neg(#s(#0)))	→	c21	(108)
#succ^#(#neg(#s(#s(z0))))	→	c22	(110)
#succ^#(#pos(#s(z0)))	→	c23	(112)
*^#(z0,z1)	→	c24(#mult^#(z0,z1))	(41)
+^#(z0,z1)	→	c25(#add^#(z0,z1))	(43)
computeLine^#(z0,z1,z2)	→	c26(computeLine#1^#(z0,z2,z1))	(45)
computeLine#1^#(::(z0,z1),z2,z3)	→	c27(computeLine#2^#(z3,z2,z0,z1))	(47)
computeLine#1^#(nil,z0,z1)	→	c28	(49)
computeLine#2^#(::(z0,z1),z2,z3,z4)	→	c29(computeLine^#(z4,z1,lineMult(z3,z0,z2)),lineMult^#(z3,z0,z2))	(51)
computeLine#2^#(nil,z0,z1,z2)	→	c30	(53)
lineMult^#(z0,z1,z2)	→	c31(lineMult#1^#(z1,z2,z0))	(55)
lineMult#1^#(::(z0,z1),z2,z3)	→	c32(lineMult#2^#(z2,z3,z0,z1))	(57)
lineMult#1^#(nil,z0,z1)	→	c33	(59)
lineMult#2^#(::(z0,z1),z2,z3,z4)	→	c34(+^#((z3,z2),z0),^#(z3,z2),lineMult^#(z2,z4,z1))	(61)
lineMult#2^#(nil,z0,z1,z2)	→	c35(*^#(z1,z0),lineMult^#(z0,z2,nil))	(63)
matrixMult^#(z0,z1)	→	c36(matrixMult#1^#(z0,z1))	(65)
matrixMult#1^#(::(z0,z1),z2)	→	c37(computeLine^#(z0,z2,nil),matrixMult^#(z1,z2))	(67)
matrixMult#1^#(nil,z0)	→	c38	(69)

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