Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM01_GM)

The rewrite relation of the following TRS is considered.

a__incr(nil)	→	nil	(1)
a__incr(cons(X,L))	→	cons(s(mark(X)),incr(L))	(2)
a__adx(nil)	→	nil	(3)
a__adx(cons(X,L))	→	a__incr(cons(mark(X),adx(L)))	(4)
a__nats	→	a__adx(a__zeros)	(5)
a__zeros	→	cons(0,zeros)	(6)
a__head(cons(X,L))	→	mark(X)	(7)
a__tail(cons(X,L))	→	mark(L)	(8)
mark(incr(X))	→	a__incr(mark(X))	(9)
mark(adx(X))	→	a__adx(mark(X))	(10)
mark(nats)	→	a__nats	(11)
mark(zeros)	→	a__zeros	(12)
mark(head(X))	→	a__head(mark(X))	(13)
mark(tail(X))	→	a__tail(mark(X))	(14)
mark(nil)	→	nil	(15)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
mark(s(X))	→	s(mark(X))	(17)
mark(0)	→	0	(18)
a__incr(X)	→	incr(X)	(19)
a__adx(X)	→	adx(X)	(20)
a__nats	→	nats	(21)
a__zeros	→	zeros	(22)
a__head(X)	→	head(X)	(23)
a__tail(X)	→	tail(X)	(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^#(head(X))	→	a__head^#(mark(X))	(25)
mark^#(nats)	→	a__nats^#	(26)
a__nats^#	→	a__adx^#(a__zeros)	(27)
mark^#(tail(X))	→	mark^#(X)	(28)
mark^#(adx(X))	→	a__adx^#(mark(X))	(29)
mark^#(adx(X))	→	mark^#(X)	(30)
a__nats^#	→	a__zeros^#	(31)
mark^#(zeros)	→	a__zeros^#	(32)
a__head^#(cons(X,L))	→	mark^#(X)	(33)
mark^#(incr(X))	→	mark^#(X)	(34)
a__tail^#(cons(X,L))	→	mark^#(L)	(35)
a__adx^#(cons(X,L))	→	mark^#(X)	(36)
mark^#(cons(X1,X2))	→	mark^#(X1)	(37)
mark^#(head(X))	→	mark^#(X)	(38)
a__incr^#(cons(X,L))	→	mark^#(X)	(39)
mark^#(tail(X))	→	a__tail^#(mark(X))	(40)
mark^#(s(X))	→	mark^#(X)	(41)
mark^#(incr(X))	→	a__incr^#(mark(X))	(42)
a__adx^#(cons(X,L))	→	a__incr^#(cons(mark(X),adx(L)))	(43)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__adx^#(cons(X,L))	→	a__incr^#(cons(mark(X),adx(L)))	(43)
mark^#(incr(X))	→	a__incr^#(mark(X))	(42)
mark^#(s(X))	→	mark^#(X)	(41)
mark^#(adx(X))	→	mark^#(X)	(30)
mark^#(tail(X))	→	a__tail^#(mark(X))	(40)
a__incr^#(cons(X,L))	→	mark^#(X)	(39)
mark^#(head(X))	→	mark^#(X)	(38)
mark^#(cons(X1,X2))	→	mark^#(X1)	(37)
mark^#(adx(X))	→	a__adx^#(mark(X))	(29)
mark^#(tail(X))	→	mark^#(X)	(28)
a__nats^#	→	a__adx^#(a__zeros)	(27)
a__adx^#(cons(X,L))	→	mark^#(X)	(36)
a__tail^#(cons(X,L))	→	mark^#(L)	(35)
mark^#(nats)	→	a__nats^#	(26)
mark^#(incr(X))	→	mark^#(X)	(34)
a__head^#(cons(X,L))	→	mark^#(X)	(33)
mark^#(head(X))	→	a__head^#(mark(X))	(25)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[incr(x₁)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[a__head^#(x₁)]	=	x₁ + 1
[a__incr(x₁)]	=	x₁ + 0
[a__nats]	=	41439
[adx(x₁)]	=	x₁ + 18458
[zeros]	=	22979
[a__adx^#(x₁)]	=	x₁ + 18458
[tail(x₁)]	=	x₁ + 2
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[a__zeros^#]	=	0
[nil]	=	1
[a__nats^#]	=	41438
[mark(x₁)]	=	x₁ + 0
[a__adx(x₁)]	=	x₁ + 18458
[nats]	=	41439
[a__incr^#(x₁)]	=	x₁ + 0
[head(x₁)]	=	x₁ + 25908
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[a__tail(x₁)]	=	x₁ + 2
[a__tail^#(x₁)]	=	x₁ + 1
[a__zeros]	=	22979
[a__head(x₁)]	=	x₁ + 25908

together with the usable rules

mark(0)	→	0	(18)
a__adx(cons(X,L))	→	a__incr(cons(mark(X),adx(L)))	(4)
mark(nil)	→	nil	(15)
a__tail(cons(X,L))	→	mark(L)	(8)
a__incr(nil)	→	nil	(1)
a__adx(nil)	→	nil	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__nats	→	nats	(21)
a__incr(X)	→	incr(X)	(19)
mark(s(X))	→	s(mark(X))	(17)
a__zeros	→	zeros	(22)
a__nats	→	a__adx(a__zeros)	(5)
mark(adx(X))	→	a__adx(mark(X))	(10)
a__head(cons(X,L))	→	mark(X)	(7)
a__adx(X)	→	adx(X)	(20)
mark(tail(X))	→	a__tail(mark(X))	(14)
mark(zeros)	→	a__zeros	(12)
a__head(X)	→	head(X)	(23)
a__tail(X)	→	tail(X)	(24)
mark(nats)	→	a__nats	(11)
mark(incr(X))	→	a__incr(mark(X))	(9)
mark(head(X))	→	a__head(mark(X))	(13)
a__zeros	→	cons(0,zeros)	(6)
a__incr(cons(X,L))	→	cons(s(mark(X)),incr(L))	(2)

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

mark^#(adx(X))	→	mark^#(X)	(30)
mark^#(tail(X))	→	a__tail^#(mark(X))	(40)
mark^#(head(X))	→	mark^#(X)	(38)
mark^#(tail(X))	→	mark^#(X)	(28)
a__nats^#	→	a__adx^#(a__zeros)	(27)
a__adx^#(cons(X,L))	→	mark^#(X)	(36)
a__tail^#(cons(X,L))	→	mark^#(L)	(35)
mark^#(nats)	→	a__nats^#	(26)
a__head^#(cons(X,L))	→	mark^#(X)	(33)
mark^#(head(X))	→	a__head^#(mark(X))	(25)

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__adx^#(cons(X,L))	→	a__incr^#(cons(mark(X),adx(L)))	(43)
mark^#(cons(X1,X2))	→	mark^#(X1)	(37)
mark^#(s(X))	→	mark^#(X)	(41)
mark^#(adx(X))	→	a__adx^#(mark(X))	(29)
mark^#(incr(X))	→	mark^#(X)	(34)
mark^#(incr(X))	→	a__incr^#(mark(X))	(42)
a__incr^#(cons(X,L))	→	mark^#(X)	(39)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[incr(x₁)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[a__head^#(x₁)]	=	0
[a__incr(x₁)]	=	x₁ + 0
[a__nats]	=	5
[adx(x₁)]	=	x₁ + 1
[zeros]	=	4
[a__adx^#(x₁)]	=	x₁ + 2
[tail(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	x₁ + 2
[0]	=	1
[a__zeros^#]	=	0
[nil]	=	1
[a__nats^#]	=	0
[mark(x₁)]	=	x₁ + 0
[a__adx(x₁)]	=	x₁ + 1
[nats]	=	5
[a__incr^#(x₁)]	=	x₁ + 0
[head(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	max(x₁ + 3, x₂ + 0, 0)
[a__tail(x₁)]	=	x₁ + 1
[a__tail^#(x₁)]	=	0
[a__zeros]	=	4
[a__head(x₁)]	=	x₁ + 1

together with the usable rules

mark(0)	→	0	(18)
a__adx(cons(X,L))	→	a__incr(cons(mark(X),adx(L)))	(4)
mark(nil)	→	nil	(15)
a__tail(cons(X,L))	→	mark(L)	(8)
a__incr(nil)	→	nil	(1)
a__adx(nil)	→	nil	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__nats	→	nats	(21)
a__incr(X)	→	incr(X)	(19)
mark(s(X))	→	s(mark(X))	(17)
a__zeros	→	zeros	(22)
a__nats	→	a__adx(a__zeros)	(5)
mark(adx(X))	→	a__adx(mark(X))	(10)
a__head(cons(X,L))	→	mark(X)	(7)
a__adx(X)	→	adx(X)	(20)
mark(tail(X))	→	a__tail(mark(X))	(14)
mark(zeros)	→	a__zeros	(12)
a__head(X)	→	head(X)	(23)
a__tail(X)	→	tail(X)	(24)
mark(nats)	→	a__nats	(11)
mark(incr(X))	→	a__incr(mark(X))	(9)
mark(head(X))	→	a__head(mark(X))	(13)
a__zeros	→	cons(0,zeros)	(6)
a__incr(cons(X,L))	→	cons(s(mark(X)),incr(L))	(2)

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

a__adx^#(cons(X,L))	→	a__incr^#(cons(mark(X),adx(L)))	(43)
mark^#(cons(X1,X2))	→	mark^#(X1)	(37)
mark^#(adx(X))	→	a__adx^#(mark(X))	(29)
mark^#(incr(X))	→	a__incr^#(mark(X))	(42)
a__incr^#(cons(X,L))	→	mark^#(X)	(39)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(s(X))	→	mark^#(X)	(41)
mark^#(incr(X))	→	mark^#(X)	(34)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[incr(x₁)]	=	x₁ + 56455
[s(x₁)]	=	x₁ + 1
[a__head^#(x₁)]	=	1
[a__incr(x₁)]	=	56454
[a__nats]	=	28229
[adx(x₁)]	=	x₁ + 28231
[zeros]	=	28230
[a__adx^#(x₁)]	=	0
[tail(x₁)]	=	2
[mark^#(x₁)]	=	x₁ + 0
[0]	=	28229
[a__zeros^#]	=	0
[nil]	=	56455
[a__nats^#]	=	41438
[mark(x₁)]	=	28228
[a__adx(x₁)]	=	28230
[nats]	=	28230
[a__incr^#(x₁)]	=	0
[head(x₁)]	=	2
[cons(x₁, x₂)]	=	x₁ + 28226
[a__tail(x₁)]	=	x₁ + 1
[a__tail^#(x₁)]	=	1
[a__zeros]	=	28229
[a__head(x₁)]	=	x₁ + 1

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

mark^#(s(X))	→	mark^#(X)	(41)
mark^#(incr(X))	→	mark^#(X)	(34)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.