Certification Problem

Input (TPDB SRS_Standard/Trafo_06/un17)

The rewrite relation of the following TRS is considered.

b(b(b(x1)))	→	b(b(a(b(a(b(a(b(x1))))))))	(1)
b(a(b(b(x1))))	→	b(a(b(a(b(a(a(b(x1))))))))	(2)
b(b(a(b(a(b(a(a(b(x1)))))))))	→	b(b(b(b(a(b(x1))))))	(3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

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

b(b(b(x1)))	→	b(a(b(a(b(a(b(b(x1))))))))	(4)
b(b(a(b(x1))))	→	b(a(a(b(a(b(a(b(x1))))))))	(5)
b(a(a(b(a(b(a(b(b(x1)))))))))	→	b(a(b(b(b(b(x1))))))	(6)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

b_b(b_b(b_b(x1)))	→	b_a(a_b(b_a(a_b(b_a(a_b(b_b(b_b(x1))))))))	(7)
b_b(b_b(b_a(x1)))	→	b_a(a_b(b_a(a_b(b_a(a_b(b_b(b_a(x1))))))))	(8)
b_b(b_a(a_b(b_b(x1))))	→	b_a(a_a(a_b(b_a(a_b(b_a(a_b(b_b(x1))))))))	(9)
b_b(b_a(a_b(b_a(x1))))	→	b_a(a_a(a_b(b_a(a_b(b_a(a_b(b_a(x1))))))))	(10)
b_a(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_b(x1)))))))))	→	b_a(a_b(b_b(b_b(b_b(b_b(x1))))))	(11)
b_a(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_a(x1)))))))))	→	b_a(a_b(b_b(b_b(b_b(b_a(x1))))))	(12)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

b_b^#(b_b(b_b(x1)))	→	b_a^#(a_b(b_a(a_b(b_a(a_b(b_b(b_b(x1))))))))	(13)
b_b^#(b_b(b_b(x1)))	→	b_a^#(a_b(b_a(a_b(b_b(b_b(x1))))))	(14)
b_b^#(b_b(b_b(x1)))	→	b_a^#(a_b(b_b(b_b(x1))))	(15)
b_b^#(b_b(b_a(x1)))	→	b_a^#(a_b(b_a(a_b(b_a(a_b(b_b(b_a(x1))))))))	(16)
b_b^#(b_b(b_a(x1)))	→	b_a^#(a_b(b_a(a_b(b_b(b_a(x1))))))	(17)
b_b^#(b_b(b_a(x1)))	→	b_a^#(a_b(b_b(b_a(x1))))	(18)
b_b^#(b_a(a_b(b_b(x1))))	→	b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(x1))))))))	(19)
b_b^#(b_a(a_b(b_b(x1))))	→	b_a^#(a_b(b_a(a_b(b_b(x1)))))	(20)
b_b^#(b_a(a_b(b_a(x1))))	→	b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_a(x1))))))))	(21)
b_b^#(b_a(a_b(b_a(x1))))	→	b_a^#(a_b(b_a(a_b(b_a(x1)))))	(22)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_b(x1)))))))))	→	b_a^#(a_b(b_b(b_b(b_b(b_b(x1))))))	(23)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_b(x1)))))))))	→	b_b^#(b_b(b_b(b_b(x1))))	(24)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_b(x1)))))))))	→	b_b^#(b_b(b_b(x1)))	(25)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_a(x1)))))))))	→	b_a^#(a_b(b_b(b_b(b_b(b_a(x1))))))	(26)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_a(x1)))))))))	→	b_b^#(b_b(b_b(b_a(x1))))	(27)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_a(x1)))))))))	→	b_b^#(b_b(b_a(x1)))	(28)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

b_b^#(b_a(a_b(b_b(x1))))	→	b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(x1))))))))	(19)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_b(x1)))))))))	→	b_b^#(b_b(b_b(b_b(x1))))	(24)
b_b^#(b_a(a_b(b_a(x1))))	→	b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_a(x1))))))))	(21)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_b(x1)))))))))	→	b_b^#(b_b(b_b(x1)))	(25)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_a(x1)))))))))	→	b_b^#(b_b(b_b(b_a(x1))))	(27)
b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(b_a(x1)))))))))	→	b_b^#(b_b(b_a(x1)))	(28)

1.1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the integers

[b_b^#(x₁)]

=

1

0

0

+

1	0	0
0	0	0
0	0	0

· x₁

[b_a(x₁)]

=

0

0

0

+

0	0	1
0	1	0
0	0	0

· x₁

[a_b(x₁)]

=

0

0

0

+

0	1	0
1	0	0
0	0	1

· x₁

[b_b(x₁)]

=

0

0

1

+

1	0	0
1	1	0
1	0	0

· x₁

[b_a^#(x₁)]

=

0

0

0

+

0	0	1
0	0	0
0	0	0

· x₁

[a_a(x₁)]

=

0

0

0

+

0	0	0
1	0	0
1	0	0

· x₁

the pairs

b_b^#(b_a(a_b(b_b(x1))))	→	b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_b(x1))))))))	(19)
b_b^#(b_a(a_b(b_a(x1))))	→	b_a^#(a_a(a_b(b_a(a_b(b_a(a_b(b_a(x1))))))))	(21)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.