Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z002)

The rewrite relation of the following TRS is considered.

b(c(a(x1)))	→	a(b(a(b(x1))))	(1)
b(x1)	→	c(c(x1))	(2)
a(a(x1))	→	a(c(b(a(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

a(c(b(x1)))	→	b(a(b(a(x1))))	(4)
b(x1)	→	c(c(x1))	(2)
a(a(x1))	→	a(b(c(a(x1))))	(5)

1.1 Bounds

The given TRS is match-(raise)-bounded by 3. This is shown by the following automaton.

final states:

{0, 1, 2}

transitions:

a₀(0)	→	0
a₀(1)	→	0
a₀(2)	→	0
c₀(0)	→	1
c₀(1)	→	1
c₀(2)	→	1
b₀(0)	→	2
b₀(1)	→	2
b₀(2)	→	2
a₁(0)	→	5
b₁(5)	→	4
a₁(4)	→	3
b₁(3)	→	0
a₁(1)	→	5
a₁(2)	→	5
c₁(0)	→	6
c₁(6)	→	2
c₁(1)	→	6
c₁(2)	→	6
c₁(5)	→	8
b₁(8)	→	7
a₁(7)	→	0
a₁(3)	→	5
c₂(3)	→	9
c₂(9)	→	0
c₂(5)	→	9
c₂(9)	→	4
c₂(8)	→	9
c₂(9)	→	7
a₂(7)	→	12
c₂(12)	→	11
b₂(11)	→	10
a₂(10)	→	0
a₂(4)	→	12
c₃(11)	→	13
c₃(13)	→	10
a₁(10)	→	0
0	→	5
9	→	11