Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z064)

The rewrite relation of the following TRS is considered.

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

→

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

(1)

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

→

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

(2)

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:

b₀(0)	→	0
b₀(1)	→	0
b₀(2)	→	0
c₀(0)	→	1
c₀(1)	→	1
c₀(2)	→	1
a₀(0)	→	2
a₀(1)	→	2
a₀(2)	→	2
a₁(0)	→	8
c₁(8)	→	7
b₁(7)	→	6
b₁(6)	→	5
b₁(5)	→	4
a₁(4)	→	3
c₁(3)	→	0
a₁(1)	→	8
a₁(2)	→	8
a₁(5)	→	8
a₂(6)	→	14
c₂(14)	→	13
b₂(13)	→	12
b₂(12)	→	11
b₂(11)	→	10
a₂(10)	→	9
c₂(9)	→	0
a₁(11)	→	8
a₂(7)	→	14
c₂(9)	→	11
a₂(12)	→	14
a₃(13)	→	20
c₃(20)	→	19
b₃(19)	→	18
b₃(18)	→	17
b₃(17)	→	16
a₃(16)	→	15
c₃(15)	→	11
0	→	5
0	→	4