Certification Problem

Input (TPDB TRS_Standard/Rubio_04/lindau)

The rewrite relation of the following TRS is considered.

c(b(a(X)))	→	a(a(b(b(c(c(X))))))	(1)
a(X)	→	e	(2)
b(X)	→	e	(3)
c(X)	→	e	(4)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Bounds

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

final states:

{0, 1, 2, 3}

transitions:

c₀(0)	→	0
c₀(1)	→	0
c₀(2)	→	0
c₀(3)	→	0
b₀(0)	→	1
b₀(1)	→	1
b₀(2)	→	1
b₀(3)	→	1
a₀(0)	→	2
a₀(1)	→	2
a₀(2)	→	2
a₀(3)	→	2
e₀	→	3
c₁(0)	→	8
c₁(8)	→	7
b₁(7)	→	6
b₁(6)	→	5
a₁(5)	→	4
a₁(4)	→	0
c₁(1)	→	8
c₁(2)	→	8
c₁(3)	→	8
e₁	→	2
c₁(4)	→	8
e₂	→	0
2	→	1
2	→	0
0	→	8
0	→	4
0	→	6
0	→	5
0	→	7