Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/raML/minsort.raml)

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

#less(@x,@y)	→	#cklt(#compare(@x,@y))	(1)
findMin(@l)	→	findMin#1(@l)	(2)
findMin#1(::(@x,@xs))	→	findMin#2(findMin(@xs),@x)	(3)
findMin#1(nil)	→	nil	(4)
findMin#2(::(@y,@ys),@x)	→	findMin#3(#less(@x,@y),@x,@y,@ys)	(5)
findMin#2(nil,@x)	→	::(@x,nil)	(6)
findMin#3(#false,@x,@y,@ys)	→	::(@y,::(@x,@ys))	(7)
findMin#3(#true,@x,@y,@ys)	→	::(@x,::(@y,@ys))	(8)
minSort(@l)	→	minSort#1(findMin(@l))	(9)
minSort#1(::(@x,@xs))	→	::(@x,minSort(@xs))	(10)
minSort#1(nil)	→	nil	(11)

and S is the following TRS.

#cklt(#EQ)	→	#false	(12)
#cklt(#GT)	→	#false	(13)
#cklt(#LT)	→	#true	(14)
#compare(#0,#0)	→	#EQ	(15)
#compare(#0,#neg(@y))	→	#GT	(16)
#compare(#0,#pos(@y))	→	#LT	(17)
#compare(#0,#s(@y))	→	#LT	(18)
#compare(#neg(@x),#0)	→	#LT	(19)
#compare(#neg(@x),#neg(@y))	→	#compare(@y,@x)	(20)
#compare(#neg(@x),#pos(@y))	→	#LT	(21)
#compare(#pos(@x),#0)	→	#GT	(22)
#compare(#pos(@x),#neg(@y))	→	#GT	(23)
#compare(#pos(@x),#pos(@y))	→	#compare(@x,@y)	(24)
#compare(#s(@x),#0)	→	#GT	(25)
#compare(#s(@x),#s(@y))	→	#compare(@x,@y)	(26)

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

(28)

originates from

#less(z0,z1)

→

#cklt(#compare(z0,z1))

(27)

findMin^#(z0)

→

c16(findMin#1^#(z0))

(30)

originates from

findMin(z0)

→

findMin#1(z0)

(29)

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

→

c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))

(32)

originates from

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

→

findMin#2(findMin(z1),z0)

(31)

findMin#1^#(nil)

→

c18

(33)

originates from

findMin#1(nil)

→

nil

(4)

findMin#2^#(::(z0,z1),z2)

→

c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))

(35)

originates from

findMin#2(::(z0,z1),z2)

→

findMin#3(#less(z2,z0),z2,z0,z1)

(34)

findMin#2^#(nil,z0)

→

c20

(37)

originates from

findMin#2(nil,z0)

→

::(z0,nil)

(36)

findMin#3^#(#false,z0,z1,z2)

→

c21

(39)

originates from

findMin#3(#false,z0,z1,z2)

→

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

(38)

findMin#3^#(#true,z0,z1,z2)

→

c22

(41)

originates from

findMin#3(#true,z0,z1,z2)

→

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

(40)

minSort^#(z0)

→

