Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec11_1_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)
half(0)	→	0	(10)
half(s(0))	→	0	(11)
half(s(s(X)))	→	s(half(X))	(12)
half(dbl(X))	→	X	(13)
terms(X)	→	n__terms(X)	(14)
first(X1,X2)	→	n__first(X1,X2)	(15)
activate(n__terms(X))	→	terms(X)	(16)
activate(n__first(X1,X2))	→	first(X1,X2)	(17)
activate(X)	→	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.

half^#(s(s(X)))	→	half^#(X)	(19)
activate^#(n__terms(X))	→	terms^#(X)	(20)
sqr^#(s(X))	→	dbl^#(X)	(21)
sqr^#(s(X))	→	add^#(sqr(X),dbl(X))	(22)
terms^#(N)	→	sqr^#(N)	(23)
activate^#(n__first(X1,X2))	→	first^#(X1,X2)	(24)
add^#(s(X),Y)	→	add^#(X,Y)	(25)
first^#(s(X),cons(Y,Z))	→	activate^#(Z)	(26)
sqr^#(s(X))	→	sqr^#(X)	(27)
dbl^#(s(X))	→	dbl^#(X)	(28)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	1
[n__first(x₁, x₂)]	=	x₁ + x₂ + 1
[recip(x₁)]	=	0
[activate(x₁)]	=	0
[dbl(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[activate^#(x₁)]	=	x₁ + 0
[half^#(x₁)]	=	0
[half(x₁)]	=	0
[sqr^#(x₁)]	=	0
[0]	=	0
[first^#(x₁, x₂)]	=	x₁ + x₂ + 0
[nil]	=	0
[first(x₁, x₂)]	=	0
[n__terms(x₁)]	=	0
[cons(x₁, x₂)]	=	x₂ + 28958
[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

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

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)

(27)

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
[half^#(x₁)]	=	0
[half(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₂)]	=	28958
[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)

(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

dbl^#(s(X))

→

dbl^#(X)

(28)

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₁)]	=	x₁ + 0
[terms^#(x₁)]	=	0
[activate^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	0
[sqr^#(x₁)]	=	0
[0]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[first(x₁, x₂)]	=	0
[n__terms(x₁)]	=	0
[cons(x₁, x₂)]	=	28958
[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)

(28)

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

add^#(s(X),Y)

→

add^#(X,Y)

(25)

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₁)]	=	0
[terms^#(x₁)]	=	0
[activate^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	0
[sqr^#(x₁)]	=	0
[0]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[first(x₁, x₂)]	=	0
[n__terms(x₁)]	=	0
[cons(x₁, x₂)]	=	28958
[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)

(25)

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

half^#(s(s(X)))

→

half^#(X)

(19)

1.1.5 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
[half^#(x₁)]	=	x₁ + 0
[half(x₁)]	=	0
[sqr^#(x₁)]	=	0
[0]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[first(x₁, x₂)]	=	0
[n__terms(x₁)]	=	0
[cons(x₁, x₂)]	=	28958
[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

half^#(s(s(X)))

→

half^#(X)

(19)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.