Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/raML/listsort.raml)

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

#equal(@x,@y)	→	#eq(@x,@y)	(1)
#less(@x,@y)	→	#cklt(#compare(@x,@y))	(2)
and(@x,@y)	→	#and(@x,@y)	(3)
insert(@x,@l)	→	insert#1(@l,@x)	(4)
insert#1(::(@y,@ys),@x)	→	insert#2(leq(@x,@y),@x,@y,@ys)	(5)
insert#1(nil,@x)	→	::(@x,nil)	(6)
insert#2(#false,@x,@y,@ys)	→	::(@y,insert(@x,@ys))	(7)
insert#2(#true,@x,@y,@ys)	→	::(@x,::(@y,@ys))	(8)
isortlist(@l)	→	isortlist#1(@l)	(9)
isortlist#1(::(@x,@xs))	→	insert(@x,isortlist(@xs))	(10)
isortlist#1(nil)	→	nil	(11)
leq(@l1,@l2)	→	leq#1(@l1,@l2)	(12)
leq#1(::(@x,@xs),@l2)	→	leq#2(@l2,@x,@xs)	(13)
leq#1(nil,@l2)	→	#true	(14)
leq#2(::(@y,@ys),@x,@xs)	→	or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))	(15)
leq#2(nil,@x,@xs)	→	#false	(16)
or(@x,@y)	→	#or(@x,@y)	(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)
#cklt(#EQ)	→	#false	(22)
#cklt(#GT)	→	#false	(23)
#cklt(#LT)	→	#true	(24)
#compare(#0,#0)	→	#EQ	(25)
#compare(#0,#neg(@y))	→	#GT	(26)
#compare(#0,#pos(@y))	→	#LT	(27)
#compare(#0,#s(@y))	→	#LT	(28)
#compare(#neg(@x),#0)	→	#LT	(29)
#compare(#neg(@x),#neg(@y))	→	#compare(@y,@x)	(30)
#compare(#neg(@x),#pos(@y))	→	#LT	(31)
#compare(#pos(@x),#0)	→	#GT	(32)
#compare(#pos(@x),#neg(@y))	→	#GT	(33)
#compare(#pos(@x),#pos(@y))	→	#compare(@x,@y)	(34)
#compare(#s(@x),#0)	→	#GT	(35)
#compare(#s(@x),#s(@y))	→	#compare(@x,@y)	(36)
#eq(#0,#0)	→	#true	(37)
#eq(#0,#neg(@y))	→	#false	(38)
#eq(#0,#pos(@y))	→	#false	(39)
#eq(#0,#s(@y))	→	#false	(40)
#eq(#neg(@x),#0)	→	#false	(41)
#eq(#neg(@x),#neg(@y))	→	#eq(@x,@y)	(42)
#eq(#neg(@x),#pos(@y))	→	#false	(43)
#eq(#pos(@x),#0)	→	#false	(44)
#eq(#pos(@x),#neg(@y))	→	#false	(45)
#eq(#pos(@x),#pos(@y))	→	#eq(@x,@y)	(46)
#eq(#s(@x),#0)	→	#false	(47)
#eq(#s(@x),#s(@y))	→	#eq(@x,@y)	(48)
#eq(::(@x_1,@x_2),::(@y_1,@y_2))	→	#and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))	(49)
#eq(::(@x_1,@x_2),nil)	→	#false	(50)
#eq(nil,::(@y_1,@y_2))	→	#false	(51)
#eq(nil,nil)	→	#true	(52)
#or(#false,#false)	→	#false	(53)
#or(#false,#true)	→	#true	(54)
#or(#true,#false)	→	#true	(55)
#or(#true,#true)	→	#true	(56)

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)

→

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

(58)

originates from

#equal(z0,z1)

→

#eq(z0,z1)

(57)

#less^#(z0,z1)

→

c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))

(60)

originates from

#less(z0,z1)

→

#cklt(#compare(z0,z1))

(59)

and^#(z0,z1)

→

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

(62)

originates from

and(z0,z1)

→

#and(z0,z1)

(61)

insert^#(z0,z1)

→

c42(insert#1^#(z1,z0))

(64)

originates from

insert(z0,z1)

→

insert#1(z1,z0)

(63)

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

→

c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))

