Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/raML/flatten.raml)

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

#less(@x,@y)	→	#cklt(#compare(@x,@y))	(1)
append(@l1,@l2)	→	append#1(@l1,@l2)	(2)
append#1(::(@x,@xs),@l2)	→	::(@x,append(@xs,@l2))	(3)
append#1(nil,@l2)	→	@l2	(4)
flatten(@t)	→	flatten#1(@t)	(5)
flatten#1(leaf)	→	nil	(6)
flatten#1(node(@l,@t1,@t2))	→	append(@l,append(flatten(@t1),flatten(@t2)))	(7)
flattensort(@t)	→	insertionsort(flatten(@t))	(8)
insert(@x,@l)	→	insert#1(@l,@x)	(9)
insert#1(::(@y,@ys),@x)	→	insert#2(#less(@y,@x),@x,@y,@ys)	(10)
insert#1(nil,@x)	→	::(@x,nil)	(11)
insert#2(#false,@x,@y,@ys)	→	::(@x,::(@y,@ys))	(12)
insert#2(#true,@x,@y,@ys)	→	::(@y,insert(@x,@ys))	(13)
insertionsort(@l)	→	insertionsort#1(@l)	(14)
insertionsort#1(::(@x,@xs))	→	insert(@x,insertionsort(@xs))	(15)
insertionsort#1(nil)	→	nil	(16)

and S is the following TRS.

#cklt(#EQ)	→	#false	(17)
#cklt(#GT)	→	#false	(18)
#cklt(#LT)	→	#true	(19)
#compare(#0,#0)	→	#EQ	(20)
#compare(#0,#neg(@y))	→	#GT	(21)
#compare(#0,#pos(@y))	→	#LT	(22)
#compare(#0,#s(@y))	→	#LT	(23)
#compare(#neg(@x),#0)	→	#LT	(24)
#compare(#neg(@x),#neg(@y))	→	#compare(@y,@x)	(25)
#compare(#neg(@x),#pos(@y))	→	#LT	(26)
#compare(#pos(@x),#0)	→	#GT	(27)
#compare(#pos(@x),#neg(@y))	→	#GT	(28)
#compare(#pos(@x),#pos(@y))	→	#compare(@x,@y)	(29)
#compare(#s(@x),#0)	→	#GT	(30)
#compare(#s(@x),#s(@y))	→	#compare(@x,@y)	(31)

The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n²).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:

#less^#(z0,z1)

→

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

(33)

originates from

#less(z0,z1)

→

#cklt(#compare(z0,z1))

(32)

append^#(z0,z1)

→

c16(append#1^#(z0,z1))

(35)

originates from

append(z0,z1)

→

append#1(z0,z1)

(34)

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

→

c17(append^#(z1,z2))

(37)

originates from

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

→

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

(36)

append#1^#(nil,z0)

→

c18

(39)

originates from

append#1(nil,z0)

→

(38)

flatten^#(z0)

→

c19(flatten#1^#(z0))

(41)

originates from

flatten(z0)

→

flatten#1(z0)

(40)

flatten#1^#(leaf)

→

c20

(42)

originates from

flatten#1(leaf)

→

nil

(6)

flatten#1^#(node(z0,z1,z2))

→

c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))

(44)

originates from

flatten#1(node(z0,z1,z2))

→

append(z0,append(flatten(z1),flatten(z2)))

(43)

flattensort^#(z0)

→

c22(insertionsort^#(flatten(z0)),flatten^#(z0))

(46)

originates from

flattensort(z0)

→

insertionsort(flatten(z0))

(45)

insert^#(z0,z1)

→

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

(48)

originates from

insert(z0,z1)

→

insert#1(z1,z0)

(47)

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

→

c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))

(50)

originates from

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

→

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

(49)

insert#1^#(nil,z0)

→

c25

(52)

originates from

insert#1(nil,z0)

→

::(z0,nil)

(51)

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

→

c26

(54)

originates from

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

→

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

(53)

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

→

c27(insert^#(z0,z2))

(56)

originates from

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

→

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

(55)

insertionsort^#(z0)

→

c28(insertionsort#1^#(z0))

(58)

originates from

insertionsort(z0)

→

insertionsort#1(z0)

(57)

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

→

c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))

(60)

originates from

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

→

insert(z0,insertionsort(z1))

(59)

insertionsort#1^#(nil)

→

c30

(61)

originates from

insertionsort#1(nil)

→

nil

