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 AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals

[a(x₁)]	=	1 · x₁ + 2
[b(x₁)]	=	1 · x₁ + 2
[C(x₁)]	=	1 · x₁ + 3
[c(x₁)]	=	1 · x₁ + 2
[A(x₁)]	=	1 · x₁ + 3
[B(x₁)]	=	1 · x₁ + 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 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1.1 Monotonic Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[B(x₁)]	=	3 + 1 · x₁
[a(x₁)]	=	2 + 1 · x₁
[c(x₁)]	=	2 + 1 · x₁
[A(x₁)]	=	3 + 1 · x₁
[b(x₁)]	=	2 + 1 · x₁
[C(x₁)]	=	3 + 1 · x₁
[B^#(x₁)]	=	2 + 2 · x₁
[A^#(x₁)]	=	2 + 2 · x₁
[C^#(x₁)]	=	2 + 2 · x₁

the pairs

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

and no rules could be deleted.

1.1.1.1.1 P is empty

There are no pairs anymore.