Certification Problem

Input (TPDB TRS_Standard/SK90/4.27)

The rewrite relation of the following TRS is considered.

int(0,0)	→	.(0,nil)	(1)
int(0,s(y))	→	.(0,int(s(0),s(y)))	(2)
int(s(x),0)	→	nil	(3)
int(s(x),s(y))	→	int_list(int(x,y))	(4)
int_list(nil)	→	nil	(5)
int_list(.(x,y))	→	.(s(x),int_list(y))	(6)

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.

int_list^#(.(x,y))	→	int_list^#(y)	(7)
int^#(s(x),s(y))	→	int_list^#(int(x,y))	(8)
int^#(0,s(y))	→	int^#(s(0),s(y))	(9)
int^#(s(x),s(y))	→	int^#(x,y)	(10)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

int^#(s(x),s(y))	→	int^#(x,y)	(10)
int^#(0,s(y))	→	int^#(s(0),s(y))	(9)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[int_list^#(x₁)]	=	0
[0]	=	28958
[int_list(x₁)]	=	0
[nil]	=	0
[int(x₁, x₂)]	=	0
[.(x₁, x₂)]	=	0
[int^#(x₁, x₂)]	=	x₂ + 0

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

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

→

int^#(x,y)

(10)

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

int_list^#(.(x,y))

→

int_list^#(y)

(7)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	1
[int_list^#(x₁)]	=	x₁ + 0
[0]	=	28958
[int_list(x₁)]	=	0
[nil]	=	0
[int(x₁, x₂)]	=	0
[.(x₁, x₂)]	=	x₂ + 1
[int^#(x₁, x₂)]	=	0

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

int_list^#(.(x,y))

→

int_list^#(y)

(7)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.