Certification Problem

Input (TPDB TRS_Standard/SK90/4.61)

The rewrite relation of the following TRS is considered.

bsort(nil)	→	nil	(1)
bsort(.(x,y))	→	last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))	(2)
bubble(nil)	→	nil	(3)
bubble(.(x,nil))	→	.(x,nil)	(4)
bubble(.(x,.(y,z)))	→	if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))	(5)
last(nil)	→	0	(6)
last(.(x,nil))	→	x	(7)
last(.(x,.(y,z)))	→	last(.(y,z))	(8)
butlast(nil)	→	nil	(9)
butlast(.(x,nil))	→	nil	(10)
butlast(.(x,.(y,z)))	→	.(x,butlast(.(y,z)))	(11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

bsort^#(.(x,y))	→	bubble^#(.(x,y))	(12)
butlast^#(.(x,.(y,z)))	→	butlast^#(.(y,z))	(13)
last^#(.(x,.(y,z)))	→	last^#(.(y,z))	(14)
bubble^#(.(x,.(y,z)))	→	bubble^#(.(x,z))	(15)
bsort^#(.(x,y))	→	bubble^#(.(x,y))	(12)
bsort^#(.(x,y))	→	bsort^#(butlast(bubble(.(x,y))))	(16)
bsort^#(.(x,y))	→	last^#(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))	(17)
bubble^#(.(x,.(y,z)))	→	bubble^#(.(y,z))	(18)
bsort^#(.(x,y))	→	butlast^#(bubble(.(x,y)))	(19)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

bsort^#(.(x,y))

→

bsort^#(butlast(bubble(.(x,y))))

(16)

1.1.1 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

[bubble^#(x₁)]

[butlast^#(x₁)]

[<=(x₁, x₂)]

[bsort^#(x₁)]

1	0
0	0

· x₁ +

[butlast(x₁)]

0	1
0	1

· x₁ +

39790

[last^#(x₁)]

[if(x₁, x₂, x₃)]

0	1
0	0

· x₃ +

42893

[0]

[last(x₁)]

[nil]

[.(x₁, x₂)]

1	0
1	0

· x₂ +

42893

[bubble(x₁)]

0	1
0	1

· x₁ +

64777

[bsort(x₁)]

together with the usable rules

bubble(.(x,nil))	→	.(x,nil)	(4)
bubble(nil)	→	nil	(3)
bubble(.(x,.(y,z)))	→	if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))	(5)
butlast(.(x,nil))	→	nil	(10)
butlast(.(x,.(y,z)))	→	.(x,butlast(.(y,z)))	(11)
butlast(nil)	→	nil	(9)

(w.r.t. the implicit argument filter of the reduction pair), the pair

bsort^#(.(x,y))

→

bsort^#(butlast(bubble(.(x,y))))

(16)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

last^#(.(x,.(y,z)))

→

last^#(.(y,z))

(14)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[bubble^#(x₁)]	=	0
[butlast^#(x₁)]	=	0
[<=(x₁, x₂)]	=	1
[bsort^#(x₁)]	=	0
[butlast(x₁)]	=	36459
[last^#(x₁)]	=	x₁ + 0
[if(x₁, x₂, x₃)]	=	x₁ + 0
[0]	=	0
[last(x₁)]	=	0
[nil]	=	36460
[.(x₁, x₂)]	=	x₂ + 1
[bubble(x₁)]	=	36461
[bsort(x₁)]	=	0

together with the usable rules

bubble(.(x,nil))	→	.(x,nil)	(4)
bubble(nil)	→	nil	(3)
bubble(.(x,.(y,z)))	→	if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))	(5)

(w.r.t. the implicit argument filter of the reduction pair), the pair

last^#(.(x,.(y,z)))

→

last^#(.(y,z))

(14)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

butlast^#(.(x,.(y,z)))

→

butlast^#(.(y,z))

(13)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[bubble^#(x₁)]	=	0
[butlast^#(x₁)]	=	x₁ + 0
[<=(x₁, x₂)]	=	1
[bsort^#(x₁)]	=	0
[butlast(x₁)]	=	2998
[last^#(x₁)]	=	0
[if(x₁, x₂, x₃)]	=	x₁ + 0
[0]	=	0
[last(x₁)]	=	0
[nil]	=	36460
[.(x₁, x₂)]	=	x₂ + 1
[bubble(x₁)]	=	36461
[bsort(x₁)]	=	0

together with the usable rules

bubble(.(x,nil))	→	.(x,nil)	(4)
bubble(nil)	→	nil	(3)
bubble(.(x,.(y,z)))	→	if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))	(5)

(w.r.t. the implicit argument filter of the reduction pair), the pair

butlast^#(.(x,.(y,z)))

→

butlast^#(.(y,z))

(13)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

bubble^#(.(x,.(y,z)))	→	bubble^#(.(y,z))	(18)
bubble^#(.(x,.(y,z)))	→	bubble^#(.(x,z))	(15)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[bubble^#(x₁)]	=	x₁ + 0
[butlast^#(x₁)]	=	0
[<=(x₁, x₂)]	=	1
[bsort^#(x₁)]	=	0
[butlast(x₁)]	=	30205
[last^#(x₁)]	=	0
[if(x₁, x₂, x₃)]	=	x₁ + 30206
[0]	=	0
[last(x₁)]	=	0
[nil]	=	30206
[.(x₁, x₂)]	=	x₂ + 1
[bubble(x₁)]	=	30207
[bsort(x₁)]	=	0

together with the usable rules

bubble(.(x,nil))	→	.(x,nil)	(4)
bubble(nil)	→	nil	(3)
bubble(.(x,.(y,z)))	→	if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))	(5)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

bubble^#(.(x,.(y,z)))	→	bubble^#(.(y,z))	(18)
bubble^#(.(x,.(y,z)))	→	bubble^#(.(x,z))	(15)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.