Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/raML/duplicates.raml)

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

#equal(@x,@y)	→	#eq(@x,@y)	(1)
and(@x,@y)	→	#and(@x,@y)	(2)
eq(@l1,@l2)	→	eq#1(@l1,@l2)	(3)
eq#1(::(@x,@xs),@l2)	→	eq#3(@l2,@x,@xs)	(4)
eq#1(nil,@l2)	→	eq#2(@l2)	(5)
eq#2(::(@y,@ys))	→	#false	(6)
eq#2(nil)	→	#true	(7)
eq#3(::(@y,@ys),@x,@xs)	→	and(#equal(@x,@y),eq(@xs,@ys))	(8)
eq#3(nil,@x,@xs)	→	#false	(9)
nub(@l)	→	nub#1(@l)	(10)
nub#1(::(@x,@xs))	→	::(@x,nub(remove(@x,@xs)))	(11)
nub#1(nil)	→	nil	(12)
remove(@x,@l)	→	remove#1(@l,@x)	(13)
remove#1(::(@y,@ys),@x)	→	remove#2(eq(@x,@y),@x,@y,@ys)	(14)
remove#1(nil,@x)	→	nil	(15)
remove#2(#false,@x,@y,@ys)	→	::(@y,remove(@x,@ys))	(16)
remove#2(#true,@x,@y,@ys)	→	remove(@x,@ys)	(17)

and S is the following TRS.

#and(#false,#false)	→	#false	(18)
#and(#false,#true)	→	#false	(19)
#and(#true,#false)	→	#false	(20)
#and(#true,#true)	→	#true	(21)
#eq(#0,#0)	→	#true	(22)
#eq(#0,#neg(@y))	→	#false	(23)
#eq(#0,#pos(@y))	→	#false	(24)
#eq(#0,#s(@y))	→	#false	(25)
#eq(#neg(@x),#0)	→	#false	(26)
#eq(#neg(@x),#neg(@y))	→	#eq(@x,@y)	(27)
#eq(#neg(@x),#pos(@y))	→	#false	(28)
#eq(#pos(@x),#0)	→	#false	(29)
#eq(#pos(@x),#neg(@y))	→	#false	(30)
#eq(#pos(@x),#pos(@y))	→	#eq(@x,@y)	(31)
#eq(#s(@x),#0)	→	#false	(32)
#eq(#s(@x),#s(@y))	→	#eq(@x,@y)	(33)
#eq(::(@x_1,@x_2),::(@y_1,@y_2))	→	#and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))	(34)
#eq(::(@x_1,@x_2),nil)	→	#false	(35)
#eq(nil,::(@y_1,@y_2))	→	#false	(36)
#eq(nil,nil)	→	#true	(37)

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:

#equal^#(z0,z1)

→

