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 ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[pairNs]

0	0	0
0	0	0
0	0	0

[cons(x₁, x₂)]

1	0	0
1	0	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
1	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[0]

0	0	0
0	0	0
0	0	0

[incr(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__repItems(x₁)]

1	1	0
1	1	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[tail(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[repItems(x₁)]

1	1	0
1	1	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[a__oddNs]

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__pairNs]

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[zip(x₁, x₂)]

1	0	0
1	1	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

1	0	0
0	0	0
0	0	0

[a__zip(x₁, x₂)]

1	0	1
1	1	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

1	0	0
0	0	0
0	0	0

[take(x₁, x₂)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	1	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__take(x₁, x₂)]

1	1	1
0	0	0
0	0	0

· x₁ +

1	1	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[pair(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__incr(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[oddNs]

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

a__zip(nil,XS)	→	nil	(6)
a__zip(X,nil)	→	nil	(7)
a__repItems(nil)	→	nil	(10)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[pairNs]

0	0	0
0	0	0
0	0	0

[cons(x₁, x₂)]

1	0	0
1	0	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[s(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[0]

0	0	0
1	0	0
1	0	0

[incr(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__repItems(x₁)]

1	1	0
1	1	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

[tail(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[repItems(x₁)]

1	1	0
1	1	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[a__oddNs]

0	0	0
0	0	0
1	0	0

[nil]

0	0	0
0	0	0
1	0	0

[a__pairNs]

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[zip(x₁, x₂)]

1	0	0
1	0	0
0	0	0

· x₁ +

1	1	0
0	1	0
0	0	1

· x₂ +

0	0	0
1	0	0
0	0	0

[a__zip(x₁, x₂)]

1	0	0
1	0	0
0	0	0

· x₁ +

1	1	0
0	1	0
0	0	1

· x₂ +

0	0	0
1	0	0
0	0	0

[take(x₁, x₂)]

1	1	0
0	0	0
0	0	1

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__take(x₁, x₂)]

1	1	0
0	0	0
0	0	1

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[pair(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	1

· x₂ +

0	0	0
0	0	0
0	0	0

[a__incr(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[oddNs]

0	0	0
0	0	0
1	0	0

all of the following rules can be deleted.

a__take(0,XS)

→

nil

(4)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[pairNs]

0	0	0
1	0	0
0	0	0

[cons(x₁, x₂)]

1	0	0
1	0	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	1	1
0	1	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[0]

0	0	0
0	0	0
0	0	0

[incr(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[a__repItems(x₁)]

1	1	0
1	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[tail(x₁)]

1	1	0
0	1	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[repItems(x₁)]

1	1	0
1	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__oddNs]

0	0	0
1	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__pairNs]

0	0	0
1	0	0
0	0	0

[mark(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[zip(x₁, x₂)]

1	1	0
1	0	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

0	0	0
1	0	0
0	0	0

[a__zip(x₁, x₂)]

1	1	0
1	0	0
0	0	0

· x₁ +

1	0	1
0	1	0
0	0	0

· x₂ +

0	0	0
1	0	0
0	0	0

[take(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	1	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__take(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	1	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[pair(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__incr(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[oddNs]

0	0	0
1	0	0
0	0	0

all of the following rules can be deleted.

a__tail(cons(X,XS))

→

mark(XS)

(9)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[pairNs]

0	0	0
0	0	0
0	0	0

[cons(x₁, x₂)]

1	0	0
1	0	0
0	0	0

· x₁ +

1	0	0
0	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
0	1	1
0	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[0]

0	0	0
1	0	0
0	0	0

[incr(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__repItems(x₁)]

1	1	0
1	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[tail(x₁)]

1	0	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[repItems(x₁)]

1	1	0
1	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__oddNs]

0	0	0
1	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__pairNs]

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[zip(x₁, x₂)]

1	0	0
1	0	0
0	0	0

· x₁ +

1	0	0
1	1	0
0	0	0

· x₂ +

0	0	0
1	0	0
0	0	0

[a__zip(x₁, x₂)]

1	0	0
1	0	0
0	0	0

· x₁ +

1	0	1
1	1	1
0	0	0

· x₂ +

0	0	0
1	0	0
0	0	0

[take(x₁, x₂)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	1	0
1	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__take(x₁, x₂)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	1	0
1	1	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[pair(x₁, x₂)]

1	0	1
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
1	0	0
0	0	0

[a__incr(x₁)]

1	0	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[oddNs]

0	0	0
1	0	0
0	0	0

all of the following rules can be deleted.

a__take(s(N),cons(X,XS))

→

cons(mark(X),take(N,XS))

(5)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[pairNs]	=	0
[cons(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[a__tail(x₁)]	=	0 · x₁ + -∞
[s(x₁)]	=	0 · x₁ + -∞
[0]	=	0
[incr(x₁)]	=	0 · x₁ + 0
[a__repItems(x₁)]	=	0 · x₁ + 0
[a__oddNs^#]	=	0
[tail(x₁)]	=	0 · x₁ + -∞
[repItems(x₁)]	=	0 · x₁ + 0
[a__incr^#(x₁)]	=	0 · x₁ + -∞
[a__oddNs]	=	0
[nil]	=	5
[a__pairNs]	=	0
[mark(x₁)]	=	0 · x₁ + -∞
[a__repItems^#(x₁)]	=	0 · x₁ + -∞
[zip(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 0
[a__zip(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 0
[mark^#(x₁)]	=	0 · x₁ + 0
[a__zip^#(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + -∞
[take(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__take(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[pair(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__incr(x₁)]	=	0 · x₁ + 0
[oddNs]	=	0

together with the usable rules

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__zip(cons(X,XS),cons(Y,YS))	→	cons(pair(mark(X),mark(Y)),zip(XS,YS))	(8)
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)

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

a__zip^#(cons(X,XS),cons(Y,YS))

→

mark^#(Y)

(34)

could be deleted.

1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[pairNs]	=	0
[cons(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__tail(x₁)]	=	5 · x₁ + 0
[s(x₁)]	=	0 · x₁ + 0
[0]	=	0
[incr(x₁)]	=	0 · x₁ + -∞
[a__repItems(x₁)]	=	0 · x₁ + -∞
[a__oddNs^#]	=	0
[tail(x₁)]	=	5 · x₁ + 0
[repItems(x₁)]	=	0 · x₁ + -∞
[a__incr^#(x₁)]	=	0 · x₁ + -∞
[a__oddNs]	=	0
[nil]	=	4
[a__pairNs]	=	0
[mark(x₁)]	=	0 · x₁ + -∞
[a__repItems^#(x₁)]	=	0 · x₁ + -∞
[zip(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + -∞
[a__zip(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + -∞
[mark^#(x₁)]	=	0 · x₁ + -∞
[a__zip^#(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + -∞
[take(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__take(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[pair(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__incr(x₁)]	=	0 · x₁ + -∞
[oddNs]	=	0

together with the usable rules

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__zip(cons(X,XS),cons(Y,YS))	→	cons(pair(mark(X),mark(Y)),zip(XS,YS))	(8)
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)

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

mark^#(zip(X1,X2))	→	mark^#(X2)	(44)
mark^#(tail(X))	→	mark^#(X)	(47)

could be deleted.

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[pairNs]	=	0
[cons(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__tail(x₁)]	=	1 · x₁ + -∞
[s(x₁)]	=	0 · x₁ + -∞
[0]	=	0
[incr(x₁)]	=	0 · x₁ + 0
[a__repItems(x₁)]	=	1 · x₁ + 4
[a__oddNs^#]	=	0
[tail(x₁)]	=	1 · x₁ + -∞
[repItems(x₁)]	=	1 · x₁ + 4
[a__incr^#(x₁)]	=	0 · x₁ + 0
[a__oddNs]	=	0
[nil]	=	3
[a__pairNs]	=	0
[mark(x₁)]	=	0 · x₁ + -∞
[a__repItems^#(x₁)]	=	0 · x₁ + 0
[zip(x₁, x₂)]	=	4 · x₁ + 5 · x₂ + 0
[a__zip(x₁, x₂)]	=	4 · x₁ + 5 · x₂ + 0
[mark^#(x₁)]	=	0 · x₁ + 0
[a__zip^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[take(x₁, x₂)]	=	6 · x₁ + 0 · x₂ + -∞
[a__take(x₁, x₂)]	=	6 · x₁ + 0 · x₂ + -∞
[pair(x₁, x₂)]	=	0 · x₁ + 5 · x₂ + -∞
[a__incr(x₁)]	=	0 · x₁ + 0
[oddNs]	=	0

together with the usable rules

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__zip(cons(X,XS),cons(Y,YS))	→	cons(pair(mark(X),mark(Y)),zip(XS,YS))	(8)
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)

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

mark^#(repItems(X))	→	mark^#(X)	(49)
mark^#(repItems(X))	→	a__repItems^#(mark(X))	(50)

could be deleted.

1.1.1.1.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)	(38)
mark^#(incr(X))	→	a__incr^#(mark(X))	(39)
a__incr^#(cons(X,XS))	→	mark^#(X)	(33)
mark^#(oddNs)	→	a__oddNs^#	(40)
a__oddNs^#	→	a__incr^#(a__pairNs)	(32)
mark^#(take(X1,X2))	→	mark^#(X2)	(41)
mark^#(take(X1,X2))	→	mark^#(X1)	(42)
mark^#(zip(X1,X2))	→	mark^#(X1)	(45)
mark^#(zip(X1,X2))	→	a__zip^#(mark(X1),mark(X2))	(46)
a__zip^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(35)
mark^#(cons(X1,X2))	→	mark^#(X1)	(51)
mark^#(s(X))	→	mark^#(X)	(52)
mark^#(pair(X1,X2))	→	mark^#(X2)	(53)
mark^#(pair(X1,X2))	→	mark^#(X1)	(54)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[pairNs]	=	7
[cons(x₁, x₂)]	=	4 · x₁ + 0 · x₂ + 4
[a__tail(x₁)]	=	2 · x₁ + 2
[s(x₁)]	=	0 · x₁ + -∞
[0]	=	0
[incr(x₁)]	=	0 · x₁ + -∞
[a__repItems(x₁)]	=	0 · x₁ + -∞
[a__oddNs^#]	=	7
[tail(x₁)]	=	2 · x₁ + 2
[repItems(x₁)]	=	0 · x₁ + -∞
[a__incr^#(x₁)]	=	0 · x₁ + 0
[a__oddNs]	=	7
[nil]	=	3
[a__pairNs]	=	7
[mark(x₁)]	=	0 · x₁ + -∞
[zip(x₁, x₂)]	=	3 · x₁ + 0 · x₂ + 2
[a__zip(x₁, x₂)]	=	3 · x₁ + 0 · x₂ + 2
[mark^#(x₁)]	=	0 · x₁ + 0
[a__zip^#(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[take(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 0
[a__take(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 0
[pair(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__incr(x₁)]	=	0 · x₁ + -∞
[oddNs]	=	7

together with the usable rules

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__zip(cons(X,XS),cons(Y,YS))	→	cons(pair(mark(X),mark(Y)),zip(XS,YS))	(8)
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)

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

a__incr^#(cons(X,XS))	→	mark^#(X)	(33)
mark^#(zip(X1,X2))	→	mark^#(X1)	(45)
mark^#(zip(X1,X2))	→	a__zip^#(mark(X1),mark(X2))	(46)
a__zip^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(35)
mark^#(cons(X1,X2))	→	mark^#(X1)	(51)

could be deleted.

1.1.1.1.1.1.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^#(pair(X1,X2))	→	mark^#(X2)	(53)
mark^#(incr(X))	→	mark^#(X)	(38)
mark^#(take(X1,X2))	→	mark^#(X2)	(41)
mark^#(take(X1,X2))	→	mark^#(X1)	(42)
mark^#(s(X))	→	mark^#(X)	(52)
mark^#(pair(X1,X2))	→	mark^#(X1)	(54)

1.1.1.1.1.1.1.1.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^#(pair(X1,X2))	→	mark^#(X2)	(53)

1	>	1
mark^#(incr(X))	→	mark^#(X)	(38)

1	>	1
mark^#(take(X1,X2))	→	mark^#(X2)	(41)

1	>	1
mark^#(take(X1,X2))	→	mark^#(X1)	(42)

1	>	1
mark^#(s(X))	→	mark^#(X)	(52)

1	>	1
mark^#(pair(X1,X2))	→	mark^#(X1)	(54)

1	>	1

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