Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex3_2_Luc97_GM)

The rewrite relation of the following TRS is considered.

a__dbl(0)	→	0	(1)
a__dbl(s(X))	→	s(s(dbl(X)))	(2)
a__dbls(nil)	→	nil	(3)
a__dbls(cons(X,Y))	→	cons(dbl(X),dbls(Y))	(4)
a__sel(0,cons(X,Y))	→	mark(X)	(5)
a__sel(s(X),cons(Y,Z))	→	a__sel(mark(X),mark(Z))	(6)
a__indx(nil,X)	→	nil	(7)
a__indx(cons(X,Y),Z)	→	cons(sel(X,Z),indx(Y,Z))	(8)
a__from(X)	→	cons(X,from(s(X)))	(9)
mark(dbl(X))	→	a__dbl(mark(X))	(10)
mark(dbls(X))	→	a__dbls(mark(X))	(11)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
mark(indx(X1,X2))	→	a__indx(mark(X1),X2)	(13)
mark(from(X))	→	a__from(X)	(14)
mark(0)	→	0	(15)
mark(s(X))	→	s(X)	(16)
mark(nil)	→	nil	(17)
mark(cons(X1,X2))	→	cons(X1,X2)	(18)
a__dbl(X)	→	dbl(X)	(19)
a__dbls(X)	→	dbls(X)	(20)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
a__indx(X1,X2)	→	indx(X1,X2)	(22)
a__from(X)	→	from(X)	(23)

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.