c20(#eq^#(z0,z1))

(39)

originates from

#equal(z0,z1)

→

#eq(z0,z1)

(38)

and^#(z0,z1)

→

c21(#and^#(z0,z1))

(41)

originates from

and(z0,z1)

→

#and(z0,z1)

(40)

eq^#(z0,z1)

→

c22(eq#1^#(z0,z1))

(43)

originates from

eq(z0,z1)

→

eq#1(z0,z1)

(42)

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

→

c23(eq#3^#(z2,z0,z1))

(45)

originates from

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

→

eq#3(z2,z0,z1)

(44)

eq#1^#(nil,z0)

→

c24(eq#2^#(z0))

(47)

originates from

eq#1(nil,z0)

→

eq#2(z0)

(46)

eq#2^#(::(z0,z1))

→

c25

(49)

originates from

eq#2(::(z0,z1))

→

#false

(48)

eq#2^#(nil)

→

c26

(50)

originates from

eq#2(nil)

→

#true

(7)

eq#3^#(::(z0,z1),z2,z3)

→

c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))

(52)

originates from

eq#3(::(z0,z1),z2,z3)

→

and(#equal(z2,z0),eq(z3,z1))

(51)

eq#3^#(nil,z0,z1)

→

c28

(54)

originates from

eq#3(nil,z0,z1)

→

#false

(53)

nub^#(z0)

→

c29(nub#1^#(z0))

(56)

originates from

nub(z0)

→

nub#1(z0)

(55)

nub#1^#(::(z0,z1))

→

c30(nub^#(remove(z0,z1)),remove^#(z0,z1))

(58)

originates from

nub#1(::(z0,z1))

→

::(z0,nub(remove(z0,z1)))

(57)

nub#1^#(nil)

→

c31

(59)

originates from

nub#1(nil)

→

nil

(12)

remove^#(z0,z1)

→

c32(remove#1^#(z1,z0))

(61)

originates from

remove(z0,z1)

→

remove#1(z1,z0)

(60)

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

→

c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))

(63)

originates from

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

→

remove#2(eq(z2,z0),z2,z0,z1)

(62)

remove#1^#(nil,z0)

→

c34

(65)

originates from

remove#1(nil,z0)

→

nil

(64)

remove#2^#(#false,z0,z1,z2)

→

c35(remove^#(z0,z2))

(67)

originates from

remove#2(#false,z0,z1,z2)

→

::(z1,remove(z0,z2))

(66)

remove#2^#(#true,z0,z1,z2)

→

c36(remove^#(z0,z2))

(69)

originates from

remove#2(#true,z0,z1,z2)

→

remove(z0,z2)

(68)

#and^#(#false,#false)

→

(70)

originates from

#and(#false,#false)

→

#false

(18)

#and^#(#false,#true)

→

(71)

originates from

#and(#false,#true)

→

#false

(19)

#and^#(#true,#false)

→

(72)

originates from

#and(#true,#false)

→

#false

(20)

#and^#(#true,#true)

→

(73)

originates from

#and(#true,#true)

→

#true

(21)

#eq^#(#0,#0)

→

(74)

originates from

#eq(#0,#0)

→

#true

(22)

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

→

(76)

originates from

#eq(#0,#neg(z0))

→

#false

(75)

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

→

(78)

originates from

#eq(#0,#pos(z0))

→

#false

(77)

#eq^#(#0,#s(z0))

→

(80)

originates from

#eq(#0,#s(z0))

→

#false

(79)

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

→

(82)

originates from

#eq(#neg(z0),#0)

→

#false

(81)

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

→

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

(84)

originates from

#eq(#neg(z0),#neg(z1))

→

#eq(z0,z1)

(83)

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

→

c10

(86)

originates from

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

→

#false

(85)

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

→

c11

(88)

originates from

#eq(#pos(z0),#0)

→

#false

(87)

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

→

c12

(90)

originates from

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

→

#false

(89)

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

→

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

(92)

originates from

#eq(#pos(z0),#pos(z1))

→

#eq(z0,z1)

(91)

#eq^#(#s(z0),#0)

→

c14

(94)

originates from

#eq(#s(z0),#0)

→

#false

(93)

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

→

c15(#eq^#(z0,z1))

(96)

originates from

#eq(#s(z0),#s(z1))

→

#eq(z0,z1)

(95)

#eq^#(::(z0,z1),::(z2,z3))

→

c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))

(98)

originates from

#eq(::(z0,z1),::(z2,z3))

→

#and(#eq(z0,z2),#eq(z1,z3))

(97)

#eq^#(::(z0,z1),nil)

→

c17

(100)

originates from

#eq(::(z0,z1),nil)

→

#false

(99)

#eq^#(nil,::(z0,z1))

→

c18

(102)

originates from

#eq(nil,::(z0,z1))

→

#false

(101)

#eq^#(nil,nil)

→

c19

(103)

originates from

#eq(nil,nil)

→

#true

(37)

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

#and^#(#false,#false)

#and^#(#false,#true)

#and^#(#true,#false)

#and^#(#true,#true)

#eq^#(#0,#0)

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

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

#eq^#(#0,#s(z0))

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

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

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

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

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

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

#eq^#(#s(z0),#0)

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

#eq^#(::(z0,z1),::(z2,z3))

#eq^#(::(z0,z1),nil)

#eq^#(nil,::(z0,z1))

#eq^#(nil,nil)

#equal^#(z0,z1)

and^#(z0,z1)

eq^#(z0,z1)

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

eq#1^#(nil,z0)

eq#2^#(::(z0,z1))

eq#2^#(nil)

eq#3^#(::(z0,z1),z2,z3)

eq#3^#(nil,z0,z1)

nub^#(z0)

nub#1^#(::(z0,z1))

nub#1^#(nil)

remove^#(z0,z1)

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

remove#1^#(nil,z0)

remove#2^#(#false,z0,z1,z2)

remove#2^#(#true,z0,z1,z2)

1.1 Usable Rules

We remove the following rules since they are not usable.

nub(z0)	→	nub#1(z0)	(55)
nub#1(::(z0,z1))	→	::(z0,nub(remove(z0,z1)))	(57)
nub#1(nil)	→	nil	(12)

1.1.1 Rule Shifting

The rules

nub#1^#(nil)

→

c31

(59)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[eq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1 + 1 · x₁
[remove(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[remove#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[remove#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[eq#1^#(x₁, x₂)]	=	0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	0
[nub^#(x₁)]	=	1
[nub#1^#(x₁)]	=	1
[remove^#(x₁, x₂)]	=	0
[remove#1^#(x₁, x₂)]	=	0
[remove#2^#(x₁,...,x₄)]	=	0
[::(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#pos(x₁)]	=	1 + 1 · x₁
[#s(x₁)]	=	1 + 1 · x₁

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)

1.1.1.1 Rule Shifting

The rules

nub#1^#(::(z0,z1))

→

c30(nub^#(remove(z0,z1)),remove^#(z0,z1))

(58)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[eq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1 + 1 · x₁
[remove(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[remove#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[remove#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[eq#1^#(x₁, x₂)]	=	0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	0
[nub^#(x₁)]	=	1 + 1 · x₁
[nub#1^#(x₁)]	=	1 + 1 · x₁
[remove^#(x₁, x₂)]	=	0
[remove#1^#(x₁, x₂)]	=	0
[remove#2^#(x₁,...,x₄)]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#pos(x₁)]	=	1 + 1 · x₁
[#s(x₁)]	=	1 + 1 · x₁

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1 Rule Shifting

The rules

nub^#(z0)

→

c29(nub#1^#(z0))

(56)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[eq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1 + 1 · x₁
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	1 + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[eq#1^#(x₁, x₂)]	=	0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	0
[nub^#(x₁)]	=	1 + 1 · x₁
[nub#1^#(x₁)]	=	1 · x₁ + 0
[remove^#(x₁, x₂)]	=	1 · x₁ + 0
[remove#1^#(x₁, x₂)]	=	1 · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	1 · x₂ + 0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#pos(x₁)]	=	1 + 1 · x₁
[#s(x₁)]	=	1 + 1 · x₁

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1 Rule Shifting

The rules

remove#1^#(nil,z0)

→

c34

(65)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[eq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1 + 1 · x₁
[remove(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[remove#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[remove#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[eq#1^#(x₁, x₂)]	=	0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	0
[nub^#(x₁)]	=	1 + 1 · x₁
[nub#1^#(x₁)]	=	1 + 1 · x₁
[remove^#(x₁, x₂)]	=	1
[remove#1^#(x₁, x₂)]	=	1
[remove#2^#(x₁,...,x₄)]	=	1
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#pos(x₁)]	=	1 + 1 · x₁
[#s(x₁)]	=	1 + 1 · x₁

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1 Rule Shifting

The rules

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

→

c23(eq#3^#(z2,z0,z1))

(45)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	2
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	2 + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[#equal^#(x₁, x₂)]	=	2 · x₁ + 0 + 1 · x₁ · x₂
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	2 · x₁ + 0 + 1 · x₁ · x₂
[eq#1^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₁ · x₂
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	1 · x₁ · x₃ + 0 + 1 · x₂ · x₁
[nub^#(x₁)]	=	1 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[remove#1^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	1 · x₂ · x₄ + 0
[::(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	1 · x₁ + 0
[#pos(x₁)]	=	1 · x₁ + 0
[#s(x₁)]	=	1 · x₁ + 0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

eq#2^#(nil)

→

c26

(50)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	1 · x₃ + 0 + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[eq#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[eq#2^#(x₁)]	=	1 · x₁ + 0
[eq#3^#(x₁, x₂, x₃)]	=	2 · x₁ · x₃ + 0
[nub^#(x₁)]	=	1 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[::(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[nil]	=	1
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

eq#2^#(::(z0,z1))

→

c25

(49)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	2
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	1 + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[eq#1^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[eq#2^#(x₁)]	=	1 · x₁ + 0
[eq#3^#(x₁, x₂, x₃)]	=	1 · x₁ · x₃ + 0
[nub^#(x₁)]	=	2 + 1 · x₁ · x₁
[nub#1^#(x₁)]	=	1 + 1 · x₁ · x₁
[remove^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[remove#1^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	1 · x₂ · x₄ + 0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	2
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 + 1 · x₂
[remove#1(x₁, x₂)]	=	1 + 1 · x₁
[remove#2(x₁,...,x₄)]	=	2 + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	2 · x₁ + 0
[eq#1^#(x₁, x₂)]	=	2 · x₁ + 0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	1 + 2 · x₃
[nub^#(x₁)]	=	2 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

remove#2^#(#true,z0,z1,z2)

→

c36(remove^#(z0,z2))

(69)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	1 · x₂ + 0
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	1 · x₁ + 0
[eq#1(x₁, x₂)]	=	1 · x₁ + 0
[eq#3(x₁, x₂, x₃)]	=	1 · x₃ + 0
[and(x₁, x₂)]	=	1 · x₂ + 0
[eq#2(x₁)]	=	2
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	1 + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[eq#1^#(x₁, x₂)]	=	0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	0
[nub^#(x₁)]	=	2 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	2 · x₁ + 0 + 2 · x₂ · x₄ + 2 · x₃ · x₁
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	2
[#false]	=	0
[#true]	=	2
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
eq#3(::(z0,z1),z2,z3)	→	and(#equal(z2,z0),eq(z3,z1))	(51)
and(z0,z1)	→	#and(z0,z1)	(40)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
#and(#false,#true)	→	#false	(19)
#and(#true,#false)	→	#false	(20)
#and(#true,#true)	→	#true	(21)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove#1(nil,z0)	→	nil	(64)
eq#1(::(z0,z1),z2)	→	eq#3(z2,z0,z1)	(44)
eq#1(nil,z0)	→	eq#2(z0)	(46)
eq#3(nil,z0,z1)	→	#false	(53)
eq#2(nil)	→	#true	(7)
eq(z0,z1)	→	eq#1(z0,z1)	(42)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
eq#2(::(z0,z1))	→	#false	(48)
#and(#false,#false)	→	#false	(18)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

and^#(z0,z1)

→

c21(#and^#(z0,z1))

(41)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	1 + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	1
[eq^#(x₁, x₂)]	=	1 · x₁ + 0
[eq#1^#(x₁, x₂)]	=	1 · x₁ + 0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	1 + 1 · x₃
[nub^#(x₁)]	=	1 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

remove^#(z0,z1)

→

c32(remove#1^#(z1,z0))

(61)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	1 + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[eq#1^#(x₁, x₂)]	=	0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	0
[nub^#(x₁)]	=	1 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	1 + 1 · x₂
[remove#1^#(x₁, x₂)]	=	1 · x₁ + 0
[remove#2^#(x₁,...,x₄)]	=	1 + 1 · x₄
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

#equal^#(z0,z1)

→

c20(#eq^#(z0,z1))

(39)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	2
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	2
[eq#1(x₁, x₂)]	=	2
[eq#3(x₁, x₂, x₃)]	=	2
[and(x₁, x₂)]	=	2
[eq#2(x₁)]	=	2
[remove(x₁, x₂)]	=	2 + 1 · x₂
[remove#1(x₁, x₂)]	=	2 + 1 · x₁
[remove#2(x₁,...,x₄)]	=	1 · x₃ + 0 + 1 · x₄ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[#equal^#(x₁, x₂)]	=	1 + 1 · x₁ · x₂
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[eq#1^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₁ · x₃ + 1 · x₂ · x₁
[nub^#(x₁)]	=	2 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[remove#1^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	1 · x₂ · x₄ + 0
[::(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	2
[#true]	=	2
[#0]	=	2
[#neg(x₁)]	=	1 · x₁ + 0
[#pos(x₁)]	=	1 · x₁ + 0
[#s(x₁)]	=	1 · x₁ + 0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
eq#3(::(z0,z1),z2,z3)	→	and(#equal(z2,z0),eq(z3,z1))	(51)
and(z0,z1)	→	#and(z0,z1)	(40)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
#and(#false,#true)	→	#false	(19)
#and(#true,#false)	→	#false	(20)
#and(#true,#true)	→	#true	(21)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove#1(nil,z0)	→	nil	(64)
eq#1(::(z0,z1),z2)	→	eq#3(z2,z0,z1)	(44)
eq#1(nil,z0)	→	eq#2(z0)	(46)
eq#3(nil,z0,z1)	→	#false	(53)
eq#2(nil)	→	#true	(7)
eq(z0,z1)	→	eq#1(z0,z1)	(42)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
eq#2(::(z0,z1))	→	#false	(48)
#and(#false,#false)	→	#false	(18)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

eq#1^#(nil,z0)

→

c24(eq#2^#(z0))

(47)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	2
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	2 + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	1 · x₁ + 0
[eq#1^#(x₁, x₂)]	=	1 · x₁ + 0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	2 + 1 · x₃
[nub^#(x₁)]	=	2 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[remove#2^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[::(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[nil]	=	1
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	2
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	2 + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	0
[eq#1^#(x₁, x₂)]	=	0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	0
[nub^#(x₁)]	=	2 + 1 · x₁ · x₁
[nub#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	1 · x₂ + 0
[remove#1^#(x₁, x₂)]	=	1 · x₁ + 0
[remove#2^#(x₁,...,x₄)]	=	1 + 1 · x₄
[::(x₁, x₂)]	=	2 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

eq^#(z0,z1)

→

c22(eq#1^#(z0,z1))

(43)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20(x₁)]	=	1 · x₁ + 0
[c21(x₁)]	=	1 · x₁ + 0
[c22(x₁)]	=	1 · x₁ + 0
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c28]	=	0
[c29(x₁)]	=	1 · x₁ + 0
[c30(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c31]	=	0
[c32(x₁)]	=	1 · x₁ + 0
[c33(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c34]	=	0
[c35(x₁)]	=	1 · x₁ + 0
[c36(x₁)]	=	1 · x₁ + 0
[#eq(x₁, x₂)]	=	0
[#and(x₁, x₂)]	=	1
[#equal(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[eq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[eq#3(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[and(x₁, x₂)]	=	1
[eq#2(x₁)]	=	1
[remove(x₁, x₂)]	=	1 · x₂ + 0
[remove#1(x₁, x₂)]	=	1 · x₁ + 0
[remove#2(x₁,...,x₄)]	=	2 + 1 · x₃ + 1 · x₄
[#and^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[eq^#(x₁, x₂)]	=	1 + 1 · x₂
[eq#1^#(x₁, x₂)]	=	1 · x₂ + 0
[eq#2^#(x₁)]	=	0
[eq#3^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[nub^#(x₁)]	=	2 · x₁ · x₁ + 0
[nub#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[remove^#(x₁, x₂)]	=	1 · x₂ + 0
[remove#1^#(x₁, x₂)]	=	1 · x₁ + 0
[remove#2^#(x₁,...,x₄)]	=	1 · x₄ + 0
[::(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0

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

#and^#(#false,#false)	→	c	(70)
#and^#(#false,#true)	→	c1	(71)
#and^#(#true,#false)	→	c2	(72)
#and^#(#true,#true)	→	c3	(73)
#eq^#(#0,#0)	→	c4	(74)
#eq^#(#0,#neg(z0))	→	c5	(76)
#eq^#(#0,#pos(z0))	→	c6	(78)
#eq^#(#0,#s(z0))	→	c7	(80)
#eq^#(#neg(z0),#0)	→	c8	(82)
#eq^#(#neg(z0),#neg(z1))	→	c9(#eq^#(z0,z1))	(84)
#eq^#(#neg(z0),#pos(z1))	→	c10	(86)
#eq^#(#pos(z0),#0)	→	c11	(88)
#eq^#(#pos(z0),#neg(z1))	→	c12	(90)
#eq^#(#pos(z0),#pos(z1))	→	c13(#eq^#(z0,z1))	(92)
#eq^#(#s(z0),#0)	→	c14	(94)
#eq^#(#s(z0),#s(z1))	→	c15(#eq^#(z0,z1))	(96)
#eq^#(::(z0,z1),::(z2,z3))	→	c16(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(98)
#eq^#(::(z0,z1),nil)	→	c17	(100)
#eq^#(nil,::(z0,z1))	→	c18	(102)
#eq^#(nil,nil)	→	c19	(103)
#equal^#(z0,z1)	→	c20(#eq^#(z0,z1))	(39)
and^#(z0,z1)	→	c21(#and^#(z0,z1))	(41)
eq^#(z0,z1)	→	c22(eq#1^#(z0,z1))	(43)
eq#1^#(::(z0,z1),z2)	→	c23(eq#3^#(z2,z0,z1))	(45)
eq#1^#(nil,z0)	→	c24(eq#2^#(z0))	(47)
eq#2^#(::(z0,z1))	→	c25	(49)
eq#2^#(nil)	→	c26	(50)
eq#3^#(::(z0,z1),z2,z3)	→	c27(and^#(#equal(z2,z0),eq(z3,z1)),#equal^#(z2,z0),eq^#(z3,z1))	(52)
eq#3^#(nil,z0,z1)	→	c28	(54)
nub^#(z0)	→	c29(nub#1^#(z0))	(56)
nub#1^#(::(z0,z1))	→	c30(nub^#(remove(z0,z1)),remove^#(z0,z1))	(58)
nub#1^#(nil)	→	c31	(59)
remove^#(z0,z1)	→	c32(remove#1^#(z1,z0))	(61)
remove#1^#(::(z0,z1),z2)	→	c33(remove#2^#(eq(z2,z0),z2,z0,z1),eq^#(z2,z0))	(63)
remove#1^#(nil,z0)	→	c34	(65)
remove#2^#(#false,z0,z1,z2)	→	c35(remove^#(z0,z2))	(67)
remove#2^#(#true,z0,z1,z2)	→	c36(remove^#(z0,z2))	(69)
remove#2(#false,z0,z1,z2)	→	::(z1,remove(z0,z2))	(66)
remove#2(#true,z0,z1,z2)	→	remove(z0,z2)	(68)
remove#1(::(z0,z1),z2)	→	remove#2(eq(z2,z0),z2,z0,z1)	(62)
remove(z0,z1)	→	remove#1(z1,z0)	(60)
remove#1(nil,z0)	→	nil	(64)

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