(16)

#cklt^#(#EQ)

→

(62)

originates from

#cklt(#EQ)

→

#false

(17)

#cklt^#(#GT)

→

(63)

originates from

#cklt(#GT)

→

#false

(18)

#cklt^#(#LT)

→

(64)

originates from

#cklt(#LT)

→

#true

(19)

#compare^#(#0,#0)

→

(65)

originates from

#compare(#0,#0)

→

#EQ

(20)

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

→

(67)

originates from

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

→

#GT

(66)

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

→

(69)

originates from

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

→

#LT

(68)

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

→

(71)

originates from

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

→

#LT

(70)

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

→

(73)

originates from

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

→

#LT

(72)

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

→

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

(75)

originates from

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

→

#compare(z1,z0)

(74)

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

→

(77)

originates from

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

→

#LT

(76)

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

→

c10

(79)

originates from

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

→

#GT

(78)

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

→

c11

(81)

originates from

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

→

#GT

(80)

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

→

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

(83)

originates from

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

→

#compare(z0,z1)

(82)

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

→

c13

(85)

originates from

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

→

#GT

(84)

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

→

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

(87)

originates from

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

→

#compare(z0,z1)

(86)

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

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

#less^#(z0,z1)

append^#(z0,z1)

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

append#1^#(nil,z0)

flatten^#(z0)

flatten#1^#(leaf)

flatten#1^#(node(z0,z1,z2))

flattensort^#(z0)

insert^#(z0,z1)

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

insert#1^#(nil,z0)

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

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

insertionsort^#(z0)

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

insertionsort#1^#(nil)

1.1 Usable Rules

We remove the following rules since they are not usable.

flattensort(z0)

→

insertionsort(flatten(z0))

(45)

1.1.1 Rule Shifting

The rules

