Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/Ex1_Luc04b_GM)

The rewrite relation of the following TRS is considered.

a__nats	→	cons(0,incr(nats))	(1)
a__pairs	→	cons(0,incr(odds))	(2)
a__odds	→	a__incr(a__pairs)	(3)
a__incr(cons(X,XS))	→	cons(s(mark(X)),incr(XS))	(4)
a__head(cons(X,XS))	→	mark(X)	(5)
a__tail(cons(X,XS))	→	mark(XS)	(6)
mark(nats)	→	a__nats	(7)
mark(pairs)	→	a__pairs	(8)
mark(odds)	→	a__odds	(9)
mark(incr(X))	→	a__incr(mark(X))	(10)
mark(head(X))	→	a__head(mark(X))	(11)
mark(tail(X))	→	a__tail(mark(X))	(12)
mark(0)	→	0	(13)
mark(s(X))	→	s(mark(X))	(14)
mark(nil)	→	nil	(15)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__nats	→	nats	(17)
a__pairs	→	pairs	(18)
a__odds	→	odds	(19)
a__incr(X)	→	incr(X)	(20)
a__head(X)	→	head(X)	(21)
a__tail(X)	→	tail(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.

mark^#(odds)	→	a__odds^#	(23)
mark^#(tail(X))	→	mark^#(X)	(24)
a__odds^#	→	a__incr^#(a__pairs)	(25)
mark^#(incr(X))	→	a__incr^#(mark(X))	(26)
a__head^#(cons(X,XS))	→	mark^#(X)	(27)
mark^#(cons(X1,X2))	→	mark^#(X1)	(28)
a__odds^#	→	a__pairs^#	(29)
mark^#(s(X))	→	mark^#(X)	(30)
mark^#(incr(X))	→	mark^#(X)	(31)
mark^#(tail(X))	→	a__tail^#(mark(X))	(32)
a__incr^#(cons(X,XS))	→	mark^#(X)	(33)
mark^#(head(X))	→	a__head^#(mark(X))	(34)
a__tail^#(cons(X,XS))	→	mark^#(XS)	(35)
mark^#(nats)	→	a__nats^#	(36)
mark^#(pairs)	→	a__pairs^#	(37)
mark^#(head(X))	→	mark^#(X)	(38)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(head(X))	→	mark^#(X)	(38)
mark^#(cons(X1,X2))	→	mark^#(X1)	(28)
a__tail^#(cons(X,XS))	→	mark^#(XS)	(35)
mark^#(head(X))	→	a__head^#(mark(X))	(34)
a__incr^#(cons(X,XS))	→	mark^#(X)	(33)
a__head^#(cons(X,XS))	→	mark^#(X)	(27)
mark^#(incr(X))	→	a__incr^#(mark(X))	(26)
a__odds^#	→	a__incr^#(a__pairs)	(25)
mark^#(tail(X))	→	mark^#(X)	(24)
mark^#(tail(X))	→	a__tail^#(mark(X))	(32)
mark^#(incr(X))	→	mark^#(X)	(31)
mark^#(s(X))	→	mark^#(X)	(30)
mark^#(odds)	→	a__odds^#	(23)

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₁ + 4
[a__incr(x₁)]	=	x₁ + 0
[pairs]	=	0
[a__nats]	=	18919
[a__pairs^#]	=	0
[a__odds]	=	0
[tail(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	x₁ + 4
[0]	=	0
[odds]	=	0
[nil]	=	46823
[a__nats^#]	=	0
[mark(x₁)]	=	x₁ + 0
[nats]	=	18919
[a__incr^#(x₁)]	=	x₁ + 4
[head(x₁)]	=	x₁ + 8946
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[a__odds^#]	=	4
[a__pairs]	=	0
[a__tail(x₁)]	=	x₁ + 1
[a__tail^#(x₁)]	=	x₁ + 4
[a__head(x₁)]	=	x₁ + 8946

together with the usable rules

a__pairs	→	pairs	(18)
a__incr(cons(X,XS))	→	cons(s(mark(X)),incr(XS))	(4)
mark(nil)	→	nil	(15)
mark(pairs)	→	a__pairs	(8)
a__nats	→	cons(0,incr(nats))	(1)
a__odds	→	a__incr(a__pairs)	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__head(X)	→	head(X)	(21)
a__odds	→	odds	(19)
a__nats	→	nats	(17)
a__tail(X)	→	tail(X)	(22)
a__head(cons(X,XS))	→	mark(X)	(5)
mark(incr(X))	→	a__incr(mark(X))	(10)
mark(nats)	→	a__nats	(7)
a__incr(X)	→	incr(X)	(20)
mark(s(X))	→	s(mark(X))	(14)
mark(tail(X))	→	a__tail(mark(X))	(12)
mark(head(X))	→	a__head(mark(X))	(11)
mark(odds)	→	a__odds	(9)
mark(0)	→	0	(13)
a__tail(cons(X,XS))	→	mark(XS)	(6)
a__pairs	→	cons(0,incr(odds))	(2)

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

mark^#(head(X))	→	mark^#(X)	(38)
mark^#(head(X))	→	a__head^#(mark(X))	(34)
mark^#(tail(X))	→	mark^#(X)	(24)
mark^#(tail(X))	→	a__tail^#(mark(X))	(32)

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__incr^#(cons(X,XS))	→	mark^#(X)	(33)
a__odds^#	→	a__incr^#(a__pairs)	(25)
mark^#(cons(X1,X2))	→	mark^#(X1)	(28)
mark^#(incr(X))	→	mark^#(X)	(31)
mark^#(incr(X))	→	a__incr^#(mark(X))	(26)
mark^#(s(X))	→	mark^#(X)	(30)
mark^#(odds)	→	a__odds^#	(23)

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
[pairs]	=	41418
[a__nats]	=	41418
[a__pairs^#]	=	0
[a__odds]	=	41418
[tail(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	x₁ + 2
[0]	=	33050
[odds]	=	41418
[nil]	=	41141
[a__nats^#]	=	0
[mark(x₁)]	=	x₁ + 0
[nats]	=	41418
[a__incr^#(x₁)]	=	x₁ + 0
[head(x₁)]	=	x₁ + 22248
[cons(x₁, x₂)]	=	max(x₁ + 8368, x₂ + 0, 0)
[a__odds^#]	=	41419
[a__pairs]	=	41418
[a__tail(x₁)]	=	x₁ + 1
[a__tail^#(x₁)]	=	0
[a__head(x₁)]	=	x₁ + 22248

together with the usable rules

a__pairs	→	pairs	(18)
a__incr(cons(X,XS))	→	cons(s(mark(X)),incr(XS))	(4)
mark(nil)	→	nil	(15)
mark(pairs)	→	a__pairs	(8)
a__nats	→	cons(0,incr(nats))	(1)
a__odds	→	a__incr(a__pairs)	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__head(X)	→	head(X)	(21)
a__odds	→	odds	(19)
a__nats	→	nats	(17)
a__tail(X)	→	tail(X)	(22)
a__head(cons(X,XS))	→	mark(X)	(5)
mark(incr(X))	→	a__incr(mark(X))	(10)
mark(nats)	→	a__nats	(7)
a__incr(X)	→	incr(X)	(20)
mark(s(X))	→	s(mark(X))	(14)
mark(tail(X))	→	a__tail(mark(X))	(12)
mark(head(X))	→	a__head(mark(X))	(11)
mark(odds)	→	a__odds	(9)
mark(0)	→	0	(13)
a__tail(cons(X,XS))	→	mark(XS)	(6)
a__pairs	→	cons(0,incr(odds))	(2)

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

a__incr^#(cons(X,XS))	→	mark^#(X)	(33)
a__odds^#	→	a__incr^#(a__pairs)	(25)
mark^#(cons(X1,X2))	→	mark^#(X1)	(28)
mark^#(incr(X))	→	a__incr^#(mark(X))	(26)
mark^#(odds)	→	a__odds^#	(23)

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^#(incr(X))	→	mark^#(X)	(31)
mark^#(s(X))	→	mark^#(X)	(30)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[incr(x₁)]	=	x₁ + 4
[s(x₁)]	=	x₁ + 1
[a__head^#(x₁)]	=	4
[a__incr(x₁)]	=	3
[pairs]	=	3
[a__nats]	=	2
[a__pairs^#]	=	0
[a__odds]	=	2
[tail(x₁)]	=	3
[mark^#(x₁)]	=	x₁ + 3
[0]	=	2
[odds]	=	3
[nil]	=	2
[a__nats^#]	=	0
[mark(x₁)]	=	1
[nats]	=	21240
[a__incr^#(x₁)]	=	3
[head(x₁)]	=	8946
[cons(x₁, x₂)]	=	4
[a__odds^#]	=	3
[a__pairs]	=	2
[a__tail(x₁)]	=	2
[a__tail^#(x₁)]	=	4
[a__head(x₁)]	=	2

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

mark^#(incr(X))	→	mark^#(X)	(31)
mark^#(s(X))	→	mark^#(X)	(30)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.