Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/isort)

The rewrite relation of the following TRS is considered.

sort#2(Nil)	→	Nil	(1)
sort#2(Cons(x4,x2))	→	insert#3(x4,sort#2(x2))	(2)
cond_insert_ord_x_ys_1(True,x3,x2,x1)	→	Cons(x3,Cons(x2,x1))	(3)
cond_insert_ord_x_ys_1(False,x3,x2,x1)	→	Cons(x2,insert#3(x3,x1))	(4)
insert#3(x2,Nil)	→	Cons(x2,Nil)	(5)
insert#3(x6,Cons(x4,x2))	→	cond_insert_ord_x_ys_1(leq#2(x6,x4),x6,x4,x2)	(6)
leq#2(0,x8)	→	True	(7)
leq#2(S(x12),0)	→	False	(8)
leq#2(S(x4),S(x2))	→	leq#2(x4,x2)	(9)
main(x1)	→	sort#2(x1)	(10)

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:

sort#2^#(Nil)

→

(11)

originates from

sort#2(Nil)

→

Nil

(1)

sort#2^#(Cons(z0,z1))

→

c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))

(13)

originates from

sort#2(Cons(z0,z1))

→

insert#3(z0,sort#2(z1))

(12)

cond_insert_ord_x_ys_1^#(True,z0,z1,z2)

→

(15)

originates from

cond_insert_ord_x_ys_1(True,z0,z1,z2)

→

Cons(z0,Cons(z1,z2))

(14)

cond_insert_ord_x_ys_1^#(False,z0,z1,z2)

→

c3(insert#3^#(z0,z2))

(17)

originates from

cond_insert_ord_x_ys_1(False,z0,z1,z2)

→

Cons(z1,insert#3(z0,z2))

(16)

insert#3^#(z0,Nil)

→

(19)

originates from

insert#3(z0,Nil)

→

Cons(z0,Nil)

(18)

insert#3^#(z0,Cons(z1,z2))

→

c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))

(21)

originates from

insert#3(z0,Cons(z1,z2))

→

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

(20)

leq#2^#(0,z0)

→

(23)

originates from

leq#2(0,z0)

→

True

(22)

leq#2^#(S(z0),0)

→

(25)

originates from

leq#2(S(z0),0)

→

False

(24)

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

→

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

(27)

originates from

leq#2(S(z0),S(z1))

→

leq#2(z0,z1)

(26)

main^#(z0)

→