a__sel^#(s(X),cons(Y,Z))	→	mark^#(X)	(24)
mark^#(dbls(X))	→	a__dbls^#(mark(X))	(25)
mark^#(dbl(X))	→	mark^#(X)	(26)
mark^#(sel(X1,X2))	→	mark^#(X1)	(27)
mark^#(from(X))	→	a__from^#(X)	(28)
mark^#(dbl(X))	→	a__dbl^#(mark(X))	(29)
a__sel^#(0,cons(X,Y))	→	mark^#(X)	(30)
mark^#(dbls(X))	→	mark^#(X)	(31)
mark^#(sel(X1,X2))	→	mark^#(X2)	(32)
mark^#(indx(X1,X2))	→	mark^#(X1)	(33)
a__sel^#(s(X),cons(Y,Z))	→	mark^#(Z)	(34)
a__sel^#(s(X),cons(Y,Z))	→	a__sel^#(mark(X),mark(Z))	(35)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(36)
mark^#(indx(X1,X2))	→	a__indx^#(mark(X1),X2)	(37)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__sel^#(0,cons(X,Y))	→	mark^#(X)	(30)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(36)
a__sel^#(s(X),cons(Y,Z))	→	a__sel^#(mark(X),mark(Z))	(35)
a__sel^#(s(X),cons(Y,Z))	→	mark^#(Z)	(34)
mark^#(sel(X1,X2))	→	mark^#(X1)	(27)
mark^#(dbl(X))	→	mark^#(X)	(26)
mark^#(indx(X1,X2))	→	mark^#(X1)	(33)
mark^#(sel(X1,X2))	→	mark^#(X2)	(32)
mark^#(dbls(X))	→	mark^#(X)	(31)
a__sel^#(s(X),cons(Y,Z))	→	mark^#(X)	(24)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[a__from^#(x₁)]	=	0
[dbls(x₁)]	=	x₁ + 282
[a__indx(x₁, x₂)]	=	max(x₁ + 15945, x₂ + 15944, 0)
[a__from(x₁)]	=	x₁ + 5854
[a__indx^#(x₁, x₂)]	=	max(0)
[dbl(x₁)]	=	x₁ + 130
[indx(x₁, x₂)]	=	max(x₁ + 15945, x₂ + 15944, 0)
[a__dbl(x₁)]	=	x₁ + 130
[a__dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 26285
[0]	=	48638
[sel(x₁, x₂)]	=	max(x₁ + 15945, x₂ + 10090, 0)
[from(x₁)]	=	x₁ + 5854
[nil]	=	15945
[a__dbl^#(x₁)]	=	0
[a__sel^#(x₁, x₂)]	=	max(x₁ + 26286, x₂ + 35232, 0)
[mark(x₁)]	=	x₁ + 0
[a__sel(x₁, x₂)]	=	max(x₁ + 15945, x₂ + 10090, 0)
[a__dbls(x₁)]	=	x₁ + 282
[cons(x₁, x₂)]	=	max(x₁ + 5854, x₂ + 0, 0)

together with the usable rules

mark(cons(X1,X2))	→	cons(X1,X2)	(18)
a__dbls(cons(X,Y))	→	cons(dbl(X),dbls(Y))	(4)
mark(0)	→	0	(15)
a__indx(cons(X,Y),Z)	→	cons(sel(X,Z),indx(Y,Z))	(8)
a__dbl(0)	→	0	(1)
a__dbls(nil)	→	nil	(3)
mark(s(X))	→	s(X)	(16)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
a__dbl(X)	→	dbl(X)	(19)
mark(nil)	→	nil	(17)
a__indx(X1,X2)	→	indx(X1,X2)	(22)
a__sel(0,cons(X,Y))	→	mark(X)	(5)
mark(dbl(X))	→	a__dbl(mark(X))	(10)
a__indx(nil,X)	→	nil	(7)
a__dbls(X)	→	dbls(X)	(20)
mark(from(X))	→	a__from(X)	(14)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
a__from(X)	→	from(X)	(23)
mark(dbls(X))	→	a__dbls(mark(X))	(11)
a__from(X)	→	cons(X,from(s(X)))	(9)
mark(indx(X1,X2))	→	a__indx(mark(X1),X2)	(13)
a__sel(s(X),cons(Y,Z))	→	a__sel(mark(X),mark(Z))	(6)
a__dbl(s(X))	→	s(s(dbl(X)))	(2)

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

a__sel^#(0,cons(X,Y))	→	mark^#(X)	(30)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(36)
a__sel^#(s(X),cons(Y,Z))	→	mark^#(Z)	(34)
mark^#(sel(X1,X2))	→	mark^#(X1)	(27)
mark^#(dbl(X))	→	mark^#(X)	(26)
mark^#(indx(X1,X2))	→	mark^#(X1)	(33)
mark^#(sel(X1,X2))	→	mark^#(X2)	(32)
mark^#(dbls(X))	→	mark^#(X)	(31)
a__sel^#(s(X),cons(Y,Z))	→	mark^#(X)	(24)

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

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

→

a__sel^#(mark(X),mark(Z))

(35)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__dbls^#)	=	1
π(mark)	=	1

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

prec(s)	=	2		status(s)	=	[1]		list-extension(s)	=	Lex
prec(a__from^#)	=	0		status(a__from^#)	=	[]		list-extension(a__from^#)	=	Lex
prec(dbls)	=	4		status(dbls)	=	[1]		list-extension(dbls)	=	Lex
prec(a__indx)	=	5		status(a__indx)	=	[]		list-extension(a__indx)	=	Lex
prec(a__from)	=	4		status(a__from)	=	[1]		list-extension(a__from)	=	Lex
prec(a__indx^#)	=	0		status(a__indx^#)	=	[]		list-extension(a__indx^#)	=	Lex
prec(dbl)	=	3		status(dbl)	=	[1]		list-extension(dbl)	=	Lex
prec(indx)	=	5		status(indx)	=	[]		list-extension(indx)	=	Lex
prec(a__dbl)	=	3		status(a__dbl)	=	[1]		list-extension(a__dbl)	=	Lex
prec(mark^#)	=	0		status(mark^#)	=	[]		list-extension(mark^#)	=	Lex
prec(0)	=	3		status(0)	=	[]		list-extension(0)	=	Lex
prec(sel)	=	6		status(sel)	=	[]		list-extension(sel)	=	Lex
prec(from)	=	4		status(from)	=	[1]		list-extension(from)	=	Lex
prec(nil)	=	0		status(nil)	=	[]		list-extension(nil)	=	Lex
prec(a__dbl^#)	=	0		status(a__dbl^#)	=	[]		list-extension(a__dbl^#)	=	Lex
prec(a__sel^#)	=	0		status(a__sel^#)	=	[1]		list-extension(a__sel^#)	=	Lex
prec(a__sel)	=	6		status(a__sel)	=	[]		list-extension(a__sel)	=	Lex
prec(a__dbls)	=	4		status(a__dbls)	=	[1]		list-extension(a__dbls)	=	Lex
prec(cons)	=	4		status(cons)	=	[1]		list-extension(cons)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[a__from^#(x₁)]	=	1
[dbls(x₁)]	=	x₁ + 19455
[a__indx(x₁, x₂)]	=	x₂ + 19453
[a__from(x₁)]	=	x₁ + 9728
[a__indx^#(x₁, x₂)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 9727
[indx(x₁, x₂)]	=	x₂ + 19453
[a__dbl(x₁)]	=	x₁ + 9727
[mark^#(x₁)]	=	1
[0]	=	1
[sel(x₁, x₂)]	=	x₂ + 9726
[from(x₁)]	=	x₁ + 9728
[nil]	=	0
[a__dbl^#(x₁)]	=	1
[a__sel^#(x₁, x₂)]	=	x₁ + 0
[a__sel(x₁, x₂)]	=	x₂ + 9726
[a__dbls(x₁)]	=	x₁ + 19455
[cons(x₁, x₂)]	=	max(x₁ + 9727, x₂ + 0, 0)

together with the usable rules

mark(cons(X1,X2))	→	cons(X1,X2)	(18)
a__dbls(cons(X,Y))	→	cons(dbl(X),dbls(Y))	(4)
mark(0)	→	0	(15)
a__indx(cons(X,Y),Z)	→	cons(sel(X,Z),indx(Y,Z))	(8)
a__dbl(0)	→	0	(1)
a__dbls(nil)	→	nil	(3)
mark(s(X))	→	s(X)	(16)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
a__dbl(X)	→	dbl(X)	(19)
mark(nil)	→	nil	(17)
a__indx(X1,X2)	→	indx(X1,X2)	(22)
a__sel(0,cons(X,Y))	→	mark(X)	(5)
mark(dbl(X))	→	a__dbl(mark(X))	(10)
a__indx(nil,X)	→	nil	(7)
a__dbls(X)	→	dbls(X)	(20)
mark(from(X))	→	a__from(X)	(14)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
a__from(X)	→	from(X)	(23)
mark(dbls(X))	→	a__dbls(mark(X))	(11)
a__from(X)	→	cons(X,from(s(X)))	(9)
mark(indx(X1,X2))	→	a__indx(mark(X1),X2)	(13)
a__sel(s(X),cons(Y,Z))	→	a__sel(mark(X),mark(Z))	(6)
a__dbl(s(X))	→	s(s(dbl(X)))	(2)

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

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

→

a__sel^#(mark(X),mark(Z))

(35)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.