flatten#1^#(leaf)	→	c20	(42)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[append(x₁, x₂)]	=	1 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 + 1 · x₁
[append#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#cklt(x₁)]	=	1 + 1 · x₁
[insertionsort(x₁)]	=	1 + 1 · x₁
[insertionsort#1(x₁)]	=	1 + 1 · x₁
[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₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	1 · x₁ + 0
[flatten#1^#(x₁)]	=	1 · x₁ + 0
[flattensort^#(x₁)]	=	1 + 1 · x₁
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[insertionsort^#(x₁)]	=	0
[insertionsort#1^#(x₁)]	=	0
[::(x₁, x₂)]	=	1 · x₁ + 0
[nil]	=	0
[#false]	=	1
[#true]	=	1
[#0]	=	1
[#EQ]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#GT]	=	1
[#pos(x₁)]	=	1 + 1 · x₁
[#LT]	=	1
[#s(x₁)]	=	1 + 1 · x₁
[leaf]	=	1
[node(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)

1.1.1.1 Rule Shifting

The rules

flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
insertionsort#1^#(nil)	→	c30	(61)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[append(x₁, x₂)]	=	1 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 + 1 · x₁
[append#1(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#cklt(x₁)]	=	1 + 1 · x₁
[insertionsort(x₁)]	=	1 + 1 · x₁
[insertionsort#1(x₁)]	=	1 + 1 · x₁
[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₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	1 · x₁ + 0
[flatten#1^#(x₁)]	=	1 · x₁ + 0
[flattensort^#(x₁)]	=	1 + 1 · x₁
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[insertionsort^#(x₁)]	=	1
[insertionsort#1^#(x₁)]	=	1
[::(x₁, x₂)]	=	1 · x₁ + 0
[nil]	=	0
[#false]	=	1
[#true]	=	1
[#0]	=	1
[#EQ]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#GT]	=	1
[#pos(x₁)]	=	1 + 1 · x₁
[#LT]	=	1
[#s(x₁)]	=	1 + 1 · x₁
[leaf]	=	1
[node(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)

1.1.1.1.1 Rule Shifting

The rules

append#1^#(nil,z0)

→

c18

(39)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[append(x₁, x₂)]	=	1 · x₂ + 0
[flatten(x₁)]	=	1
[flatten#1(x₁)]	=	1
[append#1(x₁, x₂)]	=	1 · x₂ + 0
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#cklt(x₁)]	=	1 + 1 · x₁
[insertionsort(x₁)]	=	1 + 1 · x₁
[insertionsort#1(x₁)]	=	1 + 1 · x₁
[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₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	1 · x₁ + 0
[append#1^#(x₁, x₂)]	=	1 · x₁ + 0
[flatten^#(x₁)]	=	1 · x₁ + 0
[flatten#1^#(x₁)]	=	1 · x₁ + 0
[flattensort^#(x₁)]	=	1 + 1 · x₁
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[insertionsort^#(x₁)]	=	1 · x₁ + 0
[insertionsort#1^#(x₁)]	=	1 · x₁ + 0
[::(x₁, x₂)]	=	1 · x₂ + 0
[nil]	=	1
[#false]	=	1
[#true]	=	1
[#0]	=	1
[#EQ]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#GT]	=	1
[#pos(x₁)]	=	1 + 1 · x₁
[#LT]	=	1
[#s(x₁)]	=	1 + 1 · x₁
[leaf]	=	1
[node(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

1.1.1.1.1.1 Rule Shifting

The rules

insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[append(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 · x₁ + 0
[append#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#cklt(x₁)]	=	1 + 1 · x₁
[insertionsort(x₁)]	=	1 + 1 · x₁
[insertionsort#1(x₁)]	=	1 + 1 · x₁
[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₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	0
[flatten#1^#(x₁)]	=	0
[flattensort^#(x₁)]	=	1 · x₁ + 0
[insert^#(x₁, x₂)]	=	1 + 1 · x₁
[insert#1^#(x₁, x₂)]	=	1 + 1 · x₂
[insert#2^#(x₁,...,x₄)]	=	1 + 1 · x₂
[insertionsort^#(x₁)]	=	1 · x₁ + 0
[insertionsort#1^#(x₁)]	=	1 · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	1
[#false]	=	1
[#true]	=	1
[#0]	=	1
[#EQ]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#GT]	=	1
[#pos(x₁)]	=	1 + 1 · x₁
[#LT]	=	1
[#s(x₁)]	=	1 + 1 · x₁
[leaf]	=	1
[node(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

1.1.1.1.1.1.1 Rule Shifting

The rules

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

→

c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))

(60)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[append(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 · x₁ + 0
[append#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#cklt(x₁)]	=	1 + 1 · x₁
[insertionsort(x₁)]	=	1 + 1 · x₁
[insertionsort#1(x₁)]	=	1 + 1 · x₁
[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₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	0
[flatten#1^#(x₁)]	=	0
[flattensort^#(x₁)]	=	1 · x₁ + 0
[insert^#(x₁, x₂)]	=	1 · x₁ + 0
[insert#1^#(x₁, x₂)]	=	1 · x₂ + 0
[insert#2^#(x₁,...,x₄)]	=	1 · x₂ + 0
[insertionsort^#(x₁)]	=	1 · x₁ + 0
[insertionsort#1^#(x₁)]	=	1 · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	1
[#false]	=	1
[#true]	=	1
[#0]	=	1
[#EQ]	=	1
[#neg(x₁)]	=	1 + 1 · x₁
[#GT]	=	1
[#pos(x₁)]	=	1 + 1 · x₁
[#LT]	=	1
[#s(x₁)]	=	1 + 1 · x₁
[leaf]	=	1
[node(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

insertionsort^#(z0)

→

c28(insertionsort#1^#(z0))

(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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	0
[append(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 · x₁ + 0
[append#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#cklt(x₁)]	=	1 + 1 · x₁
[insertionsort(x₁)]	=	1 + 1 · x₁
[insertionsort#1(x₁)]	=	1 + 1 · x₁
[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₄
[#cklt^#(x₁)]	=	1 · x₁ + 0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	0
[flatten#1^#(x₁)]	=	0
[flattensort^#(x₁)]	=	1 + 1 · x₁
[insert^#(x₁, x₂)]	=	1 · x₁ + 0
[insert#1^#(x₁, x₂)]	=	1 · x₂ + 0
[insert#2^#(x₁,...,x₄)]	=	1 · x₂ + 0
[insertionsort^#(x₁)]	=	1 + 1 · x₁
[insertionsort#1^#(x₁)]	=	1 · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	1
[#false]	=	1
[#true]	=	1
[#0]	=	1
[#EQ]	=	0
[#neg(x₁)]	=	1 + 1 · x₁
[#GT]	=	0
[#pos(x₁)]	=	1 + 1 · x₁
[#LT]	=	0
[#s(x₁)]	=	1 + 1 · x₁
[leaf]	=	1
[node(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
#compare(#0,#neg(z0))	→	#GT	(66)
#compare(#0,#pos(z0))	→	#LT	(68)
#compare(#0,#s(z0))	→	#LT	(70)
#compare(#pos(z0),#0)	→	#GT	(78)
#compare(#neg(z0),#neg(z1))	→	#compare(z1,z0)	(74)
#compare(#s(z0),#s(z1))	→	#compare(z0,z1)	(86)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
#compare(#0,#0)	→	#EQ	(20)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
#compare(#s(z0),#0)	→	#GT	(84)
#compare(#neg(z0),#pos(z1))	→	#LT	(76)
#compare(#neg(z0),#0)	→	#LT	(72)
#compare(#pos(z0),#pos(z1))	→	#compare(z0,z1)	(82)
#compare(#pos(z0),#neg(z1))	→	#GT	(80)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

flatten^#(z0)

→

c19(flatten#1^#(z0))

(41)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[append(x₁, x₂)]	=	0
[flatten(x₁)]	=	0
[flatten#1(x₁)]	=	3 + 3 · x₁
[append#1(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	3
[insertionsort(x₁)]	=	3 + 2 · x₁
[insertionsort#1(x₁)]	=	3 + 3 · x₁
[insert(x₁, x₂)]	=	3 + 3 · x₁
[insert#1(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[insert#2(x₁,...,x₄)]	=	3 + 3 · x₂ + 3 · x₃ + 3 · x₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	2 + 1 · x₁
[flatten#1^#(x₁)]	=	1 + 1 · x₁
[flattensort^#(x₁)]	=	3 + 1 · x₁
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[insertionsort^#(x₁)]	=	0
[insertionsort#1^#(x₁)]	=	0
[::(x₁, x₂)]	=	0
[nil]	=	0
[#false]	=	3
[#true]	=	0
[#0]	=	0
[#EQ]	=	3
[#neg(x₁)]	=	1 · x₁ + 0
[#GT]	=	3
[#pos(x₁)]	=	1 · x₁ + 0
[#LT]	=	3
[#s(x₁)]	=	1 · x₁ + 0
[leaf]	=	3
[node(x₁, x₂, x₃)]	=	3 + 1 · x₁ + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

append^#(z0,z1)

→

c16(append#1^#(z0,z1))

(35)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	0
[append(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 · x₁ + 0
[append#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[insertionsort(x₁)]	=	0
[insertionsort#1(x₁)]	=	1
[insert(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₁ · x₁
[insert#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[insert#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₄ · x₄ + 1 · x₃ · x₄ + 1 · x₂ · x₄ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	1 + 1 · x₁
[append#1^#(x₁, x₂)]	=	1 · x₁ + 0
[flatten^#(x₁)]	=	2 · x₁ · x₁ + 0
[flatten#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[flattensort^#(x₁)]	=	1 + 1 · x₁ + 2 · x₁ · x₁
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[insertionsort^#(x₁)]	=	0
[insertionsort#1^#(x₁)]	=	0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#false]	=	1
[#true]	=	0
[#0]	=	2
[#EQ]	=	2
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	0
[#LT]	=	1
[#s(x₁)]	=	0
[leaf]	=	0
[node(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	0
[append(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 · x₁ + 0
[append#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[insertionsort(x₁)]	=	1 · x₁ + 0
[insertionsort#1(x₁)]	=	1 · x₁ + 0
[insert(x₁, x₂)]	=	1 + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	1
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	0
[flatten#1^#(x₁)]	=	0
[flattensort^#(x₁)]	=	1 + 2 · x₁ · x₁
[insert^#(x₁, x₂)]	=	2 · x₂ + 0
[insert#1^#(x₁, x₂)]	=	2 · x₁ + 0
[insert#2^#(x₁,...,x₄)]	=	2 · x₄ + 0
[insertionsort^#(x₁)]	=	1 · x₁ · x₁ + 0
[insertionsort#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#EQ]	=	2
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	0
[#LT]	=	1
[#s(x₁)]	=	0
[leaf]	=	0
[node(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
insert#2(#false,z0,z1,z2)	→	::(z0,::(z1,z2))	(53)
insert#1(::(z0,z1),z2)	→	insert#2(#less(z0,z2),z2,z0,z1)	(49)
insert#2(#true,z0,z1,z2)	→	::(z1,insert(z0,z2))	(55)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
insertionsort#1(nil)	→	nil	(16)
insert(z0,z1)	→	insert#1(z1,z0)	(47)
insertionsort#1(::(z0,z1))	→	insert(z0,insertionsort(z1))	(59)
insert#1(nil,z0)	→	::(z0,nil)	(51)
insertionsort(z0)	→	insertionsort#1(z0)	(57)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

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

→

c17(append^#(z1,z2))

(37)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	0
[append(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[flatten(x₁)]	=	2 · x₁ + 0
[flatten#1(x₁)]	=	2 · x₁ + 0
[append#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[insertionsort(x₁)]	=	0
[insertionsort#1(x₁)]	=	1
[insert(x₁, x₂)]	=	1 + 2 · x₁ + 1 · x₁ · x₁
[insert#1(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₂ · x₂
[insert#2(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄ + 1 · x₄ · x₄ + 1 · x₃ · x₄ + 1 · x₂ · x₄ + 1 · x₃ · x₃ + 1 · x₂ · x₃ + 1 · x₂ · x₂
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	2 · x₁ + 0
[append#1^#(x₁, x₂)]	=	2 · x₁ + 0
[flatten^#(x₁)]	=	1 + 1 · x₁ · x₁
[flatten#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[flattensort^#(x₁)]	=	2 + 2 · x₁ + 2 · x₁ · x₁
[insert^#(x₁, x₂)]	=	0
[insert#1^#(x₁, x₂)]	=	0
[insert#2^#(x₁,...,x₄)]	=	0
[insertionsort^#(x₁)]	=	0
[insertionsort#1^#(x₁)]	=	0
[::(x₁, x₂)]	=	2 + 1 · x₂
[nil]	=	0
[#false]	=	1
[#true]	=	0
[#0]	=	2
[#EQ]	=	2
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	0
[#LT]	=	1
[#s(x₁)]	=	0
[leaf]	=	0
[node(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

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

→

c27(insert^#(z0,z2))

(56)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	0
[append(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 · x₁ + 0
[append#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[insertionsort(x₁)]	=	1 · x₁ + 0
[insertionsort#1(x₁)]	=	1 · 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₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	1
[#less^#(x₁, x₂)]	=	1
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	0
[flatten#1^#(x₁)]	=	0
[flattensort^#(x₁)]	=	1 + 1 · x₁ + 2 · x₁ · x₁
[insert^#(x₁, x₂)]	=	2 · x₂ + 0 + 2 · x₁ · x₂
[insert#1^#(x₁, x₂)]	=	2 · x₁ + 0 + 2 · x₁ · x₂
[insert#2^#(x₁,...,x₄)]	=	1 + 2 · x₄ + 2 · x₂ · x₄
[insertionsort^#(x₁)]	=	1 + 1 · x₁ + 1 · x₁ · x₁
[insertionsort#1^#(x₁)]	=	1 + 1 · x₁ + 1 · x₁ · x₁
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#EQ]	=	2
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	0
[#LT]	=	1
[#s(x₁)]	=	0
[leaf]	=	0
[node(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
insert#2(#false,z0,z1,z2)	→	::(z0,::(z1,z2))	(53)
insert#1(::(z0,z1),z2)	→	insert#2(#less(z0,z2),z2,z0,z1)	(49)
insert#2(#true,z0,z1,z2)	→	::(z1,insert(z0,z2))	(55)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
insertionsort#1(nil)	→	nil	(16)
insert(z0,z1)	→	insert#1(z1,z0)	(47)
insertionsort#1(::(z0,z1))	→	insert(z0,insertionsort(z1))	(59)
insert#1(nil,z0)	→	::(z0,nil)	(51)
insertionsort(z0)	→	insertionsort#1(z0)	(57)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

insert^#(z0,z1)

→

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

(48)

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(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13]	=	0
[c14(x₁)]	=	1 · x₁ + 0
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁)]	=	1 · x₁ + 0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[c21(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃ + 1 · x₄
[c22(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c23(x₁)]	=	1 · x₁ + 0
[c24(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c25]	=	0
[c26]	=	0
[c27(x₁)]	=	1 · x₁ + 0
[c28(x₁)]	=	1 · x₁ + 0
[c29(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c30]	=	0
[#compare(x₁, x₂)]	=	0
[append(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[flatten(x₁)]	=	1 · x₁ + 0
[flatten#1(x₁)]	=	1 · x₁ + 0
[append#1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[insertionsort(x₁)]	=	1 · x₁ + 0
[insertionsort#1(x₁)]	=	1 · x₁ + 0
[insert(x₁, x₂)]	=	1 + 1 · x₂
[insert#1(x₁, x₂)]	=	1 + 1 · x₁
[insert#2(x₁,...,x₄)]	=	2 + 1 · x₄
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[append^#(x₁, x₂)]	=	0
[append#1^#(x₁, x₂)]	=	0
[flatten^#(x₁)]	=	0
[flatten#1^#(x₁)]	=	0
[flattensort^#(x₁)]	=	2 + 2 · x₁ + 2 · x₁ · x₁
[insert^#(x₁, x₂)]	=	1 + 2 · x₂
[insert#1^#(x₁, x₂)]	=	2 · x₁ + 0
[insert#2^#(x₁,...,x₄)]	=	1 + 2 · x₄
[insertionsort^#(x₁)]	=	2 · x₁ · x₁ + 0
[insertionsort#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	2
[#EQ]	=	1
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	0
[#LT]	=	1
[#s(x₁)]	=	0
[leaf]	=	0
[node(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃

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

#cklt^#(#EQ)	→	c	(62)
#cklt^#(#GT)	→	c1	(63)
#cklt^#(#LT)	→	c2	(64)
#compare^#(#0,#0)	→	c3	(65)
#compare^#(#0,#neg(z0))	→	c4	(67)
#compare^#(#0,#pos(z0))	→	c5	(69)
#compare^#(#0,#s(z0))	→	c6	(71)
#compare^#(#neg(z0),#0)	→	c7	(73)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(75)
#compare^#(#neg(z0),#pos(z1))	→	c9	(77)
#compare^#(#pos(z0),#0)	→	c10	(79)
#compare^#(#pos(z0),#neg(z1))	→	c11	(81)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(83)
#compare^#(#s(z0),#0)	→	c13	(85)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(87)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(33)
append^#(z0,z1)	→	c16(append#1^#(z0,z1))	(35)
append#1^#(::(z0,z1),z2)	→	c17(append^#(z1,z2))	(37)
append#1^#(nil,z0)	→	c18	(39)
flatten^#(z0)	→	c19(flatten#1^#(z0))	(41)
flatten#1^#(leaf)	→	c20	(42)
flatten#1^#(node(z0,z1,z2))	→	c21(append^#(z0,append(flatten(z1),flatten(z2))),append^#(flatten(z1),flatten(z2)),flatten^#(z1),flatten^#(z2))	(44)
flattensort^#(z0)	→	c22(insertionsort^#(flatten(z0)),flatten^#(z0))	(46)
insert^#(z0,z1)	→	c23(insert#1^#(z1,z0))	(48)
insert#1^#(::(z0,z1),z2)	→	c24(insert#2^#(#less(z0,z2),z2,z0,z1),#less^#(z0,z2))	(50)
insert#1^#(nil,z0)	→	c25	(52)
insert#2^#(#false,z0,z1,z2)	→	c26	(54)
insert#2^#(#true,z0,z1,z2)	→	c27(insert^#(z0,z2))	(56)
insertionsort^#(z0)	→	c28(insertionsort#1^#(z0))	(58)
insertionsort#1^#(::(z0,z1))	→	c29(insert^#(z0,insertionsort(z1)),insertionsort^#(z1))	(60)
insertionsort#1^#(nil)	→	c30	(61)
flatten#1(leaf)	→	nil	(6)
flatten(z0)	→	flatten#1(z0)	(40)
insert#2(#false,z0,z1,z2)	→	::(z0,::(z1,z2))	(53)
insert#1(::(z0,z1),z2)	→	insert#2(#less(z0,z2),z2,z0,z1)	(49)
insert#2(#true,z0,z1,z2)	→	::(z1,insert(z0,z2))	(55)
append(z0,z1)	→	append#1(z0,z1)	(34)
append#1(nil,z0)	→	z0	(38)
flatten#1(node(z0,z1,z2))	→	append(z0,append(flatten(z1),flatten(z2)))	(43)
insertionsort#1(nil)	→	nil	(16)
insert(z0,z1)	→	insert#1(z1,z0)	(47)
insertionsort#1(::(z0,z1))	→	insert(z0,insertionsort(z1))	(59)
insert#1(nil,z0)	→	::(z0,nil)	(51)
insertionsort(z0)	→	insertionsort#1(z0)	(57)
append#1(::(z0,z1),z2)	→	::(z0,append(z1,z2))	(36)

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