Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z047)

The rewrite relation of the following TRS is considered.

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

→

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

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

→

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

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