Certification Problem

Input (TPDB SRS_Standard/Trafo_06/dup12)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

b(b(d(d(b(b(x1))))))	→	b(b(d(d(c(c(x1))))))	(8)
c(c(a(a(b(b(x1))))))	→	c(c(b(b(x1))))	(9)
d(d(a(a(x1))))	→	c(c(d(d(x1))))	(10)
b(b(b(b(b(b(x1))))))	→	c(c(b(b(a(a(x1))))))	(11)
c(c(d(d(x1))))	→	d(d(b(b(x1))))	(12)
c(c(d(d(x1))))	→	d(d(b(b(d(d(x1))))))	(13)
c(c(a(a(d(d(x1))))))	→	b(b(b(b(x1))))	(14)

1.1 Rule Removal

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

[d(x₁)]	=	0 · x₁ + -∞
[a(x₁)]	=	1 · x₁ + -∞
[b(x₁)]	=	1 · x₁ + -∞
[c(x₁)]	=	1 · x₁ + -∞

all of the following rules can be deleted.

c(c(a(a(b(b(x1))))))

→

c(c(b(b(x1))))

(9)

1.1.1 Rule Removal

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

[d(x₁)]

1	1	0
0	0	1
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a(x₁)]

1	0	0
0	1	0
1	0	1

· x₁ +

0	0	0
0	0	0
1	0	0

[b(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[c(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

d(d(a(a(x1))))

→

c(c(d(d(x1))))

(10)

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

b^#(b(d(d(b(b(x1))))))	→	c^#(x1)	(15)
b^#(b(d(d(b(b(x1))))))	→	c^#(c(x1))	(16)
b^#(b(d(d(b(b(x1))))))	→	b^#(d(d(c(c(x1)))))	(17)
b^#(b(d(d(b(b(x1))))))	→	b^#(b(d(d(c(c(x1))))))	(18)
b^#(b(b(b(b(b(x1))))))	→	b^#(a(a(x1)))	(19)
b^#(b(b(b(b(b(x1))))))	→	b^#(b(a(a(x1))))	(20)
b^#(b(b(b(b(b(x1))))))	→	c^#(b(b(a(a(x1)))))	(21)
b^#(b(b(b(b(b(x1))))))	→	c^#(c(b(b(a(a(x1))))))	(22)
c^#(c(d(d(x1))))	→	b^#(x1)	(23)
c^#(c(d(d(x1))))	→	b^#(b(x1))	(24)
c^#(c(d(d(x1))))	→	b^#(d(d(x1)))	(25)
c^#(c(d(d(x1))))	→	b^#(b(d(d(x1))))	(26)
c^#(c(a(a(d(d(x1))))))	→	b^#(x1)	(27)
c^#(c(a(a(d(d(x1))))))	→	b^#(b(x1))	(28)
c^#(c(a(a(d(d(x1))))))	→	b^#(b(b(x1)))	(29)
c^#(c(a(a(d(d(x1))))))	→	b^#(b(b(b(x1))))	(30)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

c^#(c(a(a(d(d(x1))))))	→	b^#(b(b(b(x1))))	(30)
b^#(b(d(d(b(b(x1))))))	→	b^#(b(d(d(c(c(x1))))))	(18)
b^#(b(d(d(b(b(x1))))))	→	c^#(c(x1))	(16)
c^#(c(a(a(d(d(x1))))))	→	b^#(b(b(x1)))	(29)
b^#(b(d(d(b(b(x1))))))	→	c^#(x1)	(15)
c^#(c(a(a(d(d(x1))))))	→	b^#(b(x1))	(28)
c^#(c(a(a(d(d(x1))))))	→	b^#(x1)	(27)
c^#(c(d(d(x1))))	→	b^#(b(d(d(x1))))	(26)
c^#(c(d(d(x1))))	→	b^#(b(x1))	(24)
c^#(c(d(d(x1))))	→	b^#(x1)	(23)

1.1.1.1.1.1 Subterm Criterion Processor

We use the projection to multisets

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

to remove the pairs:

b^#(b(d(d(b(b(x1))))))	→	c^#(c(x1))	(16)
c^#(c(a(a(d(d(x1))))))	→	b^#(b(b(x1)))	(29)
b^#(b(d(d(b(b(x1))))))	→	c^#(x1)	(15)
c^#(c(a(a(d(d(x1))))))	→	b^#(b(x1))	(28)
c^#(c(a(a(d(d(x1))))))	→	b^#(x1)	(27)
c^#(c(d(d(x1))))	→	b^#(x1)	(23)

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

b^#(b(d(d(b(b(x1))))))

→

b^#(b(d(d(c(c(x1))))))

(18)

1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

[b^#(x₁)]

0	0	1	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

1	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[d(x₁)]

0	0	1
0	1	0
0	0	0
1	0	0

· x₁ +

1	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[a(x₁)]

1	0	0
0	1	1
0	1	0
1	0	0

· x₁ +

0	0	0	0
0	0	0	0
1	0	0	0
0	0	0	0

[b(x₁)]

0	0	0	0
0	0	0	0
0	0	0	1
0	1	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
1	0	0	0

[c(x₁)]

0	1	0
1	1	0
1	0	0
0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

together with the usable rules

b(b(d(d(b(b(x1))))))	→	b(b(d(d(c(c(x1))))))	(8)
b(b(b(b(b(b(x1))))))	→	c(c(b(b(a(a(x1))))))	(11)
c(c(d(d(x1))))	→	d(d(b(b(x1))))	(12)
c(c(d(d(x1))))	→	d(d(b(b(d(d(x1))))))	(13)
c(c(a(a(d(d(x1))))))	→	b(b(b(b(x1))))	(14)

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

b^#(b(d(d(b(b(x1))))))

→

b^#(b(d(d(c(c(x1))))))

(18)

could be deleted.

1.1.1.1.1.1.1.1.1 P is empty

There are no pairs anymore.