Certification Problem

Input (TPDB SRS_Standard/Zantema_06/beans3)

The rewrite relation of the following TRS is considered.

b(a(a(x1)))	→	a(b(c(x1)))	(1)
c(a(x1))	→	a(c(x1))	(2)
b(c(a(x1)))	→	a(b(c(x1)))	(3)
c(b(x1))	→	d(x1)	(4)
a(d(x1))	→	d(a(x1))	(5)
d(x1)	→	b(a(x1))	(6)
L(a(a(x1)))	→	L(a(b(c(x1))))	(7)
c(R(x1))	→	c(b(R(x1)))	(8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

b^#(a(a(x1)))	→	c^#(x1)	(9)
b^#(a(a(x1)))	→	b^#(c(x1))	(10)
b^#(a(a(x1)))	→	a^#(b(c(x1)))	(11)
c^#(a(x1))	→	c^#(x1)	(12)
c^#(a(x1))	→	a^#(c(x1))	(13)
b^#(c(a(x1)))	→	c^#(x1)	(14)
b^#(c(a(x1)))	→	b^#(c(x1))	(15)
b^#(c(a(x1)))	→	a^#(b(c(x1)))	(16)
c^#(b(x1))	→	d^#(x1)	(17)
a^#(d(x1))	→	a^#(x1)	(18)
a^#(d(x1))	→	d^#(a(x1))	(19)
d^#(x1)	→	a^#(x1)	(20)
d^#(x1)	→	b^#(a(x1))	(21)
L^#(a(a(x1)))	→	c^#(x1)	(22)
L^#(a(a(x1)))	→	b^#(c(x1))	(23)
L^#(a(a(x1)))	→	a^#(b(c(x1)))	(24)
L^#(a(a(x1)))	→	L^#(a(b(c(x1))))	(25)
c^#(R(x1))	→	b^#(R(x1))	(26)
c^#(R(x1))	→	c^#(b(R(x1)))	(27)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

L^#(a(a(x1)))

→

L^#(a(b(c(x1))))

(25)

1.1.1 Reduction Pair Processor with Usable Rules

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

[b(x₁)]	=	-2 · x₁ + 2
[d(x₁)]	=	0 · x₁ + 2
[R(x₁)]	=	2 · x₁ + 2
[L^#(x₁)]	=	-5 · x₁ + 0
[a(x₁)]	=	2 · x₁ + 4
[c(x₁)]	=	2 · x₁ + 4

together with the usable rules

c(a(x1))	→	a(c(x1))	(2)
c(b(x1))	→	d(x1)	(4)
c(R(x1))	→	c(b(R(x1)))	(8)
a(d(x1))	→	d(a(x1))	(5)
d(x1)	→	b(a(x1))	(6)
b(a(a(x1)))	→	a(b(c(x1)))	(1)
b(c(a(x1)))	→	a(b(c(x1)))	(3)

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

L^#(a(a(x1)))

→

L^#(a(b(c(x1))))

(25)

could be deleted.

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

a^#(d(x1))	→	d^#(a(x1))	(19)
d^#(x1)	→	b^#(a(x1))	(21)
b^#(a(a(x1)))	→	a^#(b(c(x1)))	(11)
a^#(d(x1))	→	a^#(x1)	(18)
b^#(a(a(x1)))	→	b^#(c(x1))	(10)
b^#(c(a(x1)))	→	a^#(b(c(x1)))	(16)
b^#(c(a(x1)))	→	b^#(c(x1))	(15)
b^#(c(a(x1)))	→	c^#(x1)	(14)
c^#(R(x1))	→	c^#(b(R(x1)))	(27)
c^#(b(x1))	→	d^#(x1)	(17)
d^#(x1)	→	a^#(x1)	(20)
c^#(a(x1))	→	a^#(c(x1))	(13)
c^#(a(x1))	→	c^#(x1)	(12)
b^#(a(a(x1)))	→	c^#(x1)	(9)

1.1.2 Subterm Criterion Processor

We use the projection to multisets

π(d^#)	=	{ 1, 1 }
π(a^#)	=	{ 1, 1 }
π(c^#)	=	{ 1, 1 }
π(b^#)	=	{ 1 }
π(d)	=	{ 1, 1 }
π(c)	=	{ 1, 1 }
π(b)	=	{ 1 }
π(a)	=	{ 1, 1 }

to remove the pairs:

a^#(d(x1))	→	a^#(x1)	(18)
b^#(a(a(x1)))	→	b^#(c(x1))	(10)
b^#(c(a(x1)))	→	b^#(c(x1))	(15)
b^#(c(a(x1)))	→	c^#(x1)	(14)
c^#(a(x1))	→	c^#(x1)	(12)
b^#(a(a(x1)))	→	c^#(x1)	(9)

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

d^#(x1)	→	a^#(x1)	(20)
a^#(d(x1))	→	d^#(a(x1))	(19)
d^#(x1)	→	b^#(a(x1))	(21)
b^#(a(a(x1)))	→	a^#(b(c(x1)))	(11)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the

prec(d^#)	=	2	stat(d^#)	=	lex
prec(a^#)	=	0	stat(a^#)	=	lex
prec(b^#)	=	1	stat(b^#)	=	lex
prec(R)	=	0	stat(R)	=	lex
prec(d)	=	3	stat(d)	=	lex
prec(c)	=	0	stat(c)	=	lex
prec(b)	=	0	stat(b)	=	lex
prec(a)	=	0	stat(a)	=	lex

π(d^#)	=	[1]
π(a^#)	=	1
π(b^#)	=	[]
π(R)	=	1
π(d)	=	[1]
π(c)	=	[]
π(b)	=	[]
π(a)	=	1

together with the usable rules

a(d(x1))	→	d(a(x1))	(5)
d(x1)	→	b(a(x1))	(6)
b(a(a(x1)))	→	a(b(c(x1)))	(1)
b(c(a(x1)))	→	a(b(c(x1)))	(3)

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

d^#(x1)	→	a^#(x1)	(20)
a^#(d(x1))	→	d^#(a(x1))	(19)
d^#(x1)	→	b^#(a(x1))	(21)
b^#(a(a(x1)))	→	a^#(b(c(x1)))	(11)

could be deleted.

1.1.2.1.1.1 P is empty

There are no pairs anymore.