Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_AG01/#4.36)

The rewrite relation of the following TRS is considered.

eq(0,0)	→	true	(1)
eq(0,s(m))	→	false	(2)
eq(s(n),0)	→	false	(3)
eq(s(n),s(m))	→	eq(n,m)	(4)
le(0,m)	→	true	(5)
le(s(n),0)	→	false	(6)
le(s(n),s(m))	→	le(n,m)	(7)
min(cons(0,nil))	→	0	(8)
min(cons(s(n),nil))	→	s(n)	(9)
min(cons(n,cons(m,x)))	→	if_min(le(n,m),cons(n,cons(m,x)))	(10)
if_min(true,cons(n,cons(m,x)))	→	min(cons(n,x))	(11)
if_min(false,cons(n,cons(m,x)))	→	min(cons(m,x))	(12)
replace(n,m,nil)	→	nil	(13)
replace(n,m,cons(k,x))	→	if_replace(eq(n,k),n,m,cons(k,x))	(14)
if_replace(true,n,m,cons(k,x))	→	cons(m,x)	(15)
if_replace(false,n,m,cons(k,x))	→	cons(k,replace(n,m,x))	(16)
sort(nil)	→	nil	(17)
sort(cons(n,x))	→	cons(min(cons(n,x)),sort(replace(min(cons(n,x)),n,x)))	(18)

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.

if_min^#(false,cons(n,cons(m,x)))	→	min^#(cons(m,x))	(19)
min^#(cons(n,cons(m,x)))	→	if_min^#(le(n,m),cons(n,cons(m,x)))	(20)
sort^#(cons(n,x))	→	min^#(cons(n,x))	(21)
eq^#(s(n),s(m))	→	eq^#(n,m)	(22)
sort^#(cons(n,x))	→	sort^#(replace(min(cons(n,x)),n,x))	(23)
sort^#(cons(n,x))	→	replace^#(min(cons(n,x)),n,x)	(24)
min^#(cons(n,cons(m,x)))	→	le^#(n,m)	(25)
sort^#(cons(n,x))	→	min^#(cons(n,x))	(21)
le^#(s(n),s(m))	→	le^#(n,m)	(26)
replace^#(n,m,cons(k,x))	→	if_replace^#(eq(n,k),n,m,cons(k,x))	(27)
if_min^#(true,cons(n,cons(m,x)))	→	min^#(cons(n,x))	(28)
if_replace^#(false,n,m,cons(k,x))	→	replace^#(n,m,x)	(29)
replace^#(n,m,cons(k,x))	→	eq^#(n,k)	(30)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

sort^#(cons(n,x))

→

sort^#(replace(min(cons(n,x)),n,x))

