Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex2_Luc02a_GM)

The rewrite relation of the following TRS is considered.

a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
a__sqr(0)	→	0	(2)
a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
a__dbl(0)	→	0	(4)
a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
a__add(0,X)	→	mark(X)	(6)
a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
a__first(0,X)	→	nil	(8)
a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
mark(terms(X))	→	a__terms(mark(X))	(10)
mark(sqr(X))	→	a__sqr(mark(X))	(11)
mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(12)
mark(dbl(X))	→	a__dbl(mark(X))	(13)
mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(14)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(15)
mark(recip(X))	→	recip(mark(X))	(16)
mark(s(X))	→	s(mark(X))	(17)
mark(0)	→	0	(18)
mark(nil)	→	nil	(19)
a__terms(X)	→	terms(X)	(20)
a__sqr(X)	→	sqr(X)	(21)
a__add(X1,X2)	→	add(X1,X2)	(22)
a__dbl(X)	→	dbl(X)	(23)
a__first(X1,X2)	→	first(X1,X2)	(24)

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.

mark^#(dbl(X))	→	a__dbl^#(mark(X))	(25)
mark^#(cons(X1,X2))	→	mark^#(X1)	(26)
mark^#(sqr(X))	→	mark^#(X)	(27)
a__add^#(s(X),Y)	→	a__add^#(mark(X),mark(Y))	(28)
mark^#(add(X1,X2))	→	mark^#(X2)	(29)
mark^#(first(X1,X2))	→	mark^#(X1)	(30)
a__sqr^#(s(X))	→	mark^#(X)	(31)
a__sqr^#(s(X))	→	a__sqr^#(mark(X))	(32)
mark^#(first(X1,X2))	→	mark^#(X2)	(33)
a__add^#(s(X),Y)	→	mark^#(X)	(34)
a__sqr^#(s(X))	→	a__dbl^#(mark(X))	(35)
mark^#(s(X))	→	mark^#(X)	(36)
mark^#(add(X1,X2))	→	a__add^#(mark(X1),mark(X2))	(37)
mark^#(first(X1,X2))	→	a__first^#(mark(X1),mark(X2))	(38)
mark^#(sqr(X))	→	a__sqr^#(mark(X))	(39)
a__terms^#(N)	→	mark^#(N)	(40)
a__sqr^#(s(X))	→	a__add^#(a__sqr(mark(X)),a__dbl(mark(X)))	(41)
a__terms^#(N)	→	a__sqr^#(mark(N))	(42)
mark^#(terms(X))	→	mark^#(X)	(43)
a__dbl^#(s(X))	→	mark^#(X)	(44)
a__sqr^#(s(X))	→	mark^#(X)	(31)
mark^#(recip(X))	→	mark^#(X)	(45)
mark^#(terms(X))	→	a__terms^#(mark(X))	(46)
mark^#(dbl(X))	→	mark^#(X)	(47)
a__add^#(0,X)	→	mark^#(X)	(48)
mark^#(add(X1,X2))	→	mark^#(X1)	(49)
a__add^#(s(X),Y)	→	mark^#(Y)	(50)
a__first^#(s(X),cons(Y,Z))	→	mark^#(Y)	(51)
a__dbl^#(s(X))	→	a__dbl^#(mark(X))	(52)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__dbl^#(s(X))	→	a__dbl^#(mark(X))	(52)
a__sqr^#(s(X))	→	a__dbl^#(mark(X))	(35)
a__first^#(s(X),cons(Y,Z))	→	mark^#(Y)	(51)
a__add^#(s(X),Y)	→	mark^#(X)	(34)
a__add^#(s(X),Y)	→	mark^#(Y)	(50)
mark^#(first(X1,X2))	→	mark^#(X2)	(33)
mark^#(add(X1,X2))	→	mark^#(X1)	(49)
a__add^#(0,X)	→	mark^#(X)	(48)
a__sqr^#(s(X))	→	a__sqr^#(mark(X))	(32)
mark^#(dbl(X))	→	mark^#(X)	(47)
a__sqr^#(s(X))	→	mark^#(X)	(31)
mark^#(terms(X))	→	a__terms^#(mark(X))	(46)
mark^#(recip(X))	→	mark^#(X)	(45)
a__sqr^#(s(X))	→	mark^#(X)	(31)
mark^#(first(X1,X2))	→	mark^#(X1)	(30)
mark^#(add(X1,X2))	→	mark^#(X2)	(29)
a__add^#(s(X),Y)	→	a__add^#(mark(X),mark(Y))	(28)
a__dbl^#(s(X))	→	mark^#(X)	(44)
mark^#(terms(X))	→	mark^#(X)	(43)
mark^#(sqr(X))	→	mark^#(X)	(27)
a__terms^#(N)	→	a__sqr^#(mark(N))	(42)
a__sqr^#(s(X))	→	a__add^#(a__sqr(mark(X)),a__dbl(mark(X)))	(41)
a__terms^#(N)	→	mark^#(N)	(40)
mark^#(sqr(X))	→	a__sqr^#(mark(X))	(39)
mark^#(first(X1,X2))	→	a__first^#(mark(X1),mark(X2))	(38)
mark^#(add(X1,X2))	→	a__add^#(mark(X1),mark(X2))	(37)
mark^#(cons(X1,X2))	→	mark^#(X1)	(26)
mark^#(dbl(X))	→	a__dbl^#(mark(X))	(25)
mark^#(s(X))	→	mark^#(X)	(36)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[a__first^#(x₁, x₂)]	=	max(x₂ + 19308, 0)
[recip(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 32287
[a__add^#(x₁, x₂)]	=	max(x₁ + 19306, x₂ + 19307, 0)
[a__add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 11799, 0)
[a__dbl(x₁)]	=	x₁ + 32287
[a__sqr(x₁)]	=	x₁ + 44086
[a__terms^#(x₁)]	=	x₁ + 63393
[mark^#(x₁)]	=	x₁ + 19306
[0]	=	8368
[nil]	=	4
[a__dbl^#(x₁)]	=	x₁ + 19307
[mark(x₁)]	=	x₁ + 0
[first(x₁, x₂)]	=	max(x₁ + 1, x₂ + 3, 0)
[a__first(x₁, x₂)]	=	max(x₁ + 1, x₂ + 3, 0)
[cons(x₁, x₂)]	=	max(x₁ + 4, 0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 11799, 0)
[sqr(x₁)]	=	x₁ + 44086
[a__terms(x₁)]	=	x₁ + 44091
[a__sqr^#(x₁)]	=	x₁ + 63392
[terms(x₁)]	=	x₁ + 44091

together with the usable rules

mark(0)	→	0	(18)
a__dbl(0)	→	0	(4)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(15)
a__first(0,X)	→	nil	(8)
a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
mark(recip(X))	→	recip(mark(X))	(16)
a__sqr(X)	→	sqr(X)	(21)
mark(nil)	→	nil	(19)
mark(s(X))	→	s(mark(X))	(17)
a__add(X1,X2)	→	add(X1,X2)	(22)
a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
mark(terms(X))	→	a__terms(mark(X))	(10)
a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
a__terms(X)	→	terms(X)	(20)
mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(14)
mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(12)
a__dbl(X)	→	dbl(X)	(23)
a__first(X1,X2)	→	first(X1,X2)	(24)
mark(sqr(X))	→	a__sqr(mark(X))	(11)
a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
mark(dbl(X))	→	a__dbl(mark(X))	(13)
a__add(0,X)	→	mark(X)	(6)
a__sqr(0)	→	0	(2)

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

a__sqr^#(s(X))	→	a__dbl^#(mark(X))	(35)
a__first^#(s(X),cons(Y,Z))	→	mark^#(Y)	(51)
a__add^#(s(X),Y)	→	mark^#(Y)	(50)
mark^#(first(X1,X2))	→	mark^#(X2)	(33)
a__add^#(0,X)	→	mark^#(X)	(48)
mark^#(dbl(X))	→	mark^#(X)	(47)
a__sqr^#(s(X))	→	mark^#(X)	(31)
mark^#(terms(X))	→	a__terms^#(mark(X))	(46)
mark^#(recip(X))	→	mark^#(X)	(45)
a__sqr^#(s(X))	→	mark^#(X)	(31)
mark^#(first(X1,X2))	→	mark^#(X1)	(30)
mark^#(add(X1,X2))	→	mark^#(X2)	(29)
a__dbl^#(s(X))	→	mark^#(X)	(44)
mark^#(terms(X))	→	mark^#(X)	(43)
mark^#(sqr(X))	→	mark^#(X)	(27)
a__terms^#(N)	→	a__sqr^#(mark(N))	(42)
a__terms^#(N)	→	mark^#(N)	(40)
mark^#(first(X1,X2))	→	a__first^#(mark(X1),mark(X2))	(38)
mark^#(cons(X1,X2))	→	mark^#(X1)	(26)
mark^#(dbl(X))	→	a__dbl^#(mark(X))	(25)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a__dbl^#(s(X))

→

a__dbl^#(mark(X))

(52)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__terms^#)	=	1
π(a__dbl^#)	=	1
π(mark)	=	1
π(a__sqr^#)	=	1

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

prec(s)	=	0	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__first^#)	=	0	status(a__first^#)	=	[2, 1]	list-extension(a__first^#)	=	Lex
prec(recip)	=	0	status(recip)	=	[1]	list-extension(recip)	=	Lex
prec(dbl)	=	1	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(a__add^#)	=	0	status(a__add^#)	=	[1, 2]	list-extension(a__add^#)	=	Lex
prec(a__add)	=	1	status(a__add)	=	[2, 1]	list-extension(a__add)	=	Lex
prec(a__dbl)	=	1	status(a__dbl)	=	[1]	list-extension(a__dbl)	=	Lex
prec(a__sqr)	=	2	status(a__sqr)	=	[1]	list-extension(a__sqr)	=	Lex
prec(mark^#)	=	0	status(mark^#)	=	[]	list-extension(mark^#)	=	Lex
prec(0)	=	3	status(0)	=	[]	list-extension(0)	=	Lex
prec(nil)	=	4	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(first)	=	4	status(first)	=	[]	list-extension(first)	=	Lex
prec(a__first)	=	4	status(a__first)	=	[]	list-extension(a__first)	=	Lex
prec(cons)	=	0	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(add)	=	1	status(add)	=	[2, 1]	list-extension(add)	=	Lex
prec(sqr)	=	2	status(sqr)	=	[1]	list-extension(sqr)	=	Lex
prec(a__terms)	=	3	status(a__terms)	=	[]	list-extension(a__terms)	=	Lex
prec(terms)	=	3	status(terms)	=	[]	list-extension(terms)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[a__first^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[recip(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[a__add^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__dbl(x₁)]	=	x₁ + 0
[a__sqr(x₁)]	=	x₁ + 0
[mark^#(x₁)]	=	0
[0]	=	0
[nil]	=	0
[first(x₁, x₂)]	=	max(0)
[a__first(x₁, x₂)]	=	max(0)
[cons(x₁, x₂)]	=	max(0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[sqr(x₁)]	=	x₁ + 0
[a__terms(x₁)]	=	0
[terms(x₁)]	=	0

together with the usable rules

mark(0)	→	0	(18)
a__dbl(0)	→	0	(4)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(15)
a__first(0,X)	→	nil	(8)
a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
mark(recip(X))	→	recip(mark(X))	(16)
a__sqr(X)	→	sqr(X)	(21)
mark(nil)	→	nil	(19)
mark(s(X))	→	s(mark(X))	(17)
a__add(X1,X2)	→	add(X1,X2)	(22)
a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
mark(terms(X))	→	a__terms(mark(X))	(10)
a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
a__terms(X)	→	terms(X)	(20)
mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(14)
mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(12)
a__dbl(X)	→	dbl(X)	(23)
a__first(X1,X2)	→	first(X1,X2)	(24)
mark(sqr(X))	→	a__sqr(mark(X))	(11)
a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
mark(dbl(X))	→	a__dbl(mark(X))	(13)
a__add(0,X)	→	mark(X)	(6)
a__sqr(0)	→	0	(2)

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

a__dbl^#(s(X))

→

a__dbl^#(mark(X))

(52)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

a__sqr^#(s(X))	→	a__sqr^#(mark(X))	(32)
a__sqr^#(s(X))	→	a__add^#(a__sqr(mark(X)),a__dbl(mark(X)))	(41)
mark^#(s(X))	→	mark^#(X)	(36)
a__add^#(s(X),Y)	→	mark^#(X)	(34)
a__add^#(s(X),Y)	→	a__add^#(mark(X),mark(Y))	(28)
mark^#(add(X1,X2))	→	mark^#(X1)	(49)
mark^#(add(X1,X2))	→	a__add^#(mark(X1),mark(X2))	(37)
mark^#(sqr(X))	→	a__sqr^#(mark(X))	(39)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__add^#)	=	1
π(a__terms^#)	=	1
π(mark^#)	=	1
π(mark)	=	1

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

prec(s)	=	0	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__first^#)	=	0	status(a__first^#)	=	[2, 1]	list-extension(a__first^#)	=	Lex
prec(recip)	=	0	status(recip)	=	[1]	list-extension(recip)	=	Lex
prec(dbl)	=	1	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(a__add)	=	1	status(a__add)	=	[2, 1]	list-extension(a__add)	=	Lex
prec(a__dbl)	=	1	status(a__dbl)	=	[1]	list-extension(a__dbl)	=	Lex
prec(a__sqr)	=	2	status(a__sqr)	=	[1]	list-extension(a__sqr)	=	Lex
prec(0)	=	3	status(0)	=	[]	list-extension(0)	=	Lex
prec(nil)	=	4	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(a__dbl^#)	=	0	status(a__dbl^#)	=	[]	list-extension(a__dbl^#)	=	Lex
prec(first)	=	4	status(first)	=	[]	list-extension(first)	=	Lex
prec(a__first)	=	4	status(a__first)	=	[]	list-extension(a__first)	=	Lex
prec(cons)	=	0	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(add)	=	1	status(add)	=	[2, 1]	list-extension(add)	=	Lex
prec(sqr)	=	2	status(sqr)	=	[1]	list-extension(sqr)	=	Lex
prec(a__terms)	=	3	status(a__terms)	=	[]	list-extension(a__terms)	=	Lex
prec(a__sqr^#)	=	2	status(a__sqr^#)	=	[1]	list-extension(a__sqr^#)	=	Lex
prec(terms)	=	3	status(terms)	=	[]	list-extension(terms)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[a__first^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[recip(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[a__add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__dbl(x₁)]	=	x₁ + 0
[a__sqr(x₁)]	=	x₁ + 0
[0]	=	0
[nil]	=	0
[a__dbl^#(x₁)]	=	0
[first(x₁, x₂)]	=	max(0)
[a__first(x₁, x₂)]	=	max(0)
[cons(x₁, x₂)]	=	max(0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[sqr(x₁)]	=	x₁ + 0
[a__terms(x₁)]	=	0
[a__sqr^#(x₁)]	=	x₁ + 0
[terms(x₁)]	=	0

together with the usable rules

mark(0)	→	0	(18)
a__dbl(0)	→	0	(4)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(15)
a__first(0,X)	→	nil	(8)
a__terms(N)	→	cons(recip(a__sqr(mark(N))),terms(s(N)))	(1)
a__sqr(s(X))	→	s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))	(3)
mark(recip(X))	→	recip(mark(X))	(16)
a__sqr(X)	→	sqr(X)	(21)
mark(nil)	→	nil	(19)
mark(s(X))	→	s(mark(X))	(17)
a__add(X1,X2)	→	add(X1,X2)	(22)
a__dbl(s(X))	→	s(s(a__dbl(mark(X))))	(5)
mark(terms(X))	→	a__terms(mark(X))	(10)
a__add(s(X),Y)	→	s(a__add(mark(X),mark(Y)))	(7)
a__terms(X)	→	terms(X)	(20)
mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(14)
mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(12)
a__dbl(X)	→	dbl(X)	(23)
a__first(X1,X2)	→	first(X1,X2)	(24)
mark(sqr(X))	→	a__sqr(mark(X))	(11)
a__first(s(X),cons(Y,Z))	→	cons(mark(Y),first(X,Z))	(9)
mark(dbl(X))	→	a__dbl(mark(X))	(13)
a__add(0,X)	→	mark(X)	(6)
a__sqr(0)	→	0	(2)

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

a__sqr^#(s(X))	→	a__sqr^#(mark(X))	(32)
a__sqr^#(s(X))	→	a__add^#(a__sqr(mark(X)),a__dbl(mark(X)))	(41)
mark^#(s(X))	→	mark^#(X)	(36)
a__add^#(s(X),Y)	→	mark^#(X)	(34)
a__add^#(s(X),Y)	→	a__add^#(mark(X),mark(Y))	(28)
mark^#(add(X1,X2))	→	mark^#(X1)	(49)
mark^#(add(X1,X2))	→	a__add^#(mark(X1),mark(X2))	(37)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.