Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex3_2_Luc97_FR)

The rewrite relation of the following TRS is considered.

dbl(0)	→	0	(1)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)
dbls(nil)	→	nil	(3)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
sel(0,cons(X,Y))	→	activate(X)	(5)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
indx(nil,X)	→	nil	(7)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
s(X)	→	n__s(X)	(10)
dbl(X)	→	n__dbl(X)	(11)
dbls(X)	→	n__dbls(X)	(12)
sel(X1,X2)	→	n__sel(X1,X2)	(13)
indx(X1,X2)	→	n__indx(X1,X2)	(14)
from(X)	→	n__from(X)	(15)
activate(n__s(X))	→	s(X)	(16)
activate(n__dbl(X))	→	dbl(activate(X))	(17)
activate(n__dbls(X))	→	dbls(activate(X))	(18)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(19)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(20)
activate(n__from(X))	→	from(X)	(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.

dbl^#(s(X))	→	activate^#(X)	(23)
from^#(X)	→	activate^#(X)	(24)
activate^#(n__sel(X1,X2))	→	sel^#(activate(X1),activate(X2))	(25)
activate^#(n__indx(X1,X2))	→	activate^#(X1)	(26)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(27)
activate^#(n__dbls(X))	→	dbls^#(activate(X))	(28)
dbls^#(cons(X,Y))	→	activate^#(Y)	(29)
activate^#(n__dbl(X))	→	activate^#(X)	(30)
activate^#(n__sel(X1,X2))	→	activate^#(X1)	(31)
activate^#(n__dbls(X))	→	activate^#(X)	(32)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(33)
from^#(X)	→	activate^#(X)	(24)
sel^#(0,cons(X,Y))	→	activate^#(X)	(34)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(35)
dbls^#(cons(X,Y))	→	activate^#(X)	(36)
activate^#(n__s(X))	→	s^#(X)	(37)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(38)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(38)
activate^#(n__from(X))	→	from^#(X)	(39)
sel^#(s(X),cons(Y,Z))	→	sel^#(activate(X),activate(Z))	(40)
dbl^#(s(X))	→	s^#(n__s(n__dbl(activate(X))))	(41)
activate^#(n__indx(X1,X2))	→	indx^#(activate(X1),X2)	(42)
activate^#(n__sel(X1,X2))	→	activate^#(X2)	(43)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(44)
indx^#(cons(X,Y),Z)	→	activate^#(X)	(45)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

indx^#(cons(X,Y),Z)	→	activate^#(X)	(45)
activate^#(n__dbls(X))	→	activate^#(X)	(32)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(44)
activate^#(n__sel(X1,X2))	→	activate^#(X1)	(31)
activate^#(n__sel(X1,X2))	→	activate^#(X2)	(43)
activate^#(n__dbl(X))	→	activate^#(X)	(30)
activate^#(n__indx(X1,X2))	→	indx^#(activate(X1),X2)	(42)
dbls^#(cons(X,Y))	→	activate^#(Y)	(29)
sel^#(s(X),cons(Y,Z))	→	sel^#(activate(X),activate(Z))	(40)
activate^#(n__dbls(X))	→	dbls^#(activate(X))	(28)
activate^#(n__from(X))	→	from^#(X)	(39)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(38)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(27)
activate^#(n__indx(X1,X2))	→	activate^#(X1)	(26)
activate^#(n__sel(X1,X2))	→	sel^#(activate(X1),activate(X2))	(25)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(38)
from^#(X)	→	activate^#(X)	(24)
dbls^#(cons(X,Y))	→	activate^#(X)	(36)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(35)
sel^#(0,cons(X,Y))	→	activate^#(X)	(34)
from^#(X)	→	activate^#(X)	(24)
dbl^#(s(X))	→	activate^#(X)	(23)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(33)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 1144
[activate(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 1144
[indx(x₁, x₂)]	=	max(x₁ + 43183, x₂ + 37329, 0)
[n__indx(x₁, x₂)]	=	max(x₁ + 43183, x₂ + 37329, 0)
[n__from(x₁)]	=	x₁ + 20539
[dbl^#(x₁)]	=	x₁ + 1
[activate^#(x₁)]	=	x₁ + 0
[dbls^#(x₁)]	=	x₁ + 1
[n__dbls(x₁)]	=	x₁ + 1144
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 1144
[0]	=	1
[sel^#(x₁, x₂)]	=	max(x₁ + 9229, x₂ + 8946, 0)
[indx^#(x₁, x₂)]	=	max(x₁ + 12462, x₂ + 37328, 0)
[sel(x₁, x₂)]	=	max(x₁ + 43183, x₂ + 9228, 0)
[from(x₁)]	=	x₁ + 20539
[s^#(x₁)]	=	0
[nil]	=	37330
[n__sel(x₁, x₂)]	=	max(x₁ + 43183, x₂ + 9228, 0)
[from^#(x₁)]	=	x₁ + 20538
[cons(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)

together with the usable rules

activate(n__dbls(X))	→	dbls(activate(X))	(18)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
from(X)	→	n__from(X)	(15)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
dbl(0)	→	0	(1)
dbls(nil)	→	nil	(3)
activate(n__s(X))	→	s(X)	(16)
activate(n__from(X))	→	from(X)	(21)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(19)
activate(n__dbl(X))	→	dbl(activate(X))	(17)
activate(X)	→	X	(22)
sel(0,cons(X,Y))	→	activate(X)	(5)
s(X)	→	n__s(X)	(10)
indx(nil,X)	→	nil	(7)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(20)
indx(X1,X2)	→	n__indx(X1,X2)	(14)
dbls(X)	→	n__dbls(X)	(12)
dbl(X)	→	n__dbl(X)	(11)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
sel(X1,X2)	→	n__sel(X1,X2)	(13)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)

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

indx^#(cons(X,Y),Z)	→	activate^#(X)	(45)
activate^#(n__dbls(X))	→	activate^#(X)	(32)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(44)
activate^#(n__sel(X1,X2))	→	activate^#(X1)	(31)
activate^#(n__sel(X1,X2))	→	activate^#(X2)	(43)
activate^#(n__dbl(X))	→	activate^#(X)	(30)
activate^#(n__indx(X1,X2))	→	indx^#(activate(X1),X2)	(42)
dbls^#(cons(X,Y))	→	activate^#(Y)	(29)
activate^#(n__dbls(X))	→	dbls^#(activate(X))	(28)
activate^#(n__from(X))	→	from^#(X)	(39)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(38)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(27)
activate^#(n__indx(X1,X2))	→	activate^#(X1)	(26)
activate^#(n__sel(X1,X2))	→	sel^#(activate(X1),activate(X2))	(25)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(38)
from^#(X)	→	activate^#(X)	(24)
dbls^#(cons(X,Y))	→	activate^#(X)	(36)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(35)
sel^#(0,cons(X,Y))	→	activate^#(X)	(34)
from^#(X)	→	activate^#(X)	(24)
dbl^#(s(X))	→	activate^#(X)	(23)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(33)

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

sel^#(s(X),cons(Y,Z))

→

sel^#(activate(X),activate(Z))

(40)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(dbls)	=	1
π(activate)	=	1
π(n__dbls)	=	1
π(s^#)	=	1

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

prec(s)	=	4	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbl)	=	5	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	5	status(indx)	=	[2]	list-extension(indx)	=	Lex
prec(n__indx)	=	5	status(n__indx)	=	[2]	list-extension(n__indx)	=	Lex
prec(n__from)	=	5	status(n__from)	=	[]	list-extension(n__from)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(activate^#)	=	0	status(activate^#)	=	[]	list-extension(activate^#)	=	Lex
prec(dbls^#)	=	0	status(dbls^#)	=	[]	list-extension(dbls^#)	=	Lex
prec(n__s)	=	4	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(n__dbl)	=	5	status(n__dbl)	=	[1]	list-extension(n__dbl)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	4	status(sel^#)	=	[1]	list-extension(sel^#)	=	Lex
prec(indx^#)	=	0	status(indx^#)	=	[1, 2]	list-extension(indx^#)	=	Lex
prec(sel)	=	3	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(from)	=	5	status(from)	=	[]	list-extension(from)	=	Lex
prec(nil)	=	5	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(n__sel)	=	3	status(n__sel)	=	[]	list-extension(n__sel)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(cons)	=	2	status(cons)	=	[]	list-extension(cons)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[indx(x₁, x₂)]	=	x₁ + x₂ + 1738
[n__indx(x₁, x₂)]	=	x₁ + x₂ + 1738
[n__from(x₁)]	=	x₁ + 870
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[dbls^#(x₁)]	=	1
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	x₁ + 870
[indx^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₂ + 868
[from(x₁)]	=	x₁ + 870
[nil]	=	41990
[n__sel(x₁, x₂)]	=	x₂ + 868
[from^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 869, x₂ + 0, 0)

together with the usable rules

activate(n__dbls(X))	→	dbls(activate(X))	(18)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
from(X)	→	n__from(X)	(15)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
dbl(0)	→	0	(1)
dbls(nil)	→	nil	(3)
activate(n__s(X))	→	s(X)	(16)
activate(n__from(X))	→	from(X)	(21)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(19)
activate(n__dbl(X))	→	dbl(activate(X))	(17)
activate(X)	→	X	(22)
sel(0,cons(X,Y))	→	activate(X)	(5)
s(X)	→	n__s(X)	(10)
indx(nil,X)	→	nil	(7)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(20)
indx(X1,X2)	→	n__indx(X1,X2)	(14)
dbls(X)	→	n__dbls(X)	(12)
dbl(X)	→	n__dbl(X)	(11)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
sel(X1,X2)	→	n__sel(X1,X2)	(13)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)

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

sel^#(s(X),cons(Y,Z))

→

sel^#(activate(X),activate(Z))

(40)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.