Certification Problem

Input (TPDB TRS_Standard/AProVE_07/kabasci05)

The rewrite relation of the following TRS is considered.

min(x,0)	→	0	(1)
min(0,y)	→	0	(2)
min(s(x),s(y))	→	s(min(x,y))	(3)
max(x,0)	→	x	(4)
max(0,y)	→	y	(5)
max(s(x),s(y))	→	s(max(x,y))	(6)
minus(x,0)	→	x	(7)
minus(s(x),s(y))	→	s(minus(x,y))	(8)
gcd(s(x),s(y))	→	gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))	(9)
transform(x)	→	s(s(x))	(10)
transform(cons(x,y))	→	cons(cons(x,x),x)	(11)
transform(cons(x,y))	→	y	(12)
transform(s(x))	→	s(s(transform(x)))	(13)
cons(x,y)	→	y	(14)
cons(x,cons(y,s(z)))	→	cons(y,x)	(15)
cons(cons(x,z),s(y))	→	transform(x)	(16)

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.

transform^#(s(x))	→	transform^#(x)	(17)
gcd^#(s(x),s(y))	→	min^#(x,transform(y))	(18)
minus^#(s(x),s(y))	→	minus^#(x,y)	(19)
transform^#(cons(x,y))	→	cons^#(cons(x,x),x)	(20)
cons^#(cons(x,z),s(y))	→	transform^#(x)	(21)
min^#(s(x),s(y))	→	min^#(x,y)	(22)
cons^#(x,cons(y,s(z)))	→	cons^#(y,x)	(23)
gcd^#(s(x),s(y))	→	transform^#(y)	(24)
transform^#(cons(x,y))	→	cons^#(x,x)	(25)
gcd^#(s(x),s(y))	→	max^#(x,y)	(26)
gcd^#(s(x),s(y))	→	gcd^#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))	(27)
max^#(s(x),s(y))	→	max^#(x,y)	(28)
gcd^#(s(x),s(y))	→	min^#(x,y)	(29)
gcd^#(s(x),s(y))	→	minus^#(max(x,y),min(x,transform(y)))	(30)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

gcd^#(s(x),s(y))

→

gcd^#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))