(66)

originates from

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

→

insert#2(leq(z2,z0),z2,z0,z1)

(65)

insert#1^#(nil,z0)

→

c44

(68)

originates from

insert#1(nil,z0)

→

::(z0,nil)

(67)

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

→

c45(insert^#(z0,z2))

(70)

originates from

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

→

::(z1,insert(z0,z2))

(69)

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

→

c46

(72)

originates from

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

→

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

(71)

isortlist^#(z0)

→

c47(isortlist#1^#(z0))

(74)

originates from

isortlist(z0)

→

isortlist#1(z0)

(73)

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

→

c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))

(76)

originates from

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

→

insert(z0,isortlist(z1))

(75)

isortlist#1^#(nil)

→

c49

(77)

originates from

isortlist#1(nil)

→

nil

(11)

leq^#(z0,z1)

→

c50(leq#1^#(z0,z1))

(79)

originates from

leq(z0,z1)

→

leq#1(z0,z1)

(78)

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

→

c51(leq#2^#(z2,z0,z1))

(81)

originates from

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

→

leq#2(z2,z0,z1)

(80)

leq#1^#(nil,z0)

→

c52

(83)

originates from

leq#1(nil,z0)

→

#true

(82)

leq#2^#(::(z0,z1),z2,z3)

→

c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))

(85)

originates from

leq#2(::(z0,z1),z2,z3)

→

or(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1)))

(84)

leq#2^#(nil,z0,z1)

→

c54

(87)

originates from

leq#2(nil,z0,z1)

→

#false

(86)

or^#(z0,z1)

→