c9(sort#2^#(z0))

(29)

originates from

main(z0)

→

sort#2(z0)

(28)

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

sort#2^#(Nil)

sort#2^#(Cons(z0,z1))

cond_insert_ord_x_ys_1^#(True,z0,z1,z2)

cond_insert_ord_x_ys_1^#(False,z0,z1,z2)

insert#3^#(z0,Nil)

insert#3^#(z0,Cons(z1,z2))

leq#2^#(0,z0)

leq#2^#(S(z0),0)

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

main^#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.

main(z0)

→

sort#2(z0)

(28)

1.1.1 Rule Shifting

The rules

sort#2^#(Nil)	→	c	(11)
sort#2^#(Cons(z0,z1))	→	c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))	(13)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9(x₁)]	=	1 · x₁ + 0
[sort#2(x₁)]	=	1 + 1 · x₁
[insert#3(x₁, x₂)]	=	1 + 1 · x₁
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	1 + 1 · x₂ + 1 · x₃ + 1 · x₄
[leq#2(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[sort#2^#(x₁)]	=	1 + 1 · x₁
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	1 · x₂ + 0
[insert#3^#(x₁, x₂)]	=	1 · x₁ + 0
[leq#2^#(x₁, x₂)]	=	0
[main^#(x₁)]	=	1 + 1 · x₁
[0]	=	1
[True]	=	1
[S(x₁)]	=	1 + 1 · x₁
[False]	=	1
[Nil]	=	1
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂

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

sort#2^#(Nil)	→	c	(11)
sort#2^#(Cons(z0,z1))	→	c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))	(13)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(15)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert#3^#(z0,z2))	(17)
insert#3^#(z0,Nil)	→	c4	(19)
insert#3^#(z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(21)
leq#2^#(0,z0)	→	c6	(23)
leq#2^#(S(z0),0)	→	c7	(25)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(27)
main^#(z0)	→	c9(sort#2^#(z0))	(29)

1.1.1.1 Rule Shifting

The rules

cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(15)
insert#3^#(z0,Nil)	→	c4	(19)
main^#(z0)	→	c9(sort#2^#(z0))	(29)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9(x₁)]	=	1 · x₁ + 0
[sort#2(x₁)]	=	1 · x₁ + 0
[insert#3(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄
[leq#2(x₁, x₂)]	=	1
[sort#2^#(x₁)]	=	1 · x₁ + 0
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₂
[insert#3^#(x₁, x₂)]	=	1 + 1 · x₁
[leq#2^#(x₁, x₂)]	=	0
[main^#(x₁)]	=	1 + 1 · x₁
[0]	=	1
[True]	=	1
[S(x₁)]	=	1 + 1 · x₁
[False]	=	1
[Nil]	=	1
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂

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

sort#2^#(Nil)	→	c	(11)
sort#2^#(Cons(z0,z1))	→	c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))	(13)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(15)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert#3^#(z0,z2))	(17)
insert#3^#(z0,Nil)	→	c4	(19)
insert#3^#(z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(21)
leq#2^#(0,z0)	→	c6	(23)
leq#2^#(S(z0),0)	→	c7	(25)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(27)
main^#(z0)	→	c9(sort#2^#(z0))	(29)
leq#2(0,z0)	→	True	(22)
leq#2(S(z0),0)	→	False	(24)
leq#2(S(z0),S(z1))	→	leq#2(z0,z1)	(26)

1.1.1.1.1 Rule Shifting

The rules

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

→

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

(27)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9(x₁)]	=	1 · x₁ + 0
[sort#2(x₁)]	=	1 · x₁ + 0
[insert#3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	1 · x₂ + 0 + 1 · x₃ + 1 · x₄
[leq#2(x₁, x₂)]	=	0
[sort#2^#(x₁)]	=	2 + 1 · x₁ · x₁
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[insert#3^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[leq#2^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[main^#(x₁)]	=	2 + 1 · x₁ + 1 · x₁ · x₁
[0]	=	0
[True]	=	0
[S(x₁)]	=	2 + 1 · x₁
[False]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂

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

sort#2^#(Nil)	→	c	(11)
sort#2^#(Cons(z0,z1))	→	c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))	(13)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(15)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert#3^#(z0,z2))	(17)
insert#3^#(z0,Nil)	→	c4	(19)
insert#3^#(z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(21)
leq#2^#(0,z0)	→	c6	(23)
leq#2^#(S(z0),0)	→	c7	(25)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(27)
main^#(z0)	→	c9(sort#2^#(z0))	(29)
insert#3(z0,Nil)	→	Cons(z0,Nil)	(18)
cond_insert_ord_x_ys_1(True,z0,z1,z2)	→	Cons(z0,Cons(z1,z2))	(14)
cond_insert_ord_x_ys_1(False,z0,z1,z2)	→	Cons(z1,insert#3(z0,z2))	(16)
sort#2(Cons(z0,z1))	→	insert#3(z0,sort#2(z1))	(12)
sort#2(Nil)	→	Nil	(1)
insert#3(z0,Cons(z1,z2))	→	cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2)	(20)

1.1.1.1.1.1 Rule Shifting

The rules

leq#2^#(S(z0),0)

→

(25)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9(x₁)]	=	1 · x₁ + 0
[sort#2(x₁)]	=	2 · x₁ + 0
[insert#3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	1 · x₂ + 0 + 1 · x₃ + 1 · x₄
[leq#2(x₁, x₂)]	=	0
[sort#2^#(x₁)]	=	2 + 1 · x₁ · x₁
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	1 · x₂ · x₄ + 0
[insert#3^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[leq#2^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[main^#(x₁)]	=	2 + 1 · x₁ + 2 · x₁ · x₁
[0]	=	1
[True]	=	0
[S(x₁)]	=	2 + 1 · x₁
[False]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂

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

sort#2^#(Nil)	→	c	(11)
sort#2^#(Cons(z0,z1))	→	c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))	(13)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(15)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert#3^#(z0,z2))	(17)
insert#3^#(z0,Nil)	→	c4	(19)
insert#3^#(z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(21)
leq#2^#(0,z0)	→	c6	(23)
leq#2^#(S(z0),0)	→	c7	(25)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(27)
main^#(z0)	→	c9(sort#2^#(z0))	(29)
insert#3(z0,Nil)	→	Cons(z0,Nil)	(18)
cond_insert_ord_x_ys_1(True,z0,z1,z2)	→	Cons(z0,Cons(z1,z2))	(14)
cond_insert_ord_x_ys_1(False,z0,z1,z2)	→	Cons(z1,insert#3(z0,z2))	(16)
sort#2(Cons(z0,z1))	→	insert#3(z0,sort#2(z1))	(12)
sort#2(Nil)	→	Nil	(1)
insert#3(z0,Cons(z1,z2))	→	cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2)	(20)

1.1.1.1.1.1.1 Rule Shifting

The rules

leq#2^#(0,z0)

→

(23)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9(x₁)]	=	1 · x₁ + 0
[sort#2(x₁)]	=	2 · x₁ + 0
[insert#3(x₁, x₂)]	=	1 + 2 · x₁ + 1 · x₂
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	2 + 2 · x₂ + 1 · x₃ + 1 · x₄
[leq#2(x₁, x₂)]	=	0
[sort#2^#(x₁)]	=	1 + 1 · x₁ · x₁
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	1 · x₂ · x₄ + 0
[insert#3^#(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[leq#2^#(x₁, x₂)]	=	1 · x₁ + 0
[main^#(x₁)]	=	1 + 1 · x₁ + 1 · x₁ · x₁
[0]	=	1
[True]	=	0
[S(x₁)]	=	1 · x₁ + 0
[False]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂

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

sort#2^#(Nil)	→	c	(11)
sort#2^#(Cons(z0,z1))	→	c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))	(13)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(15)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert#3^#(z0,z2))	(17)
insert#3^#(z0,Nil)	→	c4	(19)
insert#3^#(z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(21)
leq#2^#(0,z0)	→	c6	(23)
leq#2^#(S(z0),0)	→	c7	(25)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(27)
main^#(z0)	→	c9(sort#2^#(z0))	(29)
insert#3(z0,Nil)	→	Cons(z0,Nil)	(18)
cond_insert_ord_x_ys_1(True,z0,z1,z2)	→	Cons(z0,Cons(z1,z2))	(14)
cond_insert_ord_x_ys_1(False,z0,z1,z2)	→	Cons(z1,insert#3(z0,z2))	(16)
sort#2(Cons(z0,z1))	→	insert#3(z0,sort#2(z1))	(12)
sort#2(Nil)	→	Nil	(1)
insert#3(z0,Cons(z1,z2))	→	cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2)	(20)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

insert#3^#(z0,Cons(z1,z2))

→

c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))

(21)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9(x₁)]	=	1 · x₁ + 0
[sort#2(x₁)]	=	1 · x₁ + 0
[insert#3(x₁, x₂)]	=	1 + 1 · x₂
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	2 + 1 · x₄
[leq#2(x₁, x₂)]	=	0
[sort#2^#(x₁)]	=	2 + 1 · x₁ · x₁
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	1 · x₄ + 0
[insert#3^#(x₁, x₂)]	=	1 · x₂ + 0
[leq#2^#(x₁, x₂)]	=	0
[main^#(x₁)]	=	2 + 2 · x₁ + 1 · x₁ · x₁
[0]	=	0
[True]	=	0
[S(x₁)]	=	0
[False]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	1 + 1 · x₂

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

sort#2^#(Nil)	→	c	(11)
sort#2^#(Cons(z0,z1))	→	c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))	(13)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(15)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert#3^#(z0,z2))	(17)
insert#3^#(z0,Nil)	→	c4	(19)
insert#3^#(z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(21)
leq#2^#(0,z0)	→	c6	(23)
leq#2^#(S(z0),0)	→	c7	(25)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(27)
main^#(z0)	→	c9(sort#2^#(z0))	(29)
insert#3(z0,Nil)	→	Cons(z0,Nil)	(18)
cond_insert_ord_x_ys_1(True,z0,z1,z2)	→	Cons(z0,Cons(z1,z2))	(14)
cond_insert_ord_x_ys_1(False,z0,z1,z2)	→	Cons(z1,insert#3(z0,z2))	(16)
sort#2(Cons(z0,z1))	→	insert#3(z0,sort#2(z1))	(12)
sort#2(Nil)	→	Nil	(1)
insert#3(z0,Cons(z1,z2))	→	cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2)	(20)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

cond_insert_ord_x_ys_1^#(False,z0,z1,z2)

→

c3(insert#3^#(z0,z2))

(17)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9(x₁)]	=	1 · x₁ + 0
[sort#2(x₁)]	=	2 · x₁ + 0
[insert#3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	1 · x₂ + 0 + 1 · x₃ + 1 · x₄
[leq#2(x₁, x₂)]	=	1 · x₁ · x₂ + 0
[sort#2^#(x₁)]	=	2 + 2 · x₁ · x₁
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	2 · x₁ + 0 + 2 · x₂ · x₄
[insert#3^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[leq#2^#(x₁, x₂)]	=	0
[main^#(x₁)]	=	2 + 2 · x₁ + 2 · x₁ · x₁
[0]	=	1
[True]	=	0
[S(x₁)]	=	1 + 1 · x₁
[False]	=	1
[Nil]	=	0
[Cons(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂

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

sort#2^#(Nil)	→	c	(11)
sort#2^#(Cons(z0,z1))	→	c1(insert#3^#(z0,sort#2(z1)),sort#2^#(z1))	(13)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(15)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert#3^#(z0,z2))	(17)
insert#3^#(z0,Nil)	→	c4	(19)
insert#3^#(z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(21)
leq#2^#(0,z0)	→	c6	(23)
leq#2^#(S(z0),0)	→	c7	(25)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(27)
main^#(z0)	→	c9(sort#2^#(z0))	(29)
insert#3(z0,Nil)	→	Cons(z0,Nil)	(18)
leq#2(0,z0)	→	True	(22)
cond_insert_ord_x_ys_1(True,z0,z1,z2)	→	Cons(z0,Cons(z1,z2))	(14)
cond_insert_ord_x_ys_1(False,z0,z1,z2)	→	Cons(z1,insert#3(z0,z2))	(16)
sort#2(Cons(z0,z1))	→	insert#3(z0,sort#2(z1))	(12)
leq#2(S(z0),0)	→	False	(24)
leq#2(S(z0),S(z1))	→	leq#2(z0,z1)	(26)
sort#2(Nil)	→	Nil	(1)
insert#3(z0,Cons(z1,z2))	→	cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2)	(20)

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