Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z069)

The rewrite relation of the following TRS is considered.

a(b(x1))	→	C(x1)	(1)
b(c(x1))	→	A(x1)	(2)
c(a(x1))	→	B(x1)	(3)
A(C(x1))	→	b(x1)	(4)
C(B(x1))	→	a(x1)	(5)
B(A(x1))	→	c(x1)	(6)
a(a(a(a(x1))))	→	A(A(A(x1)))	(7)
A(A(A(A(x1))))	→	a(a(a(x1)))	(8)
b(b(b(b(x1))))	→	B(B(B(x1)))	(9)
B(B(B(B(x1))))	→	b(b(b(x1)))	(10)
c(c(c(c(x1))))	→	C(C(C(x1)))	(11)
C(C(C(C(x1))))	→	c(c(c(x1)))	(12)
B(a(a(a(x1))))	→	c(A(A(A(x1))))	(13)
A(A(A(b(x1))))	→	a(a(a(C(x1))))	(14)
C(b(b(b(x1))))	→	a(B(B(B(x1))))	(15)
B(B(B(c(x1))))	→	b(b(b(A(x1))))	(16)
A(c(c(c(x1))))	→	b(C(C(C(x1))))	(17)
C(C(C(a(x1))))	→	c(c(c(B(x1))))	(18)
a(A(x1))	→	x1	(19)
A(a(x1))	→	x1	(20)
b(B(x1))	→	x1	(21)
B(b(x1))	→	x1	(22)
c(C(x1))	→	x1	(23)
C(c(x1))	→	x1	(24)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

B^#(A(x1))	→	c^#(x1)	(25)
C^#(b(b(b(x1))))	→	B^#(x1)	(26)
A^#(c(c(c(x1))))	→	C^#(C(x1))	(27)
c^#(a(x1))	→	B^#(x1)	(28)
C^#(C(C(a(x1))))	→	c^#(c(B(x1)))	(29)
C^#(b(b(b(x1))))	→	B^#(B(x1))	(30)
C^#(b(b(b(x1))))	→	B^#(B(B(x1)))	(31)
A^#(A(A(A(x1))))	→	a^#(a(a(x1)))	(32)
C^#(C(C(a(x1))))	→	c^#(B(x1))	(33)
C^#(C(C(a(x1))))	→	B^#(x1)	(34)
A^#(A(A(A(x1))))	→	a^#(a(x1))	(35)
B^#(a(a(a(x1))))	→	A^#(x1)	(36)
C^#(b(b(b(x1))))	→	a^#(B(B(B(x1))))	(37)
C^#(C(C(C(x1))))	→	c^#(c(c(x1)))	(38)
b^#(b(b(b(x1))))	→	B^#(x1)	(39)
c^#(c(c(c(x1))))	→	C^#(C(x1))	(40)
B^#(B(B(B(x1))))	→	b^#(b(x1))	(41)
B^#(B(B(B(x1))))	→	b^#(b(b(x1)))	(42)
C^#(C(C(a(x1))))	→	c^#(c(c(B(x1))))	(43)
c^#(c(c(c(x1))))	→	C^#(x1)	(44)
B^#(B(B(c(x1))))	→	b^#(b(b(A(x1))))	(45)
C^#(C(C(C(x1))))	→	c^#(c(x1))	(46)
A^#(c(c(c(x1))))	→	C^#(x1)	(47)
B^#(B(B(B(x1))))	→	b^#(x1)	(48)
a^#(a(a(a(x1))))	→	A^#(A(A(x1)))	(49)
b^#(b(b(b(x1))))	→	B^#(B(B(x1)))	(50)
A^#(A(A(A(x1))))	→	a^#(x1)	(51)
c^#(c(c(c(x1))))	→	C^#(C(C(x1)))	(52)
B^#(B(B(c(x1))))	→	b^#(A(x1))	(53)
B^#(a(a(a(x1))))	→	A^#(A(x1))	(54)
A^#(C(x1))	→	b^#(x1)	(55)
A^#(c(c(c(x1))))	→	C^#(C(C(x1)))	(56)
a^#(a(a(a(x1))))	→	A^#(x1)	(57)
B^#(B(B(c(x1))))	→	A^#(x1)	(58)
A^#(c(c(c(x1))))	→	b^#(C(C(C(x1))))	(59)
A^#(A(A(b(x1))))	→	a^#(a(C(x1)))	(60)
B^#(B(B(c(x1))))	→	b^#(b(A(x1)))	(61)
A^#(A(A(b(x1))))	→	C^#(x1)	(62)
C^#(B(x1))	→	a^#(x1)	(63)
a^#(b(x1))	→	C^#(x1)	(64)
a^#(a(a(a(x1))))	→	A^#(A(x1))	(65)
A^#(A(A(b(x1))))	→	a^#(a(a(C(x1))))	(66)
B^#(a(a(a(x1))))	→	c^#(A(A(A(x1))))	(67)
b^#(c(x1))	→	A^#(x1)	(68)
b^#(b(b(b(x1))))	→	B^#(B(x1))	(69)
C^#(C(C(C(x1))))	→	c^#(x1)	(70)
B^#(a(a(a(x1))))	→	A^#(A(A(x1)))	(71)
A^#(A(A(b(x1))))	→	a^#(C(x1))	(72)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

