Certification Problem

Input (TPDB SRS_Standard/Trafo_06/dup11)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

[C(x₁)]

x₁ +

[B(x₁)]

x₁ +

[A(x₁)]

x₁ +

[c(x₁)]

x₁ +

2/3

[b(x₁)]

x₁ +

2/3

[a(x₁)]

x₁ +

2/3

all of the following rules can be deleted.

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

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

C^#(C(C(C(C(C(a(a(x1))))))))	→	B^#(x1)	(25)
C^#(C(C(C(C(C(a(a(x1))))))))	→	B^#(B(x1))	(26)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(x1)	(27)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(x1))	(28)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(B(x1)))	(29)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(B(B(x1))))	(30)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(B(B(B(x1)))))	(31)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(B(B(B(B(x1))))))	(32)
B^#(B(B(B(B(B(c(c(x1))))))))	→	A^#(x1)	(33)
B^#(B(B(B(B(B(c(c(x1))))))))	→	A^#(A(x1))	(34)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(x1)	(35)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(x1))	(36)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(A(x1)))	(37)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(A(A(x1))))	(38)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(A(A(A(x1)))))	(39)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(A(A(A(A(x1))))))	(40)
A^#(A(A(A(A(A(b(b(x1))))))))	→	C^#(x1)	(41)
A^#(A(A(A(A(A(b(b(x1))))))))	→	C^#(C(x1))	(42)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(x1)	(43)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(x1))	(44)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(C(x1)))	(45)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(C(C(x1))))	(46)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(C(C(C(x1)))))	(47)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(C(C(C(C(x1))))))	(48)

1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

[C(x₁)]

x₁ +

[B(x₁)]

x₁ +

[A(x₁)]

x₁ +

[c(x₁)]

x₁ +

2/3

[b(x₁)]

x₁ +

2/3

[a(x₁)]

x₁ +

2/3

[C^#(x₁)]

x₁ +

[B^#(x₁)]

x₁ +

[A^#(x₁)]

x₁ +

together with the usable rules

B(B(a(a(a(a(a(a(a(a(x1))))))))))	→	c(c(A(A(A(A(A(A(x1))))))))	(13)
A(A(A(A(A(A(b(b(x1))))))))	→	a(a(a(a(a(a(a(a(C(C(x1))))))))))	(14)
C(C(b(b(b(b(b(b(b(b(x1))))))))))	→	a(a(B(B(B(B(B(B(x1))))))))	(15)
B(B(B(B(B(B(c(c(x1))))))))	→	b(b(b(b(b(b(b(b(A(A(x1))))))))))	(16)
A(A(c(c(c(c(c(c(c(c(x1))))))))))	→	b(b(C(C(C(C(C(C(x1))))))))	(17)
C(C(C(C(C(C(a(a(x1))))))))	→	c(c(c(c(c(c(c(c(B(B(x1))))))))))	(18)

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

C^#(C(C(C(C(C(a(a(x1))))))))	→	B^#(x1)	(25)
C^#(C(C(C(C(C(a(a(x1))))))))	→	B^#(B(x1))	(26)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(x1)	(27)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(x1))	(28)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(B(x1)))	(29)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(B(B(x1))))	(30)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(B(B(B(x1)))))	(31)
C^#(C(b(b(b(b(b(b(b(b(x1))))))))))	→	B^#(B(B(B(B(B(x1))))))	(32)
B^#(B(B(B(B(B(c(c(x1))))))))	→	A^#(x1)	(33)
B^#(B(B(B(B(B(c(c(x1))))))))	→	A^#(A(x1))	(34)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(x1)	(35)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(x1))	(36)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(A(x1)))	(37)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(A(A(x1))))	(38)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(A(A(A(x1)))))	(39)
B^#(B(a(a(a(a(a(a(a(a(x1))))))))))	→	A^#(A(A(A(A(A(x1))))))	(40)
A^#(A(A(A(A(A(b(b(x1))))))))	→	C^#(x1)	(41)
A^#(A(A(A(A(A(b(b(x1))))))))	→	C^#(C(x1))	(42)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(x1)	(43)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(x1))	(44)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(C(x1)))	(45)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(C(C(x1))))	(46)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(C(C(C(x1)))))	(47)
A^#(A(c(c(c(c(c(c(c(c(x1))))))))))	→	C^#(C(C(C(C(C(x1))))))	(48)

and no rules could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.