(23)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	x₁ + 30952
[le^#(x₁, x₂)]	=	0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	1
[false]	=	2
[min^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sort^#(x₁)]	=	x₁ + 0
[0]	=	30952
[if_replace(x₁,...,x₄)]	=	x₃ + x₄ + 1424
[nil]	=	1
[sort(x₁)]	=	0
[replace^#(x₁, x₂, x₃)]	=	0
[if_replace^#(x₁,...,x₄)]	=	0
[min(x₁)]	=	30951
[cons(x₁, x₂)]	=	x₁ + x₂ + 1425
[if_min(x₁, x₂)]	=	x₂ + 0
[replace(x₁, x₂, x₃)]	=	x₂ + x₃ + 1424

together with the usable rules

if_replace(true,n,m,cons(k,x))	→	cons(m,x)	(15)
if_replace(false,n,m,cons(k,x))	→	cons(k,replace(n,m,x))	(16)
le(0,m)	→	true	(5)
le(s(n),s(m))	→	le(n,m)	(7)
replace(n,m,cons(k,x))	→	if_replace(eq(n,k),n,m,cons(k,x))	(14)
replace(n,m,nil)	→	nil	(13)
le(s(n),0)	→	false	(6)

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

sort^#(cons(n,x))

→

sort^#(replace(min(cons(n,x)),n,x))

(23)

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

if_replace^#(false,n,m,cons(k,x))	→	replace^#(n,m,x)	(29)
replace^#(n,m,cons(k,x))	→	if_replace^#(eq(n,k),n,m,cons(k,x))	(27)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	x₁ + 30952
[le^#(x₁, x₂)]	=	0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	1
[false]	=	2
[min^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sort^#(x₁)]	=	x₁ + 0
[0]	=	6
[if_replace(x₁,...,x₄)]	=	x₃ + x₄ + 17678
[nil]	=	1
[sort(x₁)]	=	0
[replace^#(x₁, x₂, x₃)]	=	x₃ + 1
[if_replace^#(x₁,...,x₄)]	=	x₄ + 0
[min(x₁)]	=	5
[cons(x₁, x₂)]	=	x₂ + 2
[if_min(x₁, x₂)]	=	x₂ + 0
[replace(x₁, x₂, x₃)]	=	x₂ + x₃ + 17678

together with the usable rules

if_replace(true,n,m,cons(k,x))	→	cons(m,x)	(15)
if_replace(false,n,m,cons(k,x))	→	cons(k,replace(n,m,x))	(16)
le(0,m)	→	true	(5)
le(s(n),s(m))	→	le(n,m)	(7)
replace(n,m,cons(k,x))	→	if_replace(eq(n,k),n,m,cons(k,x))	(14)
replace(n,m,nil)	→	nil	(13)
le(s(n),0)	→	false	(6)

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

if_replace^#(false,n,m,cons(k,x))	→	replace^#(n,m,x)	(29)
replace^#(n,m,cons(k,x))	→	if_replace^#(eq(n,k),n,m,cons(k,x))	(27)

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

eq^#(s(n),s(m))

→

eq^#(n,m)

(22)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	x₁ + 30952
[le^#(x₁, x₂)]	=	0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	1
[false]	=	2
[min^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	x₂ + 0
[sort^#(x₁)]	=	x₁ + 0
[0]	=	6
[if_replace(x₁,...,x₄)]	=	x₃ + x₄ + 17678
[nil]	=	1
[sort(x₁)]	=	0
[replace^#(x₁, x₂, x₃)]	=	1
[if_replace^#(x₁,...,x₄)]	=	0
[min(x₁)]	=	5
[cons(x₁, x₂)]	=	x₂ + 1
[if_min(x₁, x₂)]	=	x₂ + 2
[replace(x₁, x₂, x₃)]	=	x₂ + x₃ + 17678

together with the usable rules

if_replace(true,n,m,cons(k,x))	→	cons(m,x)	(15)
if_replace(false,n,m,cons(k,x))	→	cons(k,replace(n,m,x))	(16)
le(0,m)	→	true	(5)
le(s(n),s(m))	→	le(n,m)	(7)
replace(n,m,cons(k,x))	→	if_replace(eq(n,k),n,m,cons(k,x))	(14)
replace(n,m,nil)	→	nil	(13)
le(s(n),0)	→	false	(6)

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

eq^#(s(n),s(m))

→

eq^#(n,m)

(22)

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

if_min^#(true,cons(n,cons(m,x)))	→	min^#(cons(n,x))	(28)
min^#(cons(n,cons(m,x)))	→	if_min^#(le(n,m),cons(n,cons(m,x)))	(20)
if_min^#(false,cons(n,cons(m,x)))	→	min^#(cons(m,x))	(19)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 1
[s(x₁)]	=	x₁ + 30952
[le^#(x₁, x₂)]	=	0
[if_min^#(x₁, x₂)]	=	x₂ + 0
[eq(x₁, x₂)]	=	1
[false]	=	2
[min^#(x₁)]	=	x₁ + 1
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sort^#(x₁)]	=	x₁ + 0
[0]	=	6
[if_replace(x₁,...,x₄)]	=	x₃ + x₄ + 17678
[nil]	=	1
[sort(x₁)]	=	0
[replace^#(x₁, x₂, x₃)]	=	1
[if_replace^#(x₁,...,x₄)]	=	0
[min(x₁)]	=	5
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[if_min(x₁, x₂)]	=	x₂ + 0
[replace(x₁, x₂, x₃)]	=	x₂ + x₃ + 17678

together with the usable rules

if_replace(true,n,m,cons(k,x))	→	cons(m,x)	(15)
if_replace(false,n,m,cons(k,x))	→	cons(k,replace(n,m,x))	(16)
le(0,m)	→	true	(5)
le(s(n),s(m))	→	le(n,m)	(7)
replace(n,m,cons(k,x))	→	if_replace(eq(n,k),n,m,cons(k,x))	(14)
replace(n,m,nil)	→	nil	(13)
le(s(n),0)	→	false	(6)

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

if_min^#(true,cons(n,cons(m,x)))	→	min^#(cons(n,x))	(28)
min^#(cons(n,cons(m,x)))	→	if_min^#(le(n,m),cons(n,cons(m,x)))	(20)
if_min^#(false,cons(n,cons(m,x)))	→	min^#(cons(m,x))	(19)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

le^#(s(n),s(m))

→

le^#(n,m)

(26)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 1
[s(x₁)]	=	x₁ + 30952
[le^#(x₁, x₂)]	=	x₂ + 0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	1
[false]	=	2
[min^#(x₁)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sort^#(x₁)]	=	x₁ + 0
[0]	=	1684
[if_replace(x₁,...,x₄)]	=	x₃ + x₄ + 17678
[nil]	=	1
[sort(x₁)]	=	0
[replace^#(x₁, x₂, x₃)]	=	1
[if_replace^#(x₁,...,x₄)]	=	0
[min(x₁)]	=	1683
[cons(x₁, x₂)]	=	x₁ + x₂ + 841
[if_min(x₁, x₂)]	=	x₂ + 0
[replace(x₁, x₂, x₃)]	=	x₂ + x₃ + 17678

together with the usable rules

if_replace(true,n,m,cons(k,x))	→	cons(m,x)	(15)
if_replace(false,n,m,cons(k,x))	→	cons(k,replace(n,m,x))	(16)
le(0,m)	→	true	(5)
le(s(n),s(m))	→	le(n,m)	(7)
replace(n,m,cons(k,x))	→	if_replace(eq(n,k),n,m,cons(k,x))	(14)
replace(n,m,nil)	→	nil	(13)
le(s(n),0)	→	false	(6)

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

le^#(s(n),s(m))

→

le^#(n,m)

(26)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.