Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_DLMMU04_GM)

The rewrite relation of the following TRS is considered.

a__pairNs	→	cons(0,incr(oddNs))	(1)
a__oddNs	→	a__incr(a__pairNs)	(2)
a__incr(cons(X,XS))	→	cons(s(mark(X)),incr(XS))	(3)
a__take(0,XS)	→	nil	(4)
a__take(s(N),cons(X,XS))	→	cons(mark(X),take(N,XS))	(5)
a__zip(nil,XS)	→	nil	(6)
a__zip(X,nil)	→	nil	(7)
a__zip(cons(X,XS),cons(Y,YS))	→	cons(pair(mark(X),mark(Y)),zip(XS,YS))	(8)
a__tail(cons(X,XS))	→	mark(XS)	(9)
a__repItems(nil)	→	nil	(10)
a__repItems(cons(X,XS))	→	cons(mark(X),cons(X,repItems(XS)))	(11)
mark(pairNs)	→	a__pairNs	(12)
mark(incr(X))	→	a__incr(mark(X))	(13)
mark(oddNs)	→	a__oddNs	(14)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(15)
mark(zip(X1,X2))	→	a__zip(mark(X1),mark(X2))	(16)
mark(tail(X))	→	a__tail(mark(X))	(17)
mark(repItems(X))	→	a__repItems(mark(X))	(18)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(19)
mark(0)	→	0	(20)
mark(s(X))	→	s(mark(X))	(21)
mark(nil)	→	nil	(22)
mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(23)
a__pairNs	→	pairNs	(24)
a__incr(X)	→	incr(X)	(25)
a__oddNs	→	oddNs	(26)
a__take(X1,X2)	→	take(X1,X2)	(27)
a__zip(X1,X2)	→	zip(X1,X2)	(28)
a__tail(X)	→	tail(X)	(29)
a__repItems(X)	→	repItems(X)	(30)

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__oddNs^#	→	a__pairNs^#	(31)
a__repItems^#(cons(X,XS))	→	mark^#(X)	(32)
mark^#(tail(X))	→	mark^#(X)	(33)
mark^#(pairNs)	→	a__pairNs^#	(34)
a__take^#(s(N),cons(X,XS))	→	mark^#(X)	(35)
mark^#(take(X1,X2))	→	mark^#(X2)	(36)
mark^#(take(X1,X2))	→	mark^#(X1)	(37)
mark^#(tail(X))	→	a__tail^#(mark(X))	(38)
mark^#(cons(X1,X2))	→	mark^#(X1)	(39)
mark^#(repItems(X))	→	a__repItems^#(mark(X))	(40)
a__zip^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(41)
mark^#(pair(X1,X2))	→	mark^#(X1)	(42)
mark^#(oddNs)	→	a__oddNs^#	(43)
a__tail^#(cons(X,XS))	→	mark^#(XS)	(44)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(45)
mark^#(zip(X1,X2))	→	mark^#(X1)	(46)
a__incr^#(cons(X,XS))	→	mark^#(X)	(47)
mark^#(repItems(X))	→	mark^#(X)	(48)
a__zip^#(cons(X,XS),cons(Y,YS))	→	mark^#(Y)	(49)
mark^#(zip(X1,X2))	→	a__zip^#(mark(X1),mark(X2))	(50)
mark^#(incr(X))	→	a__incr^#(mark(X))	(51)
a__oddNs^#	→	a__incr^#(a__pairNs)	(52)
mark^#(pair(X1,X2))	→	mark^#(X2)	(53)
mark^#(s(X))	→	mark^#(X)	(54)
mark^#(incr(X))	→	mark^#(X)	(55)
mark^#(zip(X1,X2))	→	mark^#(X2)	(56)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(zip(X1,X2))	→	mark^#(X2)	(56)
mark^#(repItems(X))	→	a__repItems^#(mark(X))	(40)
mark^#(incr(X))	→	mark^#(X)	(55)
mark^#(cons(X1,X2))	→	mark^#(X1)	(39)
mark^#(s(X))	→	mark^#(X)	(54)
mark^#(tail(X))	→	a__tail^#(mark(X))	(38)
mark^#(pair(X1,X2))	→	mark^#(X2)	(53)
a__oddNs^#	→	a__incr^#(a__pairNs)	(52)
mark^#(take(X1,X2))	→	mark^#(X1)	(37)
mark^#(incr(X))	→	a__incr^#(mark(X))	(51)
mark^#(take(X1,X2))	→	mark^#(X2)	(36)
mark^#(zip(X1,X2))	→	a__zip^#(mark(X1),mark(X2))	(50)
a__zip^#(cons(X,XS),cons(Y,YS))	→	mark^#(Y)	(49)
mark^#(repItems(X))	→	mark^#(X)	(48)
a__take^#(s(N),cons(X,XS))	→	mark^#(X)	(35)
mark^#(tail(X))	→	mark^#(X)	(33)
a__incr^#(cons(X,XS))	→	mark^#(X)	(47)
mark^#(zip(X1,X2))	→	mark^#(X1)	(46)
a__repItems^#(cons(X,XS))	→	mark^#(X)	(32)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(45)
a__tail^#(cons(X,XS))	→	mark^#(XS)	(44)
mark^#(oddNs)	→	a__oddNs^#	(43)
mark^#(pair(X1,X2))	→	mark^#(X1)	(42)
a__zip^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(41)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 17069
[incr(x₁)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[a__zip^#(x₁, x₂)]	=	max(x₁ + 47645, x₂ + 17067, 0)
[a__incr(x₁)]	=	x₁ + 0
[take(x₁, x₂)]	=	max(x₁ + 17069, x₂ + 17069, 0)
[pair(x₁, x₂)]	=	max(x₁ + 13506, x₂ + 13507, 0)
[a__take^#(x₁, x₂)]	=	max(x₁ + 17067, x₂ + 17069, 0)
[a__pairNs^#]	=	0
[tail(x₁)]	=	x₁ + 7631
[mark^#(x₁)]	=	x₁ + 17068
[0]	=	41054
[a__repItems(x₁)]	=	x₁ + 17069
[nil]	=	7320
[a__oddNs^#]	=	58124
[mark(x₁)]	=	x₁ + 0
[pairNs]	=	58123
[a__zip(x₁, x₂)]	=	max(x₁ + 30578, x₂ + 30576, 0)
[a__repItems^#(x₁)]	=	x₁ + 17069
[oddNs]	=	58123
[a__incr^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 17069, x₂ + 0, 0)
[a__oddNs]	=	58123
[a__take(x₁, x₂)]	=	max(x₁ + 17069, x₂ + 17069, 0)
[a__pairNs]	=	58123
[a__tail(x₁)]	=	x₁ + 7631
[a__tail^#(x₁)]	=	x₁ + 17069
[zip(x₁, x₂)]	=	max(x₁ + 30578, x₂ + 30576, 0)

together with the usable rules

mark(repItems(X))	→	a__repItems(mark(X))	(18)
a__take(0,XS)	→	nil	(4)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(15)
a__zip(cons(X,XS),cons(Y,YS))	→	cons(pair(mark(X),mark(Y)),zip(XS,YS))	(8)
a__pairNs	→	cons(0,incr(oddNs))	(1)
a__incr(cons(X,XS))	→	cons(s(mark(X)),incr(XS))	(3)
mark(zip(X1,X2))	→	a__zip(mark(X1),mark(X2))	(16)
mark(s(X))	→	s(mark(X))	(21)
a__oddNs	→	oddNs	(26)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(19)
mark(tail(X))	→	a__tail(mark(X))	(17)
a__take(X1,X2)	→	take(X1,X2)	(27)
mark(nil)	→	nil	(22)
a__zip(X1,X2)	→	zip(X1,X2)	(28)
a__take(s(N),cons(X,XS))	→	cons(mark(X),take(N,XS))	(5)
a__repItems(nil)	→	nil	(10)
a__zip(X,nil)	→	nil	(7)
mark(0)	→	0	(20)
a__incr(X)	→	incr(X)	(25)
a__repItems(X)	→	repItems(X)	(30)
mark(oddNs)	→	a__oddNs	(14)
mark(pairNs)	→	a__pairNs	(12)
mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(23)
a__pairNs	→	pairNs	(24)
a__repItems(cons(X,XS))	→	cons(mark(X),cons(X,repItems(XS)))	(11)
a__tail(cons(X,XS))	→	mark(XS)	(9)
mark(incr(X))	→	a__incr(mark(X))	(13)
a__zip(nil,XS)	→	nil	(6)
a__tail(X)	→	tail(X)	(29)
a__oddNs	→	a__incr(a__pairNs)	(2)

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

mark^#(zip(X1,X2))	→	mark^#(X2)	(56)
mark^#(repItems(X))	→	a__repItems^#(mark(X))	(40)
mark^#(cons(X1,X2))	→	mark^#(X1)	(39)
mark^#(tail(X))	→	a__tail^#(mark(X))	(38)
mark^#(pair(X1,X2))	→	mark^#(X2)	(53)
a__oddNs^#	→	a__incr^#(a__pairNs)	(52)
mark^#(take(X1,X2))	→	mark^#(X1)	(37)
mark^#(incr(X))	→	a__incr^#(mark(X))	(51)
mark^#(take(X1,X2))	→	mark^#(X2)	(36)
mark^#(zip(X1,X2))	→	a__zip^#(mark(X1),mark(X2))	(50)
a__zip^#(cons(X,XS),cons(Y,YS))	→	mark^#(Y)	(49)
mark^#(repItems(X))	→	mark^#(X)	(48)
a__take^#(s(N),cons(X,XS))	→	mark^#(X)	(35)
mark^#(tail(X))	→	mark^#(X)	(33)
a__incr^#(cons(X,XS))	→	mark^#(X)	(47)
mark^#(zip(X1,X2))	→	mark^#(X1)	(46)
a__repItems^#(cons(X,XS))	→	mark^#(X)	(32)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(45)
a__tail^#(cons(X,XS))	→	mark^#(XS)	(44)
mark^#(oddNs)	→	a__oddNs^#	(43)
mark^#(pair(X1,X2))	→	mark^#(X1)	(42)
a__zip^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(41)

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

mark^#(s(X))	→	mark^#(X)	(54)
mark^#(incr(X))	→	mark^#(X)	(55)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	2
[incr(x₁)]	=	x₁ + 13217
[s(x₁)]	=	x₁ + 1
[a__zip^#(x₁, x₂)]	=	1
[a__incr(x₁)]	=	13216
[take(x₁, x₂)]	=	x₂ + 3
[pair(x₁, x₂)]	=	x₁ + 1
[a__take^#(x₁, x₂)]	=	0
[a__pairNs^#]	=	0
[tail(x₁)]	=	2
[mark^#(x₁)]	=	x₁ + 1
[0]	=	2
[a__repItems(x₁)]	=	x₁ + 1
[nil]	=	14100
[a__oddNs^#]	=	1
[mark(x₁)]	=	1
[pairNs]	=	3
[a__zip(x₁, x₂)]	=	11494
[a__repItems^#(x₁)]	=	1
[oddNs]	=	13216
[a__incr^#(x₁)]	=	1
[cons(x₁, x₂)]	=	x₂ + 4685
[a__oddNs]	=	13215
[a__take(x₁, x₂)]	=	2
[a__pairNs]	=	2
[a__tail(x₁)]	=	x₁ + 1
[a__tail^#(x₁)]	=	1
[zip(x₁, x₂)]	=	x₁ + x₂ + 11495

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

mark^#(s(X))	→	mark^#(X)	(54)
mark^#(incr(X))	→	mark^#(X)	(55)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.