Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex26_Luc03b_FR)

The rewrite relation of the following TRS is considered.

terms(N)	→	cons(recip(sqr(N)),n__terms(n__s(N)))	(1)
sqr(0)	→	0	(2)
sqr(s(X))	→	s(n__add(n__sqr(activate(X)),n__dbl(activate(X))))	(3)
dbl(0)	→	0	(4)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(5)
add(0,X)	→	X	(6)
add(s(X),Y)	→	s(n__add(activate(X),Y))	(7)
first(0,X)	→	nil	(8)
first(s(X),cons(Y,Z))	→	cons(Y,n__first(activate(X),activate(Z)))	(9)
terms(X)	→	n__terms(X)	(10)
s(X)	→	n__s(X)	(11)
add(X1,X2)	→	n__add(X1,X2)	(12)
sqr(X)	→	n__sqr(X)	(13)
dbl(X)	→	n__dbl(X)	(14)
first(X1,X2)	→	n__first(X1,X2)	(15)
activate(n__terms(X))	→	terms(activate(X))	(16)
activate(n__s(X))	→	s(X)	(17)
activate(n__add(X1,X2))	→	add(activate(X1),activate(X2))	(18)
activate(n__sqr(X))	→	sqr(activate(X))	(19)
activate(n__dbl(X))	→	dbl(activate(X))	(20)
activate(n__first(X1,X2))	→	first(activate(X1),activate(X2))	(21)
activate(X)	→	X	(22)

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)	(23)
add^#(s(X),Y)	→	activate^#(X)	(24)
activate^#(n__first(X1,X2))	→	activate^#(X1)	(25)
activate^#(n__s(X))	→	s^#(X)	(26)
activate^#(n__sqr(X))	→	activate^#(X)	(27)
activate^#(n__add(X1,X2))	→	activate^#(X2)	(28)
activate^#(n__first(X1,X2))	→	first^#(activate(X1),activate(X2))	(29)
activate^#(n__first(X1,X2))	→	activate^#(X2)	(30)
terms^#(N)	→	sqr^#(N)	(31)
dbl^#(s(X))	→	s^#(n__s(n__dbl(activate(X))))	(32)
activate^#(n__sqr(X))	→	sqr^#(activate(X))	(33)
add^#(s(X),Y)	→	s^#(n__add(activate(X),Y))	(34)
activate^#(n__add(X1,X2))	→	activate^#(X1)	(35)
sqr^#(s(X))	→	s^#(n__add(n__sqr(activate(X)),n__dbl(activate(X))))	(36)
sqr^#(s(X))	→	activate^#(X)	(37)
activate^#(n__add(X1,X2))	→	add^#(activate(X1),activate(X2))	(38)
activate^#(n__terms(X))	→	activate^#(X)	(39)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(40)
first^#(s(X),cons(Y,Z))	→	activate^#(X)	(41)
dbl^#(s(X))	→	activate^#(X)	(42)
activate^#(n__terms(X))	→	terms^#(activate(X))	(43)
activate^#(n__dbl(X))	→	activate^#(X)	(44)
sqr^#(s(X))	→	activate^#(X)	(37)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