(27)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 64571
[minus(x₁, x₂)]	=	max(x₁ + 1, x₂ + 58716, 0)
[gcd(x₁, x₂)]	=	max(0)
[min^#(x₁, x₂)]	=	max(0)
[transform^#(x₁)]	=	0
[0]	=	5854
[transform(x₁)]	=	64573
[max(x₁, x₂)]	=	max(x₁ + 58715, x₂ + 58713, 0)
[max^#(x₁, x₂)]	=	max(0)
[minus^#(x₁, x₂)]	=	max(0)
[min(x₁, x₂)]	=	max(x₁ + 5854, 0)
[cons(x₁, x₂)]	=	max(x₂ + 1, 0)
[gcd^#(x₁, x₂)]	=	max(x₁ + 5857, x₂ + 1, 0)

together with the usable rules

max(x,0)	→	x	(4)
minus(s(x),s(y))	→	s(minus(x,y))	(8)
min(x,0)	→	0	(1)
min(s(x),s(y))	→	s(min(x,y))	(3)
max(0,y)	→	y	(5)
minus(x,0)	→	x	(7)
max(s(x),s(y))	→	s(max(x,y))	(6)
min(0,y)	→	0	(2)

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

gcd^#(s(x),s(y))

→

gcd^#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))

(27)

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

minus^#(s(x),s(y))

→

minus^#(x,y)

(19)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 3
[minus(x₁, x₂)]	=	1
[gcd(x₁, x₂)]	=	0
[min^#(x₁, x₂)]	=	0
[transform^#(x₁)]	=	0
[0]	=	52869
[transform(x₁)]	=	5
[max(x₁, x₂)]	=	x₁ + x₂ + 36336
[max^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	x₂ + 0
[min(x₁, x₂)]	=	52868
[cons(x₁, x₂)]	=	x₂ + 1
[gcd^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

minus^#(s(x),s(y))

→

minus^#(x,y)

(19)

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

min^#(s(x),s(y))

→

min^#(x,y)

(22)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 3
[minus(x₁, x₂)]	=	1
[gcd(x₁, x₂)]	=	0
[min^#(x₁, x₂)]	=	x₂ + 0
[transform^#(x₁)]	=	0
[0]	=	2
[transform(x₁)]	=	5
[max(x₁, x₂)]	=	x₁ + x₂ + 36336
[max^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[min(x₁, x₂)]	=	1
[cons(x₁, x₂)]	=	x₂ + 1
[gcd^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

min^#(s(x),s(y))

→

min^#(x,y)

(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

max^#(s(x),s(y))

→

max^#(x,y)

(28)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 3
[minus(x₁, x₂)]	=	1
[gcd(x₁, x₂)]	=	0
[min^#(x₁, x₂)]	=	0
[transform^#(x₁)]	=	0
[0]	=	2
[transform(x₁)]	=	5
[max(x₁, x₂)]	=	x₁ + x₂ + 42004
[max^#(x₁, x₂)]	=	x₁ + x₂ + 0
[minus^#(x₁, x₂)]	=	0
[min(x₁, x₂)]	=	1
[cons(x₁, x₂)]	=	x₂ + 1
[gcd^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

max^#(s(x),s(y))

→

max^#(x,y)

(28)

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

cons^#(x,cons(y,s(z)))	→	cons^#(y,x)	(23)
cons^#(cons(x,z),s(y))	→	transform^#(x)	(21)
transform^#(cons(x,y))	→	cons^#(cons(x,x),x)	(20)
transform^#(cons(x,y))	→	cons^#(x,x)	(25)
transform^#(s(x))	→	transform^#(x)	(17)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(x₁ + 40118, x₂ + 18458, 0)
[s(x₁)]	=	x₁ + 0
[minus(x₁, x₂)]	=	max(x₁ + 46883, x₂ + 46884, 0)
[gcd(x₁, x₂)]	=	max(0)
[min^#(x₁, x₂)]	=	max(0)
[transform^#(x₁)]	=	x₁ + 61776
[0]	=	1
[transform(x₁)]	=	x₁ + 64976
[max(x₁, x₂)]	=	max(x₁ + 31893, x₂ + 1, 0)
[max^#(x₁, x₂)]	=	max(0)
[minus^#(x₁, x₂)]	=	max(0)
[min(x₁, x₂)]	=	max(x₁ + 1, 0)
[cons(x₁, x₂)]	=	max(x₁ + 43316, x₂ + 21659, 0)
[gcd^#(x₁, x₂)]	=	max(x₁ + 5857, x₂ + 1, 0)

together with the usable rules

max(x,0)	→	x	(4)
cons(x,cons(y,s(z)))	→	cons(y,x)	(15)
minus(s(x),s(y))	→	s(minus(x,y))	(8)
min(x,0)	→	0	(1)
min(s(x),s(y))	→	s(min(x,y))	(3)
cons(cons(x,z),s(y))	→	transform(x)	(16)
max(0,y)	→	y	(5)
transform(x)	→	s(s(x))	(10)
minus(x,0)	→	x	(7)
cons(x,y)	→	y	(14)
transform(cons(x,y))	→	y	(12)
transform(cons(x,y))	→	cons(cons(x,x),x)	(11)
transform(s(x))	→	s(s(transform(x)))	(13)
max(s(x),s(y))	→	s(max(x,y))	(6)
min(0,y)	→	0	(2)

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

cons^#(x,cons(y,s(z)))	→	cons^#(y,x)	(23)
cons^#(cons(x,z),s(y))	→	transform^#(x)	(21)
transform^#(cons(x,y))	→	cons^#(cons(x,x),x)	(20)
transform^#(cons(x,y))	→	cons^#(x,x)	(25)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

transform^#(s(x))

→

transform^#(x)

(17)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 3
[minus(x₁, x₂)]	=	1
[gcd(x₁, x₂)]	=	0
[min^#(x₁, x₂)]	=	0
[transform^#(x₁)]	=	x₁ + 1
[0]	=	2
[transform(x₁)]	=	4
[max(x₁, x₂)]	=	x₁ + x₂ + 38145
[max^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[min(x₁, x₂)]	=	1
[cons(x₁, x₂)]	=	2
[gcd^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

transform^#(s(x))

→

transform^#(x)

(17)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.