Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec11_1_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)
a__half(0)	→	0	(10)
a__half(s(0))	→	0	(11)
a__half(s(s(X)))	→	s(a__half(mark(X)))	(12)
a__half(dbl(X))	→	mark(X)	(13)
mark(terms(X))	→	a__terms(mark(X))	(14)
mark(sqr(X))	→	a__sqr(mark(X))	(15)
mark(add(X1,X2))	→	a__add(mark(X1),mark(X2))	(16)
mark(dbl(X))	→	a__dbl(mark(X))	(17)
mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(18)
mark(half(X))	→	a__half(mark(X))	(19)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(20)
mark(recip(X))	→	recip(mark(X))	(21)
mark(s(X))	→	s(mark(X))	(22)
mark(0)	→	0	(23)
mark(nil)	→	nil	(24)
a__terms(X)	→	terms(X)	(25)
a__sqr(X)	→	sqr(X)	(26)
a__add(X1,X2)	→	add(X1,X2)	(27)
a__dbl(X)	→	dbl(X)	(28)
a__first(X1,X2)	→	first(X1,X2)	(29)
a__half(X)	→	half(X)	(30)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a__terms^#(N)	→	a__sqr^#(mark(N))	(31)
a__terms^#(N)	→	mark^#(N)	(32)
a__sqr^#(s(X))	→	a__add^#(a__sqr(mark(X)),a__dbl(mark(X)))	(33)
a__sqr^#(s(X))	→	a__sqr^#(mark(X))	(34)
a__sqr^#(s(X))	→	mark^#(X)	(35)
a__sqr^#(s(X))	→	a__dbl^#(mark(X))	(36)
a__dbl^#(s(X))	→	a__dbl^#(mark(X))	(37)
a__dbl^#(s(X))	→	mark^#(X)	(38)
a__add^#(0,X)	→	mark^#(X)	(39)
a__add^#(s(X),Y)	→	a__add^#(mark(X),mark(Y))	(40)
a__add^#(s(X),Y)	→	mark^#(X)	(41)
a__add^#(s(X),Y)	→	mark^#(Y)	(42)
a__first^#(s(X),cons(Y,Z))	→	mark^#(Y)	(43)
a__half^#(s(s(X)))	→	a__half^#(mark(X))	(44)
a__half^#(s(s(X)))	→	mark^#(X)	(45)
a__half^#(dbl(X))	→	mark^#(X)	(46)
mark^#(terms(X))	→	a__terms^#(mark(X))	(47)
mark^#(terms(X))	→	mark^#(X)	(48)
mark^#(sqr(X))	→	a__sqr^#(mark(X))	(49)
mark^#(sqr(X))	→	mark^#(X)	(50)
mark^#(add(X1,X2))	→	a__add^#(mark(X1),mark(X2))	(51)
mark^#(add(X1,X2))	→	mark^#(X1)	(52)
mark^#(add(X1,X2))	→	mark^#(X2)	(53)
mark^#(dbl(X))	→	a__dbl^#(mark(X))	(54)
mark^#(dbl(X))	→	mark^#(X)	(55)
mark^#(first(X1,X2))	→	a__first^#(mark(X1),mark(X2))	(56)
mark^#(first(X1,X2))	→	mark^#(X1)	(57)
mark^#(first(X1,X2))	→	mark^#(X2)	(58)
mark^#(half(X))	→	a__half^#(mark(X))	(59)
mark^#(half(X))	→	mark^#(X)	(60)
mark^#(cons(X1,X2))	→	mark^#(X1)	(61)
mark^#(recip(X))	→	mark^#(X)	(62)
mark^#(s(X))	→	mark^#(X)	(63)

1.1 Reduction Pair Processor

Using the