sqr^#(s(X))	→	activate^#(X)	(37)
activate^#(n__dbl(X))	→	activate^#(X)	(44)
activate^#(n__first(X1,X2))	→	activate^#(X2)	(30)
activate^#(n__terms(X))	→	terms^#(activate(X))	(43)
activate^#(n__first(X1,X2))	→	first^#(activate(X1),activate(X2))	(29)
dbl^#(s(X))	→	activate^#(X)	(42)
first^#(s(X),cons(Y,Z))	→	activate^#(X)	(41)
activate^#(n__add(X1,X2))	→	activate^#(X2)	(28)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(40)
activate^#(n__terms(X))	→	activate^#(X)	(39)
activate^#(n__add(X1,X2))	→	add^#(activate(X1),activate(X2))	(38)
activate^#(n__sqr(X))	→	activate^#(X)	(27)
activate^#(n__first(X1,X2))	→	activate^#(X1)	(25)
sqr^#(s(X))	→	activate^#(X)	(37)
add^#(s(X),Y)	→	activate^#(X)	(24)
activate^#(n__add(X1,X2))	→	activate^#(X1)	(35)
activate^#(n__sqr(X))	→	sqr^#(activate(X))	(33)
first^#(s(X),cons(Y,Z))	→	activate^#(Z)	(23)
terms^#(N)	→	sqr^#(N)	(31)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[n__sqr(x₁)]	=	x₁ + 3
[n__first(x₁, x₂)]	=	max(x₁ + 20541, x₂ + 20539, 0)
[recip(x₁)]	=	x₁ + 0
[activate(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 2
[dbl^#(x₁)]	=	x₁ + 26287
[terms^#(x₁)]	=	x₁ + 26288
[activate^#(x₁)]	=	x₁ + 26286
[n__add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[n__s(x₁)]	=	x₁ + 0
[sqr^#(x₁)]	=	x₁ + 26287
[n__dbl(x₁)]	=	x₁ + 2
[0]	=	9227
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	max(x₁ + 46826, x₂ + 46824, 0)
[nil]	=	20540
[first(x₁, x₂)]	=	max(x₁ + 20541, x₂ + 20539, 0)
[n__terms(x₁)]	=	x₁ + 3
[cons(x₁, x₂)]	=	max(x₂ + 0, 0)
[add^#(x₁, x₂)]	=	max(x₁ + 26286, 0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[sqr(x₁)]	=	x₁ + 3
[terms(x₁)]	=	x₁ + 3

together with the usable rules

activate(n__add(X1,X2))	→	add(activate(X1),activate(X2))	(18)
dbl(0)	→	0	(4)
first(X1,X2)	→	n__first(X1,X2)	(15)
first(0,X)	→	nil	(8)
terms(N)	→	cons(recip(sqr(N)),n__terms(n__s(N)))	(1)
sqr(s(X))	→	s(n__add(n__sqr(activate(X)),n__dbl(activate(X))))	(3)
activate(n__terms(X))	→	terms(activate(X))	(16)
activate(n__first(X1,X2))	→	first(activate(X1),activate(X2))	(21)
activate(n__sqr(X))	→	sqr(activate(X))	(19)
activate(n__s(X))	→	s(X)	(17)
activate(X)	→	X	(22)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(5)
terms(X)	→	n__terms(X)	(10)
add(s(X),Y)	→	s(n__add(activate(X),Y))	(7)
activate(n__dbl(X))	→	dbl(activate(X))	(20)
dbl(X)	→	n__dbl(X)	(14)
add(X1,X2)	→	n__add(X1,X2)	(12)
s(X)	→	n__s(X)	(11)
first(s(X),cons(Y,Z))	→	cons(Y,n__first(activate(X),activate(Z)))	(9)
sqr(X)	→	n__sqr(X)	(13)
add(0,X)	→	X	(6)
sqr(0)	→	0	(2)

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

sqr^#(s(X))	→	activate^#(X)	(37)
activate^#(n__dbl(X))	→	activate^#(X)	(44)
activate^#(n__first(X1,X2))	→	activate^#(X2)	(30)
activate^#(n__terms(X))	→	terms^#(activate(X))	(43)
activate^#(n__first(X1,X2))	→	first^#(activate(X1),activate(X2))	(29)
dbl^#(s(X))	→	activate^#(X)	(42)
first^#(s(X),cons(Y,Z))	→	activate^#(X)	(41)
activate^#(n__add(X1,X2))	→	activate^#(X2)	(28)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(40)
activate^#(n__terms(X))	→	activate^#(X)	(39)
activate^#(n__sqr(X))	→	activate^#(X)	(27)
activate^#(n__first(X1,X2))	→	activate^#(X1)	(25)
sqr^#(s(X))	→	activate^#(X)	(37)
activate^#(n__sqr(X))	→	sqr^#(activate(X))	(33)
first^#(s(X),cons(Y,Z))	→	activate^#(Z)	(23)
terms^#(N)	→	sqr^#(N)	(31)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

activate^#(n__add(X1,X2))	→	activate^#(X1)	(35)
activate^#(n__add(X1,X2))	→	add^#(activate(X1),activate(X2))	(38)
add^#(s(X),Y)	→	activate^#(X)	(24)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(recip)	=	1
π(activate)	=	1
π(dbl^#)	=	1
π(activate^#)	=	1
π(first^#)	=	1
π(cons)	=	2
π(add^#)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(s)	=	1	status(s)	=	[1]	list-extension(s)	=	Lex
prec(n__sqr)	=	4	status(n__sqr)	=	[1]	list-extension(n__sqr)	=	Lex
prec(n__first)	=	1	status(n__first)	=	[]	list-extension(n__first)	=	Lex
prec(dbl)	=	3	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(terms^#)	=	0	status(terms^#)	=	[]	list-extension(terms^#)	=	Lex
prec(n__add)	=	2	status(n__add)	=	[2, 1]	list-extension(n__add)	=	Lex
prec(n__s)	=	1	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(sqr^#)	=	0	status(sqr^#)	=	[]	list-extension(sqr^#)	=	Lex
prec(n__dbl)	=	3	status(n__dbl)	=	[1]	list-extension(n__dbl)	=	Lex
prec(0)	=	4	status(0)	=	[]	list-extension(0)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(nil)	=	1	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(first)	=	1	status(first)	=	[]	list-extension(first)	=	Lex
prec(n__terms)	=	4	status(n__terms)	=	[]	list-extension(n__terms)	=	Lex
prec(add)	=	2	status(add)	=	[2, 1]	list-extension(add)	=	Lex
prec(sqr)	=	4	status(sqr)	=	[1]	list-extension(sqr)	=	Lex
prec(terms)	=	4	status(terms)	=	[]	list-extension(terms)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[n__sqr(x₁)]	=	x₁ + 0
[n__first(x₁, x₂)]	=	max(0)
[dbl(x₁)]	=	x₁ + 0
[terms^#(x₁)]	=	0
[n__add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[sqr^#(x₁)]	=	0
[n__dbl(x₁)]	=	x₁ + 0
[0]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[first(x₁, x₂)]	=	max(0)
[n__terms(x₁)]	=	0
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[sqr(x₁)]	=	x₁ + 0
[terms(x₁)]	=	0

together with the usable rules

activate(n__add(X1,X2))	→	add(activate(X1),activate(X2))	(18)
dbl(0)	→	0	(4)
first(X1,X2)	→	n__first(X1,X2)	(15)
first(0,X)	→	nil	(8)
terms(N)	→	cons(recip(sqr(N)),n__terms(n__s(N)))	(1)
sqr(s(X))	→	s(n__add(n__sqr(activate(X)),n__dbl(activate(X))))	(3)
activate(n__terms(X))	→	terms(activate(X))	(16)
activate(n__first(X1,X2))	→	first(activate(X1),activate(X2))	(21)
activate(n__sqr(X))	→	sqr(activate(X))	(19)
activate(n__s(X))	→	s(X)	(17)
activate(X)	→	X	(22)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(5)
terms(X)	→	n__terms(X)	(10)
add(s(X),Y)	→	s(n__add(activate(X),Y))	(7)
activate(n__dbl(X))	→	dbl(activate(X))	(20)
dbl(X)	→	n__dbl(X)	(14)
add(X1,X2)	→	n__add(X1,X2)	(12)
s(X)	→	n__s(X)	(11)
first(s(X),cons(Y,Z))	→	cons(Y,n__first(activate(X),activate(Z)))	(9)
sqr(X)	→	n__sqr(X)	(13)
add(0,X)	→	X	(6)
sqr(0)	→	0	(2)

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

activate^#(n__add(X1,X2))	→	activate^#(X1)	(35)
activate^#(n__add(X1,X2))	→	add^#(activate(X1),activate(X2))	(38)
add^#(s(X),Y)	→	activate^#(X)	(24)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.