A^#(A(A(b(x1))))	→	a^#(C(x1))	(72)
B^#(B(B(B(x1))))	→	b^#(x1)	(48)
B^#(a(a(a(x1))))	→	A^#(A(A(x1)))	(71)
A^#(c(c(c(x1))))	→	C^#(x1)	(47)
C^#(C(C(C(x1))))	→	c^#(c(x1))	(46)
C^#(C(C(C(x1))))	→	c^#(x1)	(70)
B^#(B(B(c(x1))))	→	b^#(b(b(A(x1))))	(45)
c^#(c(c(c(x1))))	→	C^#(x1)	(44)
b^#(b(b(b(x1))))	→	B^#(B(x1))	(69)
C^#(C(C(a(x1))))	→	c^#(c(c(B(x1))))	(43)
b^#(c(x1))	→	A^#(x1)	(68)
B^#(B(B(B(x1))))	→	b^#(b(b(x1)))	(42)
B^#(a(a(a(x1))))	→	c^#(A(A(A(x1))))	(67)
B^#(B(B(B(x1))))	→	b^#(b(x1))	(41)
A^#(A(A(b(x1))))	→	a^#(a(a(C(x1))))	(66)
a^#(a(a(a(x1))))	→	A^#(A(x1))	(65)
a^#(b(x1))	→	C^#(x1)	(64)
C^#(B(x1))	→	a^#(x1)	(63)
c^#(c(c(c(x1))))	→	C^#(C(x1))	(40)
b^#(b(b(b(x1))))	→	B^#(x1)	(39)
C^#(C(C(C(x1))))	→	c^#(c(c(x1)))	(38)
B^#(B(B(c(x1))))	→	b^#(b(A(x1)))	(61)
A^#(A(A(b(x1))))	→	C^#(x1)	(62)
A^#(A(A(b(x1))))	→	a^#(a(C(x1)))	(60)
C^#(b(b(b(x1))))	→	a^#(B(B(B(x1))))	(37)
B^#(a(a(a(x1))))	→	A^#(x1)	(36)
A^#(c(c(c(x1))))	→	b^#(C(C(C(x1))))	(59)
A^#(A(A(A(x1))))	→	a^#(a(x1))	(35)
B^#(B(B(c(x1))))	→	A^#(x1)	(58)
C^#(C(C(a(x1))))	→	B^#(x1)	(34)
a^#(a(a(a(x1))))	→	A^#(x1)	(57)
A^#(c(c(c(x1))))	→	C^#(C(C(x1)))	(56)
C^#(C(C(a(x1))))	→	c^#(B(x1))	(33)
A^#(C(x1))	→	b^#(x1)	(55)
B^#(a(a(a(x1))))	→	A^#(A(x1))	(54)
A^#(A(A(A(x1))))	→	a^#(a(a(x1)))	(32)
B^#(B(B(c(x1))))	→	b^#(A(x1))	(53)
C^#(b(b(b(x1))))	→	B^#(B(B(x1)))	(31)
C^#(b(b(b(x1))))	→	B^#(B(x1))	(30)
c^#(c(c(c(x1))))	→	C^#(C(C(x1)))	(52)
C^#(C(C(a(x1))))	→	c^#(c(B(x1)))	(29)
A^#(A(A(A(x1))))	→	a^#(x1)	(51)
b^#(b(b(b(x1))))	→	B^#(B(B(x1)))	(50)
c^#(a(x1))	→	B^#(x1)	(28)
A^#(c(c(c(x1))))	→	C^#(C(x1))	(27)
C^#(b(b(b(x1))))	→	B^#(x1)	(26)
B^#(A(x1))	→	c^#(x1)	(25)
a^#(a(a(a(x1))))	→	A^#(A(A(x1)))	(49)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 30614
[b(x₁)]	=	x₁ + 30614
[B^#(x₁)]	=	x₁ + 1
[c(x₁)]	=	x₁ + 30614
[C(x₁)]	=	x₁ + 30614
[B(x₁)]	=	x₁ + 30614
[C^#(x₁)]	=	x₁ + 30613
[A(x₁)]	=	x₁ + 30614
[A^#(x₁)]	=	x₁ + 30613
[c^#(x₁)]	=	x₁ + 0
[a^#(x₁)]	=	x₁ + 30612
[b^#(x₁)]	=	x₁ + 0

together with the usable rules

C(C(C(a(x1))))	→	c(c(c(B(x1))))	(18)
A(C(x1))	→	b(x1)	(4)
C(b(b(b(x1))))	→	a(B(B(B(x1))))	(15)
A(A(A(A(x1))))	→	a(a(a(x1)))	(8)
a(b(x1))	→	C(x1)	(1)
c(a(x1))	→	B(x1)	(3)
B(B(B(c(x1))))	→	b(b(b(A(x1))))	(16)
b(B(x1))	→	x1	(21)
a(A(x1))	→	x1	(19)
A(c(c(c(x1))))	→	b(C(C(C(x1))))	(17)
B(b(x1))	→	x1	(22)
C(B(x1))	→	a(x1)	(5)
B(B(B(B(x1))))	→	b(b(b(x1)))	(10)
a(a(a(a(x1))))	→	A(A(A(x1)))	(7)
A(a(x1))	→	x1	(20)
A(A(A(b(x1))))	→	a(a(a(C(x1))))	(14)
C(C(C(C(x1))))	→	c(c(c(x1)))	(12)
c(C(x1))	→	x1	(23)
C(c(x1))	→	x1	(24)
c(c(c(c(x1))))	→	C(C(C(x1)))	(11)
b(b(b(b(x1))))	→	B(B(B(x1)))	(9)
B(a(a(a(x1))))	→	c(A(A(A(x1))))	(13)
B(A(x1))	→	c(x1)	(6)
b(c(x1))	→	A(x1)	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

A^#(A(A(b(x1))))	→	a^#(C(x1))	(72)
B^#(B(B(B(x1))))	→	b^#(x1)	(48)
B^#(a(a(a(x1))))	→	A^#(A(A(x1)))	(71)
A^#(c(c(c(x1))))	→	C^#(x1)	(47)
C^#(C(C(C(x1))))	→	c^#(c(x1))	(46)
C^#(C(C(C(x1))))	→	c^#(x1)	(70)
B^#(B(B(c(x1))))	→	b^#(b(b(A(x1))))	(45)
c^#(c(c(c(x1))))	→	C^#(x1)	(44)
b^#(b(b(b(x1))))	→	B^#(B(x1))	(69)
C^#(C(C(a(x1))))	→	c^#(c(c(B(x1))))	(43)
b^#(c(x1))	→	A^#(x1)	(68)
B^#(B(B(B(x1))))	→	b^#(b(b(x1)))	(42)
B^#(a(a(a(x1))))	→	c^#(A(A(A(x1))))	(67)
B^#(B(B(B(x1))))	→	b^#(b(x1))	(41)
A^#(A(A(b(x1))))	→	a^#(a(a(C(x1))))	(66)
a^#(a(a(a(x1))))	→	A^#(A(x1))	(65)
a^#(b(x1))	→	C^#(x1)	(64)
C^#(B(x1))	→	a^#(x1)	(63)
c^#(c(c(c(x1))))	→	C^#(C(x1))	(40)
b^#(b(b(b(x1))))	→	B^#(x1)	(39)
C^#(C(C(C(x1))))	→	c^#(c(c(x1)))	(38)
B^#(B(B(c(x1))))	→	b^#(b(A(x1)))	(61)
A^#(A(A(b(x1))))	→	C^#(x1)	(62)
A^#(A(A(b(x1))))	→	a^#(a(C(x1)))	(60)
C^#(b(b(b(x1))))	→	a^#(B(B(B(x1))))	(37)
B^#(a(a(a(x1))))	→	A^#(x1)	(36)
A^#(c(c(c(x1))))	→	b^#(C(C(C(x1))))	(59)
A^#(A(A(A(x1))))	→	a^#(a(x1))	(35)
B^#(B(B(c(x1))))	→	A^#(x1)	(58)
C^#(C(C(a(x1))))	→	B^#(x1)	(34)
a^#(a(a(a(x1))))	→	A^#(x1)	(57)
A^#(c(c(c(x1))))	→	C^#(C(C(x1)))	(56)
C^#(C(C(a(x1))))	→	c^#(B(x1))	(33)
A^#(C(x1))	→	b^#(x1)	(55)
B^#(a(a(a(x1))))	→	A^#(A(x1))	(54)
A^#(A(A(A(x1))))	→	a^#(a(a(x1)))	(32)
B^#(B(B(c(x1))))	→	b^#(A(x1))	(53)
C^#(b(b(b(x1))))	→	B^#(B(B(x1)))	(31)
C^#(b(b(b(x1))))	→	B^#(B(x1))	(30)
c^#(c(c(c(x1))))	→	C^#(C(C(x1)))	(52)
C^#(C(C(a(x1))))	→	c^#(c(B(x1)))	(29)
A^#(A(A(A(x1))))	→	a^#(x1)	(51)
b^#(b(b(b(x1))))	→	B^#(B(B(x1)))	(50)
c^#(a(x1))	→	B^#(x1)	(28)
A^#(c(c(c(x1))))	→	C^#(C(x1))	(27)
C^#(b(b(b(x1))))	→	B^#(x1)	(26)
B^#(A(x1))	→	c^#(x1)	(25)
a^#(a(a(a(x1))))	→	A^#(A(A(x1)))	(49)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.