Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/isort-fold)

The rewrite relation of the following TRS is considered.

fold#3(insert_ord(x2),Nil)	→	Nil	(1)
fold#3(insert_ord(x6),Cons(x4,x2))	→	insert_ord#2(x6,x4,fold#3(insert_ord(x6),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,x0,x5,x2)	→	Cons(x5,insert_ord#2(leq,x0,x2))	(4)
insert_ord#2(leq,x2,Nil)	→	Cons(x2,Nil)	(5)
insert_ord#2(leq,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(x3)	→	fold#3(insert_ord(leq),x3)	(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:

fold#3^#(insert_ord(z0),Nil)

→

(12)

originates from

fold#3(insert_ord(z0),Nil)

→

Nil

(11)

fold#3^#(insert_ord(z0),Cons(z1,z2))

→

c1(insert_ord#2^#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3^#(insert_ord(z0),z2))

(14)

originates from

fold#3(insert_ord(z0),Cons(z1,z2))

→

insert_ord#2(z0,z1,fold#3(insert_ord(z0),z2))

(13)

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

→

(16)

originates from

cond_insert_ord_x_ys_1(True,z0,z1,z2)

→

Cons(z0,Cons(z1,z2))

(15)

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

→

c3(insert_ord#2^#(leq,z0,z2))

(18)

originates from

cond_insert_ord_x_ys_1(False,z0,z1,z2)

→

Cons(z1,insert_ord#2(leq,z0,z2))

(17)

insert_ord#2^#(leq,z0,Nil)

→

(20)

originates from

insert_ord#2(leq,z0,Nil)

→

Cons(z0,Nil)

(19)

insert_ord#2^#(leq,z0,Cons(z1,z2))

→

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

(22)

originates from

insert_ord#2(leq,z0,Cons(z1,z2))

→

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

(21)

leq#2^#(0,z0)

→

(24)

originates from

leq#2(0,z0)

→

True

(23)

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

→

(26)

originates from

leq#2(S(z0),0)

→

False

(25)

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

→

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

(28)

originates from

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

→

leq#2(z0,z1)

(27)

main^#(z0)

→

c9(fold#3^#(insert_ord(leq),z0))

(30)

originates from

main(z0)

→

fold#3(insert_ord(leq),z0)

(29)

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

fold#3^#(insert_ord(z0),Nil)

fold#3^#(insert_ord(z0),Cons(z1,z2))

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

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

insert_ord#2^#(leq,z0,Nil)

insert_ord#2^#(leq,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)

→

fold#3(insert_ord(leq),z0)

(29)

1.1.1 Rule Shifting

The rules

main^#(z0)

→

c9(fold#3^#(insert_ord(leq),z0))

(30)

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
[fold#3(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[insert_ord#2(x₁, x₂, x₃)]	=	2 + 1 · x₃
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	1 + 3 · x₁ + 1 · x₄
[leq#2(x₁, x₂)]	=	1
[fold#3^#(x₁, x₂)]	=	0
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	0
[insert_ord#2^#(x₁, x₂, x₃)]	=	0
[leq#2^#(x₁, x₂)]	=	0
[main^#(x₁)]	=	1
[0]	=	0
[True]	=	3
[S(x₁)]	=	1 · x₁ + 0
[False]	=	3
[insert_ord(x₁)]	=	1
[Nil]	=	0
[Cons(x₁, x₂)]	=	2 + 1 · x₂
[leq]	=	0

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

fold#3^#(insert_ord(z0),Nil)	→	c	(12)
fold#3^#(insert_ord(z0),Cons(z1,z2))	→	c1(insert_ord#2^#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3^#(insert_ord(z0),z2))	(14)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(16)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert_ord#2^#(leq,z0,z2))	(18)
insert_ord#2^#(leq,z0,Nil)	→	c4	(20)
insert_ord#2^#(leq,z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(22)
leq#2^#(0,z0)	→	c6	(24)
leq#2^#(S(z0),0)	→	c7	(26)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(28)
main^#(z0)	→	c9(fold#3^#(insert_ord(leq),z0))	(30)

1.1.1.1 Rule Shifting

The rules

fold#3^#(insert_ord(z0),Nil)	→	c	(12)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(16)
insert_ord#2^#(leq,z0,Nil)	→	c4	(20)

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
[fold#3(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert_ord#2(x₁, 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₂
[fold#3^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	1 + 1 · x₂
[insert_ord#2^#(x₁, 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
[insert_ord(x₁)]	=	1
[Nil]	=	1
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[leq]	=	1

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

fold#3^#(insert_ord(z0),Nil)	→	c	(12)
fold#3^#(insert_ord(z0),Cons(z1,z2))	→	c1(insert_ord#2^#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3^#(insert_ord(z0),z2))	(14)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(16)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert_ord#2^#(leq,z0,z2))	(18)
insert_ord#2^#(leq,z0,Nil)	→	c4	(20)
insert_ord#2^#(leq,z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(22)
leq#2^#(0,z0)	→	c6	(24)
leq#2^#(S(z0),0)	→	c7	(26)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(28)
main^#(z0)	→	c9(fold#3^#(insert_ord(leq),z0))	(30)

1.1.1.1.1 Rule Shifting

The rules

fold#3^#(insert_ord(z0),Cons(z1,z2))

→

c1(insert_ord#2^#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3^#(insert_ord(z0),z2))

(14)

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
[fold#3(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[insert_ord#2(x₁, 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₂
[fold#3^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	1 · x₂ + 0
[insert_ord#2^#(x₁, 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
[insert_ord(x₁)]	=	1
[Nil]	=	1
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[leq]	=	1

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

fold#3^#(insert_ord(z0),Nil)	→	c	(12)
fold#3^#(insert_ord(z0),Cons(z1,z2))	→	c1(insert_ord#2^#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3^#(insert_ord(z0),z2))	(14)
cond_insert_ord_x_ys_1^#(True,z0,z1,z2)	→	c2	(16)
cond_insert_ord_x_ys_1^#(False,z0,z1,z2)	→	c3(insert_ord#2^#(leq,z0,z2))	(18)
insert_ord#2^#(leq,z0,Nil)	→	c4	(20)
insert_ord#2^#(leq,z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(22)
leq#2^#(0,z0)	→	c6	(24)
leq#2^#(S(z0),0)	→	c7	(26)
leq#2^#(S(z0),S(z1))	→	c8(leq#2^#(z0,z1))	(28)
main^#(z0)	→	c9(fold#3^#(insert_ord(leq),z0))	(30)

1.1.1.1.1.1 Rule Shifting

The rules

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

→

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

(28)

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
[fold#3(x₁, x₂)]	=	1 · x₂ + 0
[insert_ord#2(x₁, 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
[fold#3^#(x₁, x₂)]	=	1 · x₂ · x₂ + 0
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	2 · x₂ · x₄ + 0
[insert_ord#2^#(x₁, x₂, x₃)]	=	2 · x₂ · x₃ + 0
[leq#2^#(x₁, x₂)]	=	2 · x₁ · x₂ + 0
[main^#(x₁)]	=	2 + 2 · x₁ + 1 · x₁ · x₁
[0]	=	0
[True]	=	0
[S(x₁)]	=	2 + 1 · x₁
[False]	=	0
[insert_ord(x₁)]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[leq]	=	0

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

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

1.1.1.1.1.1.1 Rule Shifting

The rules

insert_ord#2^#(leq,z0,Cons(z1,z2))	→	c5(cond_insert_ord_x_ys_1^#(leq#2(z0,z1),z0,z1,z2),leq#2^#(z0,z1))	(22)
leq#2^#(0,z0)	→	c6	(24)
leq#2^#(S(z0),0)	→	c7	(26)

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
[fold#3(x₁, x₂)]	=	2 · x₂ + 0
[insert_ord#2(x₁, x₂, x₃)]	=	1 + 1 · x₃
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	2 + 1 · x₄
[leq#2(x₁, x₂)]	=	0
[fold#3^#(x₁, x₂)]	=	2 · x₂ · x₂ + 0
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	1 + 2 · x₄
[insert_ord#2^#(x₁, x₂, x₃)]	=	1 + 2 · x₃
[leq#2^#(x₁, x₂)]	=	1
[main^#(x₁)]	=	2 + 2 · x₁ + 2 · x₁ · x₁
[0]	=	0
[True]	=	0
[S(x₁)]	=	0
[False]	=	0
[insert_ord(x₁)]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	1 + 1 · x₂
[leq]	=	0

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

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

1.1.1.1.1.1.1.1 Rule Shifting

The rules

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

→

c3(insert_ord#2^#(leq,z0,z2))

(18)

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
[fold#3(x₁, x₂)]	=	2 · x₂ + 0
[insert_ord#2(x₁, x₂, x₃)]	=	1 + 1 · x₃
[cond_insert_ord_x_ys_1(x₁,...,x₄)]	=	2 + 1 · x₄
[leq#2(x₁, x₂)]	=	0
[fold#3^#(x₁, x₂)]	=	2 · x₂ + 0 + 2 · x₂ · x₂
[cond_insert_ord_x_ys_1^#(x₁,...,x₄)]	=	2 + 2 · x₄
[insert_ord#2^#(x₁, x₂, x₃)]	=	2 · x₃ + 0
[leq#2^#(x₁, x₂)]	=	0
[main^#(x₁)]	=	2 + 2 · x₁ + 2 · x₁ · x₁
[0]	=	0
[True]	=	0
[S(x₁)]	=	0
[False]	=	0
[insert_ord(x₁)]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	1 + 1 · x₂
[leq]	=	0

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

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

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