c55(#or^#(z0,z1))

(89)

originates from

or(z0,z1)

→

#or(z0,z1)

(88)

#and^#(#false,#false)

→

(90)

originates from

#and(#false,#false)

→

#false

(18)

#and^#(#false,#true)

→

(91)

originates from

#and(#false,#true)

→

#false

(19)

#and^#(#true,#false)

→

(92)

originates from

#and(#true,#false)

→

#false

(20)

#and^#(#true,#true)

→

(93)

originates from

#and(#true,#true)

→

#true

(21)

#cklt^#(#EQ)

→

(94)

originates from

#cklt(#EQ)

→

#false

(22)

#cklt^#(#GT)

→

(95)

originates from

#cklt(#GT)

→

#false

(23)

#cklt^#(#LT)

→

(96)

originates from

#cklt(#LT)

→

#true

(24)

#compare^#(#0,#0)

→

(97)

originates from

#compare(#0,#0)

→

#EQ

(25)

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

→

(99)

originates from

#compare(#0,#neg(z0))

→

#GT

(98)

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

→

(101)

originates from

#compare(#0,#pos(z0))

→

#LT

(100)

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

→

c10

(103)

originates from

#compare(#0,#s(z0))

→

#LT

(102)

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

→

c11

(105)

originates from

#compare(#neg(z0),#0)

→

#LT

(104)

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

→

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

(107)

originates from

#compare(#neg(z0),#neg(z1))

→

#compare(z1,z0)

(106)

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

→

c13

(109)

originates from

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

→

#LT

(108)

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

→

c14

(111)

originates from

#compare(#pos(z0),#0)

→

#GT

(110)

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

→

c15

(113)

originates from

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

→

#GT

(112)

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

→

c16(#compare^#(z0,z1))

(115)

originates from

#compare(#pos(z0),#pos(z1))

→

#compare(z0,z1)

(114)

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

→

c17

(117)

originates from

#compare(#s(z0),#0)

→

#GT

(116)

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

→

c18(#compare^#(z0,z1))

(119)

originates from

#compare(#s(z0),#s(z1))

→

#compare(z0,z1)

(118)

#eq^#(#0,#0)

→

c19

(120)

originates from

#eq(#0,#0)

→

#true

(37)

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

→

c20

(122)

originates from

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

→

#false

(121)

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

→

c21

(124)

originates from

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

→

#false

(123)

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

→

c22

(126)

originates from

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

→

#false

(125)

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

→

c23

(128)

originates from

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

→

#false

(127)

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

→

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

(130)

originates from

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

→

#eq(z0,z1)

(129)

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

→

c25

(132)

originates from

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

→

#false

(131)

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

→

c26

(134)

originates from

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

→

#false

(133)

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

→

c27

(136)

originates from

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

→

#false

(135)

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

→

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

(138)

originates from

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

→

#eq(z0,z1)

(137)

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

→

c29

(140)

originates from

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

→

#false

(139)

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

→

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

(142)

originates from

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

→

#eq(z0,z1)

(141)

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

→

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

(144)

originates from

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

→

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

(143)

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

→

c32

(146)

originates from

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

→

#false

(145)

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

→

c33

(148)

originates from

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

→

#false

(147)

#eq^#(nil,nil)

→

c34

(149)

originates from

#eq(nil,nil)

→

#true

(52)

#or^#(#false,#false)

→

c35

(150)

originates from

#or(#false,#false)

→

#false

(53)

#or^#(#false,#true)

→

c36

(151)

originates from

#or(#false,#true)

→

#true

(54)

#or^#(#true,#false)

→

c37

(152)

originates from

#or(#true,#false)

→

#true

(55)

#or^#(#true,#true)

→

c38

(153)

originates from

#or(#true,#true)

→

#true

(56)

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

#and^#(#false,#false)

#and^#(#false,#true)

#and^#(#true,#false)

#and^#(#true,#true)

#cklt^#(#EQ)

#cklt^#(#GT)

#cklt^#(#LT)

#compare^#(#0,#0)

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

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

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

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

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

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

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

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

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

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

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

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

#or^#(#false,#false)

#or^#(#false,#true)

#or^#(#true,#false)

#or^#(#true,#true)

#equal^#(z0,z1)

#less^#(z0,z1)

and^#(z0,z1)

insert^#(z0,z1)

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

insert#1^#(nil,z0)

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

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

isortlist^#(z0)

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

isortlist#1^#(nil)

leq^#(z0,z1)

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

leq#1^#(nil,z0)

leq#2^#(::(z0,z1),z2,z3)

leq#2^#(nil,z0,z1)

or^#(z0,z1)

1.1 Rule Shifting

The rules

isortlist#1^#(nil)

→

c49

(77)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and(x₁, x₂)]	=	1
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 + 1 · x₁
[isortlist#1(x₁)]	=	1 + 1 · x₁
[leq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[leq#1(x₁, x₂)]	=	1 + 1 · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[or(x₁, x₂)]	=	1 + 1 · x₁
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	1 + 1 · x₁
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[isortlist^#(x₁)]	=	1
[isortlist#1^#(x₁)]	=	1
[leq^#(x₁, x₂)]	=	0
[leq#1^#(x₁, x₂)]	=	0
[leq#2^#(x₁, x₂, x₃)]	=	0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	0
[nil]	=	1
[#0]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#pos(x₁)]	=	1 + 1 · x₁
[#s(x₁)]	=	1 + 1 · x₁
[#EQ]	=	1
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)

1.1.1 Rule Shifting

The rules

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

→

c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))

(76)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and(x₁, x₂)]	=	1
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₂
[insert#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 + 1 · x₁
[isortlist#1(x₁)]	=	1
[leq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[leq#1(x₁, x₂)]	=	1 + 1 · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[or(x₁, x₂)]	=	1 + 1 · x₁
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	1 + 1 · x₂
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[isortlist^#(x₁)]	=	1 · x₁ + 0
[isortlist#1^#(x₁)]	=	1 · x₁ + 0
[leq^#(x₁, x₂)]	=	0
[leq#1^#(x₁, x₂)]	=	0
[leq#2^#(x₁, x₂, x₃)]	=	0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#0]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#pos(x₁)]	=	1 + 1 · x₁
[#s(x₁)]	=	1 + 1 · x₁
[#EQ]	=	1
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)

1.1.1.1 Rule Shifting

The rules

isortlist^#(z0)

→

c47(isortlist#1^#(z0))

(74)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and(x₁, x₂)]	=	1
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 + 1 · x₁
[isortlist#1(x₁)]	=	1 + 1 · x₁
[leq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[leq#1(x₁, x₂)]	=	1 + 1 · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[or(x₁, x₂)]	=	1 + 1 · x₁
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	1 + 1 · x₁
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[isortlist^#(x₁)]	=	1 + 1 · x₁
[isortlist#1^#(x₁)]	=	1 · x₁ + 0
[leq^#(x₁, x₂)]	=	0
[leq#1^#(x₁, x₂)]	=	0
[leq#2^#(x₁, x₂, x₃)]	=	0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	1
[#0]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#pos(x₁)]	=	1 + 1 · x₁
[#s(x₁)]	=	1 + 1 · x₁
[#EQ]	=	1
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)

1.1.1.1.1 Rule Shifting

The rules

insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[and(x₁, x₂)]	=	1
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₂
[insert#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 + 1 · x₁
[isortlist#1(x₁)]	=	1
[leq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[leq#1(x₁, x₂)]	=	1 + 1 · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[or(x₁, x₂)]	=	1 + 1 · x₁
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	1 + 1 · x₂
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	1 + 1 · x₁
[insert#1^#(x₁, x₂)]	=	1 + 1 · x₂
[insert#2^#(x₁,...,x₄)]	=	1 + 1 · x₂
[isortlist^#(x₁)]	=	1 + 1 · x₁
[isortlist#1^#(x₁)]	=	1 + 1 · x₁
[leq^#(x₁, x₂)]	=	0
[leq#1^#(x₁, x₂)]	=	0
[leq#2^#(x₁, x₂, x₃)]	=	0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	1
[#0]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#pos(x₁)]	=	1 + 1 · x₁
[#s(x₁)]	=	1 + 1 · x₁
[#EQ]	=	1
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)

1.1.1.1.1.1 Rule Shifting

The rules

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

→

c51(leq#2^#(z2,z0,z1))

(81)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 · x₁ + 0
[isortlist#1(x₁)]	=	1 · x₁ + 0
[leq(x₁, x₂)]	=	0
[leq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[insert#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[insert#2^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[isortlist^#(x₁)]	=	1 · x₁ · x₁ + 0
[isortlist#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[leq^#(x₁, x₂)]	=	2 · x₁ + 0
[leq#1^#(x₁, x₂)]	=	2 · x₁ + 0
[leq#2^#(x₁, x₂, x₃)]	=	2 · x₃ + 0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	2
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
isortlist#1(nil)	→	nil	(11)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(nil,z0)	→	::(z0,nil)	(67)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)

1.1.1.1.1.1.1 Rule Shifting

The rules

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

→

c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))

(66)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₄
[isortlist(x₁)]	=	1 · x₁ + 0
[isortlist#1(x₁)]	=	1 · x₁ + 0
[leq(x₁, x₂)]	=	0
[leq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	2 · x₂ + 0
[insert#1^#(x₁, x₂)]	=	2 · x₁ + 0
[insert#2^#(x₁,...,x₄)]	=	2 · x₄ + 0
[isortlist^#(x₁)]	=	1 · x₁ · x₁ + 0
[isortlist#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[leq^#(x₁, x₂)]	=	0
[leq#1^#(x₁, x₂)]	=	0
[leq#2^#(x₁, x₂, x₃)]	=	0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	2
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
isortlist#1(nil)	→	nil	(11)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(nil,z0)	→	::(z0,nil)	(67)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 · x₁ + 0
[isortlist#1(x₁)]	=	1 · x₁ + 0
[leq(x₁, x₂)]	=	0
[leq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	1 · x₂ + 0
[insert#1^#(x₁, x₂)]	=	1 · x₁ + 0
[insert#2^#(x₁,...,x₄)]	=	1 · x₄ + 0
[isortlist^#(x₁)]	=	1 · x₁ · x₁ + 0
[isortlist#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[leq^#(x₁, x₂)]	=	1 · x₂ + 0
[leq#1^#(x₁, x₂)]	=	1 · x₂ + 0
[leq#2^#(x₁, x₂, x₃)]	=	1 · x₁ + 0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	1
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	1
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
isortlist#1(nil)	→	nil	(11)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(nil,z0)	→	::(z0,nil)	(67)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

or^#(z0,z1)

→

c55(#or^#(z0,z1))

(89)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 · x₁ + 0
[isortlist#1(x₁)]	=	1 · x₁ + 0
[leq(x₁, x₂)]	=	0
[leq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[insert#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[insert#2^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[isortlist^#(x₁)]	=	2 + 1 · x₁ · x₁
[isortlist#1^#(x₁)]	=	1 + 1 · x₁ · x₁
[leq^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[leq#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[leq#2^#(x₁, x₂, x₃)]	=	2 · x₁ + 0 + 2 · x₁ · x₃
[or^#(x₁, x₂)]	=	1
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	2
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
isortlist#1(nil)	→	nil	(11)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(nil,z0)	→	::(z0,nil)	(67)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

leq#1^#(nil,z0)

→

c52

(83)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	2 · x₁ + 0
[isortlist#1(x₁)]	=	2 · x₁ + 0
[leq(x₁, x₂)]	=	0
[leq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	2
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[insert#1^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[insert#2^#(x₁,...,x₄)]	=	1 · x₂ · x₄ + 0
[isortlist^#(x₁)]	=	1 · x₁ · x₁ + 0
[isortlist#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[leq^#(x₁, x₂)]	=	1 · x₁ + 0
[leq#1^#(x₁, x₂)]	=	1 · x₁ + 0
[leq#2^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	2
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	2
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
isortlist#1(nil)	→	nil	(11)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(nil,z0)	→	::(z0,nil)	(67)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

insert^#(z0,z1)

→

c42(insert#1^#(z1,z0))

(64)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₄
[isortlist(x₁)]	=	1 · x₁ + 0
[isortlist#1(x₁)]	=	1 · x₁ + 0
[leq(x₁, x₂)]	=	0
[leq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	2
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	1 + 1 · x₂
[insert#1^#(x₁, x₂)]	=	1 · x₁ + 0
[insert#2^#(x₁,...,x₄)]	=	1 + 1 · x₄
[isortlist^#(x₁)]	=	1 · x₁ · x₁ + 0
[isortlist#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[leq^#(x₁, x₂)]	=	0
[leq#1^#(x₁, x₂)]	=	0
[leq#2^#(x₁, x₂, x₃)]	=	0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	2
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
isortlist#1(nil)	→	nil	(11)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(nil,z0)	→	::(z0,nil)	(67)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 · x₁ + 0
[isortlist#1(x₁)]	=	1 · x₁ + 0
[leq(x₁, x₂)]	=	0
[leq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	2
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	2
[#less^#(x₁, x₂)]	=	1
[and^#(x₁, x₂)]	=	1
[insert^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[insert#1^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[insert#2^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[isortlist^#(x₁)]	=	2 · x₁ + 0 + 1 · x₁ · x₁
[isortlist#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[leq^#(x₁, x₂)]	=	2 · x₁ + 0 + 2 · x₁ · x₂
[leq#1^#(x₁, x₂)]	=	2 · x₁ + 0 + 2 · x₁ · x₂
[leq#2^#(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 2 · x₁ · x₃
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	2
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
isortlist#1(nil)	→	nil	(11)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(nil,z0)	→	::(z0,nil)	(67)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

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

→

c45(insert^#(z0,z2))

(70)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 · x₁ + 0
[isortlist#1(x₁)]	=	1 · x₁ + 0
[leq(x₁, x₂)]	=	0
[leq#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[leq#2(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	2
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	1 · x₂ + 0
[insert#1^#(x₁, x₂)]	=	1 · x₁ + 0
[insert#2^#(x₁,...,x₄)]	=	1 + 1 · x₄
[isortlist^#(x₁)]	=	2 · x₁ + 0 + 1 · x₁ · x₁
[isortlist#1^#(x₁)]	=	2 · x₁ + 0 + 1 · x₁ · x₁
[leq^#(x₁, x₂)]	=	0
[leq#1^#(x₁, x₂)]	=	0
[leq#2^#(x₁, x₂, x₃)]	=	0
[or^#(x₁, x₂)]	=	0
[#false]	=	0
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	2
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
isortlist#1(nil)	→	nil	(11)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(nil,z0)	→	::(z0,nil)	(67)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

leq^#(z0,z1)

→

c50(leq#1^#(z0,z1))

(79)

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]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14]	=	0
[c15]	=	0
[c16(x₁)]	=	1 · x₁ + 0
[c17]	=	0
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[c26]	=	0
[c27]	=	0
[c28(x₁)]	=	1 · x₁ + 0
[c29]	=	0
[c30(x₁)]	=	1 · x₁ + 0
[c31(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c32]	=	0
[c33]	=	0
[c34]	=	0
[c35]	=	0
[c36]	=	0
[c37]	=	0
[c38]	=	0
[c39(x₁)]	=	1 · x₁ + 0
[c40(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c41(x₁)]	=	1 · x₁ + 0
[c42(x₁)]	=	1 · x₁ + 0
[c43(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c44]	=	0
[c45(x₁)]	=	1 · x₁ + 0
[c46]	=	0
[c47(x₁)]	=	1 · x₁ + 0
[c48(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c49]	=	0
[c50(x₁)]	=	1 · x₁ + 0
[c51(x₁)]	=	1 · x₁ + 0
[c52]	=	0
[c53(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₅
[c54]	=	0
[c55(x₁)]	=	1 · x₁ + 0
[#equal(x₁, x₂)]	=	0
[#less(x₁, x₂)]	=	0
[and(x₁, x₂)]	=	0
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₂ + 1 · x₃ + 1 · x₄
[isortlist(x₁)]	=	1 · x₁ + 0
[isortlist#1(x₁)]	=	1 · x₁ + 0
[leq(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[leq#1(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[leq#2(x₁, x₂, x₃)]	=	1 · x₁ + 0
[or(x₁, x₂)]	=	1
[#and(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1
[#compare(x₁, x₂)]	=	0
[#eq(x₁, x₂)]	=	0
[#or(x₁, x₂)]	=	1
[#and^#(x₁, x₂)]	=	0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#eq^#(x₁, x₂)]	=	0
[#or^#(x₁, x₂)]	=	0
[#equal^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[insert^#(x₁, x₂)]	=	1 + 1 · x₁ · x₂
[insert#1^#(x₁, x₂)]	=	1 + 1 · x₁ · x₂
[insert#2^#(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ · x₄
[isortlist^#(x₁)]	=	2 · x₁ · x₁ + 0
[isortlist#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[leq^#(x₁, x₂)]	=	1 + 1 · x₁
[leq#1^#(x₁, x₂)]	=	1 · x₁ + 0
[leq#2^#(x₁, x₂, x₃)]	=	1 + 1 · x₃
[or^#(x₁, x₂)]	=	0
[#false]	=	1
[#true]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	1
[#0]	=	0
[#neg(x₁)]	=	0
[#pos(x₁)]	=	0
[#s(x₁)]	=	0
[#EQ]	=	2
[#GT]	=	1
[#LT]	=	1

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

#and^#(#false,#false)	→	c	(90)
#and^#(#false,#true)	→	c1	(91)
#and^#(#true,#false)	→	c2	(92)
#and^#(#true,#true)	→	c3	(93)
#cklt^#(#EQ)	→	c4	(94)
#cklt^#(#GT)	→	c5	(95)
#cklt^#(#LT)	→	c6	(96)
#compare^#(#0,#0)	→	c7	(97)
#compare^#(#0,#neg(z0))	→	c8	(99)
#compare^#(#0,#pos(z0))	→	c9	(101)
#compare^#(#0,#s(z0))	→	c10	(103)
#compare^#(#neg(z0),#0)	→	c11	(105)
#compare^#(#neg(z0),#neg(z1))	→	c12(#compare^#(z1,z0))	(107)
#compare^#(#neg(z0),#pos(z1))	→	c13	(109)
#compare^#(#pos(z0),#0)	→	c14	(111)
#compare^#(#pos(z0),#neg(z1))	→	c15	(113)
#compare^#(#pos(z0),#pos(z1))	→	c16(#compare^#(z0,z1))	(115)
#compare^#(#s(z0),#0)	→	c17	(117)
#compare^#(#s(z0),#s(z1))	→	c18(#compare^#(z0,z1))	(119)
#eq^#(#0,#0)	→	c19	(120)
#eq^#(#0,#neg(z0))	→	c20	(122)
#eq^#(#0,#pos(z0))	→	c21	(124)
#eq^#(#0,#s(z0))	→	c22	(126)
#eq^#(#neg(z0),#0)	→	c23	(128)
#eq^#(#neg(z0),#neg(z1))	→	c24(#eq^#(z0,z1))	(130)
#eq^#(#neg(z0),#pos(z1))	→	c25	(132)
#eq^#(#pos(z0),#0)	→	c26	(134)
#eq^#(#pos(z0),#neg(z1))	→	c27	(136)
#eq^#(#pos(z0),#pos(z1))	→	c28(#eq^#(z0,z1))	(138)
#eq^#(#s(z0),#0)	→	c29	(140)
#eq^#(#s(z0),#s(z1))	→	c30(#eq^#(z0,z1))	(142)
#eq^#(::(z0,z1),::(z2,z3))	→	c31(#and^#(#eq(z0,z2),#eq(z1,z3)),#eq^#(z0,z2),#eq^#(z1,z3))	(144)
#eq^#(::(z0,z1),nil)	→	c32	(146)
#eq^#(nil,::(z0,z1))	→	c33	(148)
#eq^#(nil,nil)	→	c34	(149)
#or^#(#false,#false)	→	c35	(150)
#or^#(#false,#true)	→	c36	(151)
#or^#(#true,#false)	→	c37	(152)
#or^#(#true,#true)	→	c38	(153)
#equal^#(z0,z1)	→	c39(#eq^#(z0,z1))	(58)
#less^#(z0,z1)	→	c40(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(60)
and^#(z0,z1)	→	c41(#and^#(z0,z1))	(62)
insert^#(z0,z1)	→	c42(insert#1^#(z1,z0))	(64)
insert#1^#(::(z0,z1),z2)	→	c43(insert#2^#(leq(z2,z0),z2,z0,z1),leq^#(z2,z0))	(66)
insert#1^#(nil,z0)	→	c44	(68)
insert#2^#(#false,z0,z1,z2)	→	c45(insert^#(z0,z2))	(70)
insert#2^#(#true,z0,z1,z2)	→	c46	(72)
isortlist^#(z0)	→	c47(isortlist#1^#(z0))	(74)
isortlist#1^#(::(z0,z1))	→	c48(insert^#(z0,isortlist(z1)),isortlist^#(z1))	(76)
isortlist#1^#(nil)	→	c49	(77)
leq^#(z0,z1)	→	c50(leq#1^#(z0,z1))	(79)
leq#1^#(::(z0,z1),z2)	→	c51(leq#2^#(z2,z0,z1))	(81)
leq#1^#(nil,z0)	→	c52	(83)
leq#2^#(::(z0,z1),z2,z3)	→	c53(or^#(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1))),#less^#(z2,z0),and^#(#equal(z2,z0),leq(z3,z1)),#equal^#(z2,z0),leq^#(z3,z1))	(85)
leq#2^#(nil,z0,z1)	→	c54	(87)
or^#(z0,z1)	→	c55(#or^#(z0,z1))	(89)
#or(#false,#true)	→	#true	(54)
#or(#true,#false)	→	#true	(55)
#or(#true,#true)	→	#true	(56)
leq#1(nil,z0)	→	#true	(82)
#or(#false,#false)	→	#false	(53)
isortlist#1(nil)	→	nil	(11)
leq(z0,z1)	→	leq#1(z0,z1)	(78)
insert#2(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(71)
or(z0,z1)	→	#or(z0,z1)	(88)
leq#1(::(z0,z1),z2)	→	leq#2(z2,z0,z1)	(80)
isortlist#1(::(z0,z1))	→	insert(z0,isortlist(z1))	(75)
insert#1(::(z0,z1),z2)	→	insert#2(leq(z2,z0),z2,z0,z1)	(65)
leq#2(nil,z0,z1)	→	#false	(86)
insert#2(#false,z0,z1,z2)	→	::(z1,insert(z0,z2))	(69)
leq#2(::(z0,z1),z2,z3)	→	or(#less(z2,z0),and(#equal(z2,z0),leq(z3,z1)))	(84)
insert(z0,z1)	→	insert#1(z1,z0)	(63)
isortlist(z0)	→	isortlist#1(z0)	(73)
insert#1(nil,z0)	→	::(z0,nil)	(67)

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