c23(minSort#1^#(findMin(z0)),findMin^#(z0))

(43)

originates from

minSort(z0)

→

minSort#1(findMin(z0))

(42)

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

→

c24(minSort^#(z1))

(45)

originates from

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

→

::(z0,minSort(z1))

(44)

minSort#1^#(nil)

→

c25

(46)

originates from

minSort#1(nil)

→

nil

(11)

#cklt^#(#EQ)

→

(47)

originates from

#cklt(#EQ)

→

#false

(12)

#cklt^#(#GT)

→

(48)

originates from

#cklt(#GT)

→

#false

(13)

#cklt^#(#LT)

→

(49)

originates from

#cklt(#LT)

→

#true

(14)

#compare^#(#0,#0)

→

(50)

originates from

#compare(#0,#0)

→

#EQ

(15)

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

→

(52)

originates from

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

→

#GT

(51)

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

→

(54)

originates from

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

→

#LT

(53)

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

→

(56)

originates from

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

→

#LT

(55)

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

→

(58)

originates from

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

→

#LT

(57)

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

→

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

(60)

originates from

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

→

#compare(z1,z0)

(59)

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

→

(62)

originates from

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

→

#LT

(61)

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

→

c10

(64)

originates from

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

→

#GT

(63)

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

→

c11

(66)

originates from

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

→

#GT

(65)

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

→

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

(68)

originates from

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

→

#compare(z0,z1)

(67)

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

→

c13

(70)

originates from

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

→

#GT

(69)

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

→

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

(72)

originates from

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

→

#compare(z0,z1)

(71)

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)

findMin^#(z0)

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

findMin#1^#(nil)

findMin#2^#(::(z0,z1),z2)

findMin#2^#(nil,z0)

findMin#3^#(#false,z0,z1,z2)

findMin#3^#(#true,z0,z1,z2)

minSort^#(z0)

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

minSort#1^#(nil)

1.1 Usable Rules

We remove the following rules since they are not usable.

minSort(z0)	→	minSort#1(findMin(z0))	(42)
minSort#1(::(z0,z1))	→	::(z0,minSort(z1))	(44)
minSort#1(nil)	→	nil	(11)

1.1.1 Rule Shifting

The rules

minSort#1^#(nil)

→

c25

(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₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c18]	=	0
[c19(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[#compare(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[findMin(x₁)]	=	1 · x₁ + 0
[findMin#1(x₁)]	=	1
[findMin#2(x₁, x₂)]	=	1 + 1 · x₂
[findMin#3(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[#less(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[#cklt(x₁)]	=	1 + 1 · x₁
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[findMin^#(x₁)]	=	0
[findMin#1^#(x₁)]	=	0
[findMin#2^#(x₁, x₂)]	=	0
[findMin#3^#(x₁,...,x₄)]	=	0
[minSort^#(x₁)]	=	1
[minSort#1^#(x₁)]	=	1
[::(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₁

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

#cklt^#(#EQ)	→	c	(47)
#cklt^#(#GT)	→	c1	(48)
#cklt^#(#LT)	→	c2	(49)
#compare^#(#0,#0)	→	c3	(50)
#compare^#(#0,#neg(z0))	→	c4	(52)
#compare^#(#0,#pos(z0))	→	c5	(54)
#compare^#(#0,#s(z0))	→	c6	(56)
#compare^#(#neg(z0),#0)	→	c7	(58)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(60)
#compare^#(#neg(z0),#pos(z1))	→	c9	(62)
#compare^#(#pos(z0),#0)	→	c10	(64)
#compare^#(#pos(z0),#neg(z1))	→	c11	(66)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(68)
#compare^#(#s(z0),#0)	→	c13	(70)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(72)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(28)
findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)
findMin#1^#(nil)	→	c18	(33)
findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(37)
findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)
minSort^#(z0)	→	c23(minSort#1^#(findMin(z0)),findMin^#(z0))	(43)
minSort#1^#(::(z0,z1))	→	c24(minSort^#(z1))	(45)
minSort#1^#(nil)	→	c25	(46)

1.1.1.1 Rule Shifting

The rules

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

→

c24(minSort^#(z1))

(45)

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₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c18]	=	0
[c19(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[#compare(x₁, x₂)]	=	1
[findMin(x₁)]	=	1 · x₁ + 0
[findMin#1(x₁)]	=	1 · x₁ + 0
[findMin#2(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[findMin#3(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[#less(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1 · x₁ + 0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[findMin^#(x₁)]	=	0
[findMin#1^#(x₁)]	=	0
[findMin#2^#(x₁, x₂)]	=	0
[findMin#3^#(x₁,...,x₄)]	=	0
[minSort^#(x₁)]	=	1 · x₁ + 0
[minSort#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₁

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

#cklt^#(#EQ)	→	c	(47)
#cklt^#(#GT)	→	c1	(48)
#cklt^#(#LT)	→	c2	(49)
#compare^#(#0,#0)	→	c3	(50)
#compare^#(#0,#neg(z0))	→	c4	(52)
#compare^#(#0,#pos(z0))	→	c5	(54)
#compare^#(#0,#s(z0))	→	c6	(56)
#compare^#(#neg(z0),#0)	→	c7	(58)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(60)
#compare^#(#neg(z0),#pos(z1))	→	c9	(62)
#compare^#(#pos(z0),#0)	→	c10	(64)
#compare^#(#pos(z0),#neg(z1))	→	c11	(66)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(68)
#compare^#(#s(z0),#0)	→	c13	(70)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(72)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(28)
findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)
findMin#1^#(nil)	→	c18	(33)
findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(37)
findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)
minSort^#(z0)	→	c23(minSort#1^#(findMin(z0)),findMin^#(z0))	(43)
minSort#1^#(::(z0,z1))	→	c24(minSort^#(z1))	(45)
minSort#1^#(nil)	→	c25	(46)
findMin#2(nil,z0)	→	::(z0,nil)	(36)
#compare(#0,#neg(z0))	→	#GT	(51)
findMin#1(nil)	→	nil	(4)
findMin#3(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(40)
#compare(#0,#pos(z0))	→	#LT	(53)
findMin#2(::(z0,z1),z2)	→	findMin#3(#less(z2,z0),z2,z0,z1)	(34)
findMin#3(#false,z0,z1,z2)	→	::(z1,::(z0,z2))	(38)
#compare(#0,#s(z0))	→	#LT	(55)
findMin(z0)	→	findMin#1(z0)	(29)
#compare(#pos(z0),#0)	→	#GT	(63)
#compare(#neg(z0),#neg(z1))	→	#compare(z1,z0)	(59)
#cklt(#GT)	→	#false	(13)
#compare(#s(z0),#s(z1))	→	#compare(z0,z1)	(71)
#compare(#0,#0)	→	#EQ	(15)
#compare(#s(z0),#0)	→	#GT	(69)
#compare(#neg(z0),#pos(z1))	→	#LT	(61)
#compare(#neg(z0),#0)	→	#LT	(57)
#cklt(#EQ)	→	#false	(12)
#compare(#pos(z0),#pos(z1))	→	#compare(z0,z1)	(67)
#compare(#pos(z0),#neg(z1))	→	#GT	(65)
findMin#1(::(z0,z1))	→	findMin#2(findMin(z1),z0)	(31)
#less(z0,z1)	→	#cklt(#compare(z0,z1))	(27)
#cklt(#LT)	→	#true	(14)

1.1.1.1.1 Rule Shifting

The rules

minSort^#(z0)

→

c23(minSort#1^#(findMin(z0)),findMin^#(z0))

(43)

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₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c18]	=	0
[c19(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[#compare(x₁, x₂)]	=	1
[findMin(x₁)]	=	1 · x₁ + 0
[findMin#1(x₁)]	=	1 · x₁ + 0
[findMin#2(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[findMin#3(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[#less(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1 · x₁ + 0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[findMin^#(x₁)]	=	0
[findMin#1^#(x₁)]	=	0
[findMin#2^#(x₁, x₂)]	=	0
[findMin#3^#(x₁,...,x₄)]	=	0
[minSort^#(x₁)]	=	1 + 1 · x₁
[minSort#1^#(x₁)]	=	1 · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[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₁

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

#cklt^#(#EQ)	→	c	(47)
#cklt^#(#GT)	→	c1	(48)
#cklt^#(#LT)	→	c2	(49)
#compare^#(#0,#0)	→	c3	(50)
#compare^#(#0,#neg(z0))	→	c4	(52)
#compare^#(#0,#pos(z0))	→	c5	(54)
#compare^#(#0,#s(z0))	→	c6	(56)
#compare^#(#neg(z0),#0)	→	c7	(58)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(60)
#compare^#(#neg(z0),#pos(z1))	→	c9	(62)
#compare^#(#pos(z0),#0)	→	c10	(64)
#compare^#(#pos(z0),#neg(z1))	→	c11	(66)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(68)
#compare^#(#s(z0),#0)	→	c13	(70)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(72)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(28)
findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)
findMin#1^#(nil)	→	c18	(33)
findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(37)
findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)
minSort^#(z0)	→	c23(minSort#1^#(findMin(z0)),findMin^#(z0))	(43)
minSort#1^#(::(z0,z1))	→	c24(minSort^#(z1))	(45)
minSort#1^#(nil)	→	c25	(46)
findMin#2(nil,z0)	→	::(z0,nil)	(36)
#compare(#0,#neg(z0))	→	#GT	(51)
findMin#1(nil)	→	nil	(4)
findMin#3(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(40)
#compare(#0,#pos(z0))	→	#LT	(53)
findMin#2(::(z0,z1),z2)	→	findMin#3(#less(z2,z0),z2,z0,z1)	(34)
findMin#3(#false,z0,z1,z2)	→	::(z1,::(z0,z2))	(38)
#compare(#0,#s(z0))	→	#LT	(55)
findMin(z0)	→	findMin#1(z0)	(29)
#compare(#pos(z0),#0)	→	#GT	(63)
#compare(#neg(z0),#neg(z1))	→	#compare(z1,z0)	(59)
#cklt(#GT)	→	#false	(13)
#compare(#s(z0),#s(z1))	→	#compare(z0,z1)	(71)
#compare(#0,#0)	→	#EQ	(15)
#compare(#s(z0),#0)	→	#GT	(69)
#compare(#neg(z0),#pos(z1))	→	#LT	(61)
#compare(#neg(z0),#0)	→	#LT	(57)
#cklt(#EQ)	→	#false	(12)
#compare(#pos(z0),#pos(z1))	→	#compare(z0,z1)	(67)
#compare(#pos(z0),#neg(z1))	→	#GT	(65)
findMin#1(::(z0,z1))	→	findMin#2(findMin(z1),z0)	(31)
#less(z0,z1)	→	#cklt(#compare(z0,z1))	(27)
#cklt(#LT)	→	#true	(14)

1.1.1.1.1.1 Rule Shifting

The rules

findMin#1^#(nil)

→

c18

(33)

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₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c18]	=	0
[c19(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[#compare(x₁, x₂)]	=	1
[findMin(x₁)]	=	1 · x₁ + 0
[findMin#1(x₁)]	=	1 · x₁ + 0
[findMin#2(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[findMin#3(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[#less(x₁, x₂)]	=	1
[#cklt(x₁)]	=	1 · x₁ + 0
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[findMin^#(x₁)]	=	1
[findMin#1^#(x₁)]	=	1
[findMin#2^#(x₁, x₂)]	=	0
[findMin#3^#(x₁,...,x₄)]	=	0
[minSort^#(x₁)]	=	1 + 1 · x₁
[minSort#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₁

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

#cklt^#(#EQ)	→	c	(47)
#cklt^#(#GT)	→	c1	(48)
#cklt^#(#LT)	→	c2	(49)
#compare^#(#0,#0)	→	c3	(50)
#compare^#(#0,#neg(z0))	→	c4	(52)
#compare^#(#0,#pos(z0))	→	c5	(54)
#compare^#(#0,#s(z0))	→	c6	(56)
#compare^#(#neg(z0),#0)	→	c7	(58)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(60)
#compare^#(#neg(z0),#pos(z1))	→	c9	(62)
#compare^#(#pos(z0),#0)	→	c10	(64)
#compare^#(#pos(z0),#neg(z1))	→	c11	(66)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(68)
#compare^#(#s(z0),#0)	→	c13	(70)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(72)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(28)
findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)
findMin#1^#(nil)	→	c18	(33)
findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(37)
findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)
minSort^#(z0)	→	c23(minSort#1^#(findMin(z0)),findMin^#(z0))	(43)
minSort#1^#(::(z0,z1))	→	c24(minSort^#(z1))	(45)
minSort#1^#(nil)	→	c25	(46)
findMin#2(nil,z0)	→	::(z0,nil)	(36)
#compare(#0,#neg(z0))	→	#GT	(51)
findMin#1(nil)	→	nil	(4)
findMin#3(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(40)
#compare(#0,#pos(z0))	→	#LT	(53)
findMin#2(::(z0,z1),z2)	→	findMin#3(#less(z2,z0),z2,z0,z1)	(34)
findMin#3(#false,z0,z1,z2)	→	::(z1,::(z0,z2))	(38)
#compare(#0,#s(z0))	→	#LT	(55)
findMin(z0)	→	findMin#1(z0)	(29)
#compare(#pos(z0),#0)	→	#GT	(63)
#compare(#neg(z0),#neg(z1))	→	#compare(z1,z0)	(59)
#cklt(#GT)	→	#false	(13)
#compare(#s(z0),#s(z1))	→	#compare(z0,z1)	(71)
#compare(#0,#0)	→	#EQ	(15)
#compare(#s(z0),#0)	→	#GT	(69)
#compare(#neg(z0),#pos(z1))	→	#LT	(61)
#compare(#neg(z0),#0)	→	#LT	(57)
#cklt(#EQ)	→	#false	(12)
#compare(#pos(z0),#pos(z1))	→	#compare(z0,z1)	(67)
#compare(#pos(z0),#neg(z1))	→	#GT	(65)
findMin#1(::(z0,z1))	→	findMin#2(findMin(z1),z0)	(31)
#less(z0,z1)	→	#cklt(#compare(z0,z1))	(27)
#cklt(#LT)	→	#true	(14)

1.1.1.1.1.1.1 Rule Shifting

The rules

findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(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₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c18]	=	0
[c19(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[#compare(x₁, x₂)]	=	0
[findMin(x₁)]	=	1 · x₁ + 0
[findMin#1(x₁)]	=	1 · x₁ + 0
[findMin#2(x₁, x₂)]	=	1 + 1 · x₁
[findMin#3(x₁,...,x₄)]	=	2 + 1 · x₄
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[findMin^#(x₁)]	=	1 · x₁ + 0
[findMin#1^#(x₁)]	=	1 · x₁ + 0
[findMin#2^#(x₁, x₂)]	=	1
[findMin#3^#(x₁,...,x₄)]	=	0
[minSort^#(x₁)]	=	1 · x₁ + 0 + 1 · x₁ · x₁
[minSort#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	0
[#EQ]	=	0
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	1
[#LT]	=	1
[#s(x₁)]	=	1

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

#cklt^#(#EQ)	→	c	(47)
#cklt^#(#GT)	→	c1	(48)
#cklt^#(#LT)	→	c2	(49)
#compare^#(#0,#0)	→	c3	(50)
#compare^#(#0,#neg(z0))	→	c4	(52)
#compare^#(#0,#pos(z0))	→	c5	(54)
#compare^#(#0,#s(z0))	→	c6	(56)
#compare^#(#neg(z0),#0)	→	c7	(58)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(60)
#compare^#(#neg(z0),#pos(z1))	→	c9	(62)
#compare^#(#pos(z0),#0)	→	c10	(64)
#compare^#(#pos(z0),#neg(z1))	→	c11	(66)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(68)
#compare^#(#s(z0),#0)	→	c13	(70)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(72)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(28)
findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)
findMin#1^#(nil)	→	c18	(33)
findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(37)
findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)
minSort^#(z0)	→	c23(minSort#1^#(findMin(z0)),findMin^#(z0))	(43)
minSort#1^#(::(z0,z1))	→	c24(minSort^#(z1))	(45)
minSort#1^#(nil)	→	c25	(46)
findMin#2(nil,z0)	→	::(z0,nil)	(36)
findMin#1(nil)	→	nil	(4)
findMin#3(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(40)
findMin#2(::(z0,z1),z2)	→	findMin#3(#less(z2,z0),z2,z0,z1)	(34)
findMin#3(#false,z0,z1,z2)	→	::(z1,::(z0,z2))	(38)
findMin(z0)	→	findMin#1(z0)	(29)
findMin#1(::(z0,z1))	→	findMin#2(findMin(z1),z0)	(31)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)

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₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c18]	=	0
[c19(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[#compare(x₁, x₂)]	=	0
[findMin(x₁)]	=	1 · x₁ + 0
[findMin#1(x₁)]	=	1 · x₁ + 0
[findMin#2(x₁, x₂)]	=	1 + 1 · x₁
[findMin#3(x₁,...,x₄)]	=	2 + 1 · x₄
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[findMin^#(x₁)]	=	1 + 2 · x₁
[findMin#1^#(x₁)]	=	2 · x₁ + 0
[findMin#2^#(x₁, x₂)]	=	0
[findMin#3^#(x₁,...,x₄)]	=	0
[minSort^#(x₁)]	=	1 + 2 · x₁ + 1 · x₁ · x₁
[minSort#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	0
[#EQ]	=	0
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	1
[#LT]	=	1
[#s(x₁)]	=	1

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

#cklt^#(#EQ)	→	c	(47)
#cklt^#(#GT)	→	c1	(48)
#cklt^#(#LT)	→	c2	(49)
#compare^#(#0,#0)	→	c3	(50)
#compare^#(#0,#neg(z0))	→	c4	(52)
#compare^#(#0,#pos(z0))	→	c5	(54)
#compare^#(#0,#s(z0))	→	c6	(56)
#compare^#(#neg(z0),#0)	→	c7	(58)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(60)
#compare^#(#neg(z0),#pos(z1))	→	c9	(62)
#compare^#(#pos(z0),#0)	→	c10	(64)
#compare^#(#pos(z0),#neg(z1))	→	c11	(66)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(68)
#compare^#(#s(z0),#0)	→	c13	(70)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(72)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(28)
findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)
findMin#1^#(nil)	→	c18	(33)
findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(37)
findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)
minSort^#(z0)	→	c23(minSort#1^#(findMin(z0)),findMin^#(z0))	(43)
minSort#1^#(::(z0,z1))	→	c24(minSort^#(z1))	(45)
minSort#1^#(nil)	→	c25	(46)
findMin#2(nil,z0)	→	::(z0,nil)	(36)
findMin#1(nil)	→	nil	(4)
findMin#3(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(40)
findMin#2(::(z0,z1),z2)	→	findMin#3(#less(z2,z0),z2,z0,z1)	(34)
findMin#3(#false,z0,z1,z2)	→	::(z1,::(z0,z2))	(38)
findMin(z0)	→	findMin#1(z0)	(29)
findMin#1(::(z0,z1))	→	findMin#2(findMin(z1),z0)	(31)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(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₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c18]	=	0
[c19(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[#compare(x₁, x₂)]	=	0
[findMin(x₁)]	=	1 · x₁ + 0
[findMin#1(x₁)]	=	1 · x₁ + 0
[findMin#2(x₁, x₂)]	=	1 + 1 · x₁
[findMin#3(x₁,...,x₄)]	=	2 + 1 · x₄
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	0
[findMin^#(x₁)]	=	1 · x₁ + 0
[findMin#1^#(x₁)]	=	1 · x₁ + 0
[findMin#2^#(x₁, x₂)]	=	1
[findMin#3^#(x₁,...,x₄)]	=	1
[minSort^#(x₁)]	=	2 · x₁ + 0 + 1 · x₁ · x₁
[minSort#1^#(x₁)]	=	1 · x₁ · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	0
[#EQ]	=	0
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	1
[#LT]	=	1
[#s(x₁)]	=	1

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

#cklt^#(#EQ)	→	c	(47)
#cklt^#(#GT)	→	c1	(48)
#cklt^#(#LT)	→	c2	(49)
#compare^#(#0,#0)	→	c3	(50)
#compare^#(#0,#neg(z0))	→	c4	(52)
#compare^#(#0,#pos(z0))	→	c5	(54)
#compare^#(#0,#s(z0))	→	c6	(56)
#compare^#(#neg(z0),#0)	→	c7	(58)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(60)
#compare^#(#neg(z0),#pos(z1))	→	c9	(62)
#compare^#(#pos(z0),#0)	→	c10	(64)
#compare^#(#pos(z0),#neg(z1))	→	c11	(66)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(68)
#compare^#(#s(z0),#0)	→	c13	(70)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(72)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(28)
findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)
findMin#1^#(nil)	→	c18	(33)
findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(37)
findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)
minSort^#(z0)	→	c23(minSort#1^#(findMin(z0)),findMin^#(z0))	(43)
minSort#1^#(::(z0,z1))	→	c24(minSort^#(z1))	(45)
minSort#1^#(nil)	→	c25	(46)
findMin#2(nil,z0)	→	::(z0,nil)	(36)
findMin#1(nil)	→	nil	(4)
findMin#3(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(40)
findMin#2(::(z0,z1),z2)	→	findMin#3(#less(z2,z0),z2,z0,z1)	(34)
findMin#3(#false,z0,z1,z2)	→	::(z1,::(z0,z2))	(38)
findMin(z0)	→	findMin#1(z0)	(29)
findMin#1(::(z0,z1))	→	findMin#2(findMin(z1),z0)	(31)

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

(28)

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₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c18]	=	0
[c19(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c24(x₁)]	=	1 · x₁ + 0
[c25]	=	0
[#compare(x₁, x₂)]	=	0
[findMin(x₁)]	=	1 · x₁ + 0
[findMin#1(x₁)]	=	1 · x₁ + 0
[findMin#2(x₁, x₂)]	=	1 + 1 · x₁
[findMin#3(x₁,...,x₄)]	=	2 + 1 · x₄
[#less(x₁, x₂)]	=	0
[#cklt(x₁)]	=	1
[#cklt^#(x₁)]	=	0
[#compare^#(x₁, x₂)]	=	0
[#less^#(x₁, x₂)]	=	1
[findMin^#(x₁)]	=	2 · x₁ + 0
[findMin#1^#(x₁)]	=	2 · x₁ + 0
[findMin#2^#(x₁, x₂)]	=	2
[findMin#3^#(x₁,...,x₄)]	=	0
[minSort^#(x₁)]	=	2 · x₁ + 0 + 2 · x₁ · x₁
[minSort#1^#(x₁)]	=	2 · x₁ · x₁ + 0
[::(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	0
[#false]	=	0
[#true]	=	0
[#0]	=	0
[#EQ]	=	0
[#neg(x₁)]	=	0
[#GT]	=	1
[#pos(x₁)]	=	1
[#LT]	=	1
[#s(x₁)]	=	1

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

#cklt^#(#EQ)	→	c	(47)
#cklt^#(#GT)	→	c1	(48)
#cklt^#(#LT)	→	c2	(49)
#compare^#(#0,#0)	→	c3	(50)
#compare^#(#0,#neg(z0))	→	c4	(52)
#compare^#(#0,#pos(z0))	→	c5	(54)
#compare^#(#0,#s(z0))	→	c6	(56)
#compare^#(#neg(z0),#0)	→	c7	(58)
#compare^#(#neg(z0),#neg(z1))	→	c8(#compare^#(z1,z0))	(60)
#compare^#(#neg(z0),#pos(z1))	→	c9	(62)
#compare^#(#pos(z0),#0)	→	c10	(64)
#compare^#(#pos(z0),#neg(z1))	→	c11	(66)
#compare^#(#pos(z0),#pos(z1))	→	c12(#compare^#(z0,z1))	(68)
#compare^#(#s(z0),#0)	→	c13	(70)
#compare^#(#s(z0),#s(z1))	→	c14(#compare^#(z0,z1))	(72)
#less^#(z0,z1)	→	c15(#cklt^#(#compare(z0,z1)),#compare^#(z0,z1))	(28)
findMin^#(z0)	→	c16(findMin#1^#(z0))	(30)
findMin#1^#(::(z0,z1))	→	c17(findMin#2^#(findMin(z1),z0),findMin^#(z1))	(32)
findMin#1^#(nil)	→	c18	(33)
findMin#2^#(::(z0,z1),z2)	→	c19(findMin#3^#(#less(z2,z0),z2,z0,z1),#less^#(z2,z0))	(35)
findMin#2^#(nil,z0)	→	c20	(37)
findMin#3^#(#false,z0,z1,z2)	→	c21	(39)
findMin#3^#(#true,z0,z1,z2)	→	c22	(41)
minSort^#(z0)	→	c23(minSort#1^#(findMin(z0)),findMin^#(z0))	(43)
minSort#1^#(::(z0,z1))	→	c24(minSort^#(z1))	(45)
minSort#1^#(nil)	→	c25	(46)
findMin#2(nil,z0)	→	::(z0,nil)	(36)
findMin#1(nil)	→	nil	(4)
findMin#3(#true,z0,z1,z2)	→	::(z0,::(z1,z2))	(40)
findMin#2(::(z0,z1),z2)	→	findMin#3(#less(z2,z0),z2,z0,z1)	(34)
findMin#3(#false,z0,z1,z2)	→	::(z1,::(z0,z2))	(38)
findMin(z0)	→	findMin#1(z0)	(29)
findMin#1(::(z0,z1))	→	findMin#2(findMin(z1),z0)	(31)

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