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

1 Rule Removal

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

[cons(x₁, x₂)]

1	0	0
0	1	1
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[tail(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[a__incr(x₁)]

1	0	0
0	0	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
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__pairs]

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__nats]

0	0	0
0	0	0
0	0	0

[a__odds]

0	0	0
0	0	0
0	0	0

[head(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[a__head(x₁)]

1	1	1
0	1	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[pairs]

0	0	0
0	0	0
0	0	0

[odds]

0	0	0
0	0	0
0	0	0

[nats]

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

a__tail(cons(X,XS))

→

mark(XS)

(6)

1.1 Rule Removal

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

[cons(x₁, x₂)]

1	1	1
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

[tail(x₁)]

1	1	0
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[a__incr(x₁)]

1	0	0
0	1	1
0	1	1

· 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
0	1	1
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__pairs]

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	1
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__nats]

0	0	0
0	0	0
0	0	0

[a__odds]

0	0	0
0	0	0
0	0	0

[head(x₁)]

1	0	0
0	0	0
0	1	1

· x₁ +

1	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	1	0
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[a__head(x₁)]

1	0	0
0	1	0
0	1	1

· x₁ +

1	0	0
0	0	0
0	0	0

[mark(x₁)]

1	1	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[pairs]

0	0	0
0	0	0
0	0	0

[odds]

0	0	0
0	0	0
0	0	0

[nats]

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

a__head(cons(X,XS))

→

mark(X)

(5)

1.1.1 Rule Removal

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

[cons(x₁, x₂)]

1	0	1
0	0	1
0	1	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[tail(x₁)]

1	0	1
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__incr(x₁)]

1	0	1
0	1	1
0	1	1

· 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
0	1	1
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__pairs]

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[a__nats]

1	0	0
1	0	0
1	0	0

[a__odds]

0	0	0
0	0	0
0	0	0

[head(x₁)]

1	0	1
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	0	1
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__head(x₁)]

1	0	1
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	1
0	0	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[pairs]

0	0	0
0	0	0
0	0	0

[odds]

0	0	0
0	0	0
0	0	0

[nats]

0	0	0
1	0	0
1	0	0

all of the following rules can be deleted.

a__nats	→	cons(0,incr(nats))	(1)
a__nats	→	nats	(17)

1.1.1.1 Rule Removal

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

[cons(x₁, x₂)]

1	0	0
0	0	0
1	0	0

· x₁ +

1	0	0
0	0	0
1	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[tail(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
1	0	0

· x₁ +

0	0	0
1	0	0
1	0	0

[0]

0	0	0
0	0	0
0	0	0

[incr(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[nil]

1	0	0
0	0	0
0	0	0

[a__pairs]

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	0
1	0	1
1	1	1

· x₁ +

0	0	0
0	0	0
1	0	0

[a__nats]

0	0	0
0	0	0
1	0	0

[a__odds]

0	0	0
1	0	0
1	0	0

[head(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__head(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[mark(x₁)]

1	0	0
0	0	1
0	1	1

· x₁ +

0	0	0
0	0	0
1	0	0

[pairs]

0	0	0
0	0	0
0	0	0

[odds]

0	0	0
1	0	0
1	0	0

[nats]

1	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

mark(nats)

→

a__nats

(7)

1.1.1.1.1 Rule Removal

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

[cons(x₁, x₂)]

1	0	1
0	1	0
0	1	1

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[tail(x₁)]

1	0	1
0	1	0
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[a__incr(x₁)]

1	0	1
0	1	1
0	0	1

· 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
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__pairs]

0	0	0
0	0	0
0	0	0

[s(x₁)]

1	0	1
0	1	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__odds]

1	0	0
0	0	0
1	0	0

[head(x₁)]

1	0	0
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	1	1
0	1	0
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[a__head(x₁)]

1	0	0
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	1	1
0	1	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[pairs]

0	0	0
0	0	0
0	0	0

[odds]

0	0	0
0	0	0
1	0	0

all of the following rules can be deleted.

a__odds	→	a__incr(a__pairs)	(3)
a__odds	→	odds	(19)

1.1.1.1.1.1 Rule Removal

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

[cons(x₁, x₂)]

1	1	0
1	1	0
0	0	0

· x₁ +

1	1	0
1	0	0
0	0	0

· x₂ +

1	0	0
1	0	0
0	0	0

[tail(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__incr(x₁)]

1	1	0
1	0	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	1	0
1	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__pairs]

1	0	0
1	0	0
0	0	0

[s(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__odds]

0	0	0
0	0	0
0	0	0

[head(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__tail(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__head(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

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

[pairs]

1	0	0
1	0	0
0	0	0

[odds]

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

a__incr(cons(X,XS))

→

cons(s(mark(X)),incr(XS))

(4)

1.1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

prec(nil)	=	10	weight(nil)	=	4
prec(tail)	=	2	weight(tail)	=	2
prec(head)	=	1	weight(head)	=	1
prec(pairs)	=	14	weight(pairs)	=	4
prec(a__tail)	=	3	weight(a__tail)	=	2
prec(a__head)	=	12	weight(a__head)	=	1
prec(s)	=	0	weight(s)	=	4
prec(mark)	=	13	weight(mark)	=	2
prec(a__incr)	=	9	weight(a__incr)	=	1
prec(a__odds)	=	4	weight(a__odds)	=	1
prec(odds)	=	7	weight(odds)	=	1
prec(a__pairs)	=	5	weight(a__pairs)	=	6
prec(cons)	=	6	weight(cons)	=	1
prec(incr)	=	8	weight(incr)	=	1
prec(0)	=	11	weight(0)	=	1

all of the following rules can be deleted.

a__pairs	→	cons(0,incr(odds))	(2)
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__pairs	→	pairs	(18)
a__incr(X)	→	incr(X)	(20)
a__head(X)	→	head(X)	(21)
a__tail(X)	→	tail(X)	(22)

1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.