Certification Problem

Input (TPDB TRS_Standard/SK90/2.49)

The rewrite relation of the following TRS is considered.

a(c(d(x)))	→	c(x)	(1)
u(b(d(d(x))))	→	b(x)	(2)
v(a(a(x)))	→	u(v(x))	(3)
v(a(c(x)))	→	u(b(d(x)))	(4)
v(c(x))	→	b(x)	(5)
w(a(a(x)))	→	u(w(x))	(6)
w(a(c(x)))	→	u(b(d(x)))	(7)
w(c(x))	→	b(x)	(8)

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

d(c(a(x)))	→	c(x)	(9)
d(d(b(u(x))))	→	b(x)	(10)
a(a(v(x)))	→	v(u(x))	(11)
c(a(v(x)))	→	d(b(u(x)))	(12)
c(v(x))	→	b(x)	(13)
a(a(w(x)))	→	w(u(x))	(14)
c(a(w(x)))	→	d(b(u(x)))	(15)
c(w(x))	→	b(x)	(16)

1.1 Bounds

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

final states:

{0, 1, 2, 3, 4, 5, 6}

transitions:

d₀(0)	→	0
d₀(1)	→	0
d₀(2)	→	0
d₀(3)	→	0
d₀(4)	→	0
d₀(5)	→	0
d₀(6)	→	0
c₀(0)	→	1
c₀(1)	→	1
c₀(2)	→	1
c₀(3)	→	1
c₀(4)	→	1
c₀(5)	→	1
c₀(6)	→	1
a₀(0)	→	2
a₀(1)	→	2
a₀(2)	→	2
a₀(3)	→	2
a₀(4)	→	2
a₀(5)	→	2
a₀(6)	→	2
b₀(0)	→	3
b₀(1)	→	3
b₀(2)	→	3
b₀(3)	→	3
b₀(4)	→	3
b₀(5)	→	3
b₀(6)	→	3
u₀(0)	→	4
u₀(1)	→	4
u₀(2)	→	4
u₀(3)	→	4
u₀(4)	→	4
u₀(5)	→	4
u₀(6)	→	4
v₀(0)	→	5
v₀(1)	→	5
v₀(2)	→	5
v₀(3)	→	5
v₀(4)	→	5
v₀(5)	→	5
v₀(6)	→	5
w₀(0)	→	6
w₀(1)	→	6
w₀(2)	→	6
w₀(3)	→	6
w₀(4)	→	6
w₀(5)	→	6
w₀(6)	→	6
c₁(0)	→	0
c₁(1)	→	0
c₁(2)	→	0
c₁(3)	→	0
c₁(4)	→	0
c₁(5)	→	0
c₁(6)	→	0
b₁(0)	→	0
b₁(1)	→	0
b₁(2)	→	0
b₁(3)	→	0
b₁(4)	→	0
b₁(5)	→	0
b₁(6)	→	0
u₁(0)	→	7
v₁(7)	→	2
u₁(1)	→	7
u₁(2)	→	7
u₁(3)	→	7
u₁(4)	→	7
u₁(5)	→	7
u₁(6)	→	7
b₁(7)	→	8
d₁(8)	→	1
w₁(7)	→	2
u₁(7)	→	7
b₂(7)	→	0
0	→	1
1	→	0
8	→	0