Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex2_Luc02a_Z)

The rewrite relation of the following TRS is considered.

terms(N)	→	cons(recip(sqr(N)),n__terms(s(N)))	(1)
sqr(0)	→	0	(2)
sqr(s(X))	→	s(add(sqr(X),dbl(X)))	(3)
dbl(0)	→	0	(4)
dbl(s(X))	→	s(s(dbl(X)))	(5)
add(0,X)	→	X	(6)
add(s(X),Y)	→	s(add(X,Y))	(7)
first(0,X)	→	nil	(8)
first(s(X),cons(Y,Z))	→	cons(Y,n__first(X,activate(Z)))	(9)
terms(X)	→	n__terms(X)	(10)
first(X1,X2)	→	n__first(X1,X2)	(11)
activate(n__terms(X))	→	terms(X)	(12)
activate(n__first(X1,X2))	→	first(X1,X2)	(13)
activate(X)	→	X	(14)

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.

first^#(s(X),cons(Y,Z))	→	activate^#(Z)	(15)
sqr^#(s(X))	→	add^#(sqr(X),dbl(X))	(16)
terms^#(N)	→	sqr^#(N)	(17)
sqr^#(s(X))	→	sqr^#(X)	(18)
dbl^#(s(X))	→	dbl^#(X)	(19)
activate^#(n__terms(X))	→	terms^#(X)	(20)
activate^#(n__first(X1,X2))	→	first^#(X1,X2)	(21)
sqr^#(s(X))	→	dbl^#(X)	(22)
add^#(s(X),Y)	→	add^#(X,Y)	(23)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

activate^#(n__first(X1,X2))	→	first^#(X1,X2)	(21)
first^#(s(X),cons(Y,Z))	→	activate^#(Z)	(15)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	1
[n__first(x₁, x₂)]	=	x₂ + 1
[recip(x₁)]	=	0
[activate(x₁)]	=	0
[dbl(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[activate^#(x₁)]	=	x₁ + 0
[sqr^#(x₁)]	=	0
[0]	=	0
[first^#(x₁, x₂)]	=	x₂ + 0
[nil]	=	0
[first(x₁, x₂)]	=	0
[n__terms(x₁)]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	0
[terms(x₁)]	=	0

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

activate^#(n__first(X1,X2))	→	first^#(X1,X2)	(21)
first^#(s(X),cons(Y,Z))	→	activate^#(Z)	(15)

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

sqr^#(s(X))

→

sqr^#(X)

(18)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[n__first(x₁, x₂)]	=	1
[recip(x₁)]	=	0
[activate(x₁)]	=	0
[dbl(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[activate^#(x₁)]	=	0
[sqr^#(x₁)]	=	x₁ + 0
[0]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[first(x₁, x₂)]	=	0
[n__terms(x₁)]	=	0
[cons(x₁, x₂)]	=	1
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	0
[terms(x₁)]	=	0

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

sqr^#(s(X))

→

sqr^#(X)

(18)

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

add^#(s(X),Y)

→

add^#(X,Y)

(23)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[n__first(x₁, x₂)]	=	1
[recip(x₁)]	=	0
[activate(x₁)]	=	0
[dbl(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[activate^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[0]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[first(x₁, x₂)]	=	0
[n__terms(x₁)]	=	0
[cons(x₁, x₂)]	=	1
[add^#(x₁, x₂)]	=	x₁ + 0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	0
[terms(x₁)]	=	0

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

add^#(s(X),Y)

→

add^#(X,Y)

(23)

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

dbl^#(s(X))

→

dbl^#(X)

(19)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[n__first(x₁, x₂)]	=	1
[recip(x₁)]	=	0
[activate(x₁)]	=	0
[dbl(x₁)]	=	0
[dbl^#(x₁)]	=	x₁ + 0
[terms^#(x₁)]	=	0
[activate^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[0]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[first(x₁, x₂)]	=	0
[n__terms(x₁)]	=	0
[cons(x₁, x₂)]	=	1
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	0
[terms(x₁)]	=	0

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

dbl^#(s(X))

→

dbl^#(X)

(19)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.