prec(a__terms^#)	=	6		stat(a__terms^#)	=	lex
prec(a__sqr^#)	=	6		stat(a__sqr^#)	=	lex
prec(mark^#)	=	0		stat(mark^#)	=	mul
prec(s)	=	1		stat(s)	=	lex
prec(a__add^#)	=	2		stat(a__add^#)	=	mul
prec(a__sqr)	=	6		stat(a__sqr)	=	lex
prec(a__dbl)	=	6		stat(a__dbl)	=	lex
prec(a__dbl^#)	=	3		stat(a__dbl^#)	=	lex
prec(0)	=	6		stat(0)	=	mul
prec(a__first^#)	=	0		stat(a__first^#)	=	mul
prec(a__half^#)	=	0		stat(a__half^#)	=	mul
prec(dbl)	=	6		stat(dbl)	=	lex
prec(terms)	=	6		stat(terms)	=	lex
prec(sqr)	=	6		stat(sqr)	=	lex
prec(add)	=	4		stat(add)	=	lex
prec(first)	=	7		stat(first)	=	lex
prec(a__terms)	=	6		stat(a__terms)	=	lex
prec(a__add)	=	4		stat(a__add)	=	lex
prec(a__first)	=	7		stat(a__first)	=	lex
prec(nil)	=	5		stat(nil)	=	mul

π(a__terms^#)	=	[1]
π(a__sqr^#)	=	[1]
π(mark)	=	1
π(mark^#)	=	[1]
π(s)	=	[1]
π(a__add^#)	=	[1,2]
π(a__sqr)	=	[1]
π(a__dbl)	=	[1]
π(a__dbl^#)	=	[1]
π(0)	=	[]
π(a__first^#)	=	[2]
π(cons)	=	1
π(a__half^#)	=	[1]
π(dbl)	=	[1]
π(terms)	=	[1]
π(sqr)	=	[1]
π(add)	=	[2,1]
π(first)	=	[2,1]
π(half)	=	1
π(recip)	=	1
π(a__terms)	=	[1]
π(a__add)	=	[2,1]
π(a__half)	=	1
π(a__first)	=	[2,1]
π(nil)	=	[]

the pairs

a__terms^#(N)	→	mark^#(N)	(32)
a__sqr^#(s(X))	→	a__add^#(a__sqr(mark(X)),a__dbl(mark(X)))	(33)
a__sqr^#(s(X))	→	a__sqr^#(mark(X))	(34)
a__sqr^#(s(X))	→	mark^#(X)	(35)
a__sqr^#(s(X))	→	a__dbl^#(mark(X))	(36)
a__dbl^#(s(X))	→	a__dbl^#(mark(X))	(37)
a__dbl^#(s(X))	→	mark^#(X)	(38)
a__add^#(0,X)	→	mark^#(X)	(39)
a__add^#(s(X),Y)	→	a__add^#(mark(X),mark(Y))	(40)
a__add^#(s(X),Y)	→	mark^#(X)	(41)
a__add^#(s(X),Y)	→	mark^#(Y)	(42)
a__half^#(s(s(X)))	→	a__half^#(mark(X))	(44)
a__half^#(s(s(X)))	→	mark^#(X)	(45)
a__half^#(dbl(X))	→	mark^#(X)	(46)
mark^#(terms(X))	→	a__terms^#(mark(X))	(47)
mark^#(terms(X))	→	mark^#(X)	(48)
mark^#(sqr(X))	→	a__sqr^#(mark(X))	(49)
mark^#(sqr(X))	→	mark^#(X)	(50)
mark^#(add(X1,X2))	→	a__add^#(mark(X1),mark(X2))	(51)
mark^#(add(X1,X2))	→	mark^#(X1)	(52)
mark^#(add(X1,X2))	→	mark^#(X2)	(53)
mark^#(dbl(X))	→	a__dbl^#(mark(X))	(54)
mark^#(dbl(X))	→	mark^#(X)	(55)
mark^#(first(X1,X2))	→	a__first^#(mark(X1),mark(X2))	(56)
mark^#(first(X1,X2))	→	mark^#(X1)	(57)
mark^#(first(X1,X2))	→	mark^#(X2)	(58)
mark^#(s(X))	→	mark^#(X)	(63)

could be deleted.

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(cons(X1,X2)) → mark^#(X1) (61)

mark^#(half(X)) → mark^#(X) (60)

mark^#(recip(X)) → mark^#(X) (62)

1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[cons(x₁, x₂)] = 1 · x₁ + 1 · x₂

[half(x₁)] = 1 · x₁

[recip(x₁)] = 1 · x₁

[mark^#(x₁)] = 1 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

mark^#(cons(X1,X2)) → mark^#(X1) (61)

1 > 1

mark^#(half(X)) → mark^#(X) (60)

1 > 1

mark^#(recip(X)) → mark^#(X) (62)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.