Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z070)

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(a(x1)))))	→	A(A(A(x1)))	(7)
A(A(A(A(x1))))	→	a(a(a(a(x1))))	(8)
b(b(b(b(b(x1)))))	→	B(B(B(x1)))	(9)
B(B(B(B(x1))))	→	b(b(b(b(x1))))	(10)
c(c(c(c(c(x1)))))	→	C(C(C(x1)))	(11)
C(C(C(C(x1))))	→	c(c(c(c(x1))))	(12)
B(a(a(a(a(x1)))))	→	c(A(A(A(x1))))	(13)
A(A(A(b(x1))))	→	a(a(a(a(C(x1)))))	(14)
C(b(b(b(b(x1)))))	→	a(B(B(B(x1))))	(15)
B(B(B(c(x1))))	→	b(b(b(b(A(x1)))))	(16)
A(c(c(c(c(x1)))))	→	b(C(C(C(x1))))	(17)
C(C(C(a(x1))))	→	c(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)
A^#(A(A(A(x1))))	→	a^#(a(x1))	(26)
C^#(B(x1))	→	a^#(x1)	(27)
B^#(B(B(c(x1))))	→	b^#(b(b(A(x1))))	(28)
C^#(b(b(b(b(x1)))))	→	B^#(B(B(x1)))	(29)
A^#(A(A(A(x1))))	→	a^#(a(a(x1)))	(30)
A^#(A(A(A(x1))))	→	a^#(a(a(a(x1))))	(31)
B^#(B(B(c(x1))))	→	b^#(A(x1))	(32)
C^#(b(b(b(b(x1)))))	→	B^#(B(x1))	(33)
C^#(C(C(a(x1))))	→	c^#(B(x1))	(34)
C^#(b(b(b(b(x1)))))	→	B^#(x1)	(35)
B^#(B(B(c(x1))))	→	A^#(x1)	(36)
B^#(a(a(a(a(x1)))))	→	A^#(x1)	(37)
a^#(b(x1))	→	C^#(x1)	(38)
C^#(C(C(a(x1))))	→	c^#(c(c(B(x1))))	(39)
C^#(C(C(C(x1))))	→	c^#(c(c(c(x1))))	(40)
b^#(b(b(b(b(x1)))))	→	B^#(x1)	(41)
c^#(c(c(c(c(x1)))))	→	C^#(C(x1))	(42)
a^#(a(a(a(a(x1)))))	→	A^#(x1)	(43)
a^#(a(a(a(a(x1)))))	→	A^#(A(x1))	(44)
C^#(b(b(b(b(x1)))))	→	a^#(B(B(B(x1))))	(45)
c^#(c(c(c(c(x1)))))	→	C^#(x1)	(46)
A^#(c(c(c(c(x1)))))	→	C^#(C(C(x1)))	(47)
C^#(C(C(C(x1))))	→	c^#(c(c(x1)))	(48)
A^#(c(c(c(c(x1)))))	→	b^#(C(C(C(x1))))	(49)
C^#(C(C(a(x1))))	→	c^#(c(B(x1)))	(50)
A^#(C(x1))	→	b^#(x1)	(51)
B^#(B(B(B(x1))))	→	b^#(b(b(b(x1))))	(52)
A^#(A(A(b(x1))))	→	a^#(C(x1))	(53)
b^#(b(b(b(b(x1)))))	→	B^#(B(B(x1)))	(54)
c^#(a(x1))	→	B^#(x1)	(55)
c^#(c(c(c(c(x1)))))	→	C^#(C(C(x1)))	(56)
A^#(c(c(c(c(x1)))))	→	C^#(x1)	(57)
B^#(a(a(a(a(x1)))))	→	A^#(A(x1))	(58)
A^#(A(A(A(x1))))	→	a^#(x1)	(59)
B^#(B(B(B(x1))))	→	b^#(x1)	(60)
a^#(a(a(a(a(x1)))))	→	A^#(A(A(x1)))	(61)
B^#(B(B(c(x1))))	→	b^#(b(b(b(A(x1)))))	(62)
B^#(B(B(B(x1))))	→	b^#(b(x1))	(63)
A^#(A(A(b(x1))))	→	a^#(a(a(a(C(x1)))))	(64)
A^#(c(c(c(c(x1)))))	→	C^#(C(x1))	(65)
A^#(A(A(b(x1))))	→	a^#(a(C(x1)))	(66)
B^#(B(B(B(x1))))	→	b^#(b(b(x1)))	(67)
B^#(B(B(c(x1))))	→	b^#(b(A(x1)))	(68)
A^#(A(A(b(x1))))	→	C^#(x1)	(69)
C^#(C(C(C(x1))))	→	c^#(x1)	(70)
B^#(a(a(a(a(x1)))))	→	c^#(A(A(A(x1))))	(71)
b^#(c(x1))	→	A^#(x1)	(72)
C^#(C(C(a(x1))))	→	B^#(x1)	(73)
b^#(b(b(b(b(x1)))))	→	B^#(B(x1))	(74)
C^#(C(C(C(x1))))	→	c^#(c(x1))	(75)
B^#(a(a(a(a(x1)))))	→	A^#(A(A(x1)))	(76)
C^#(C(C(a(x1))))	→	c^#(c(c(c(B(x1)))))	(77)
A^#(A(A(b(x1))))	→	a^#(a(a(C(x1))))	(78)

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 566
[b(x₁)]	=	x₁ + 566
[B^#(x₁)]	=	x₁ + 565
[c(x₁)]	=	x₁ + 566
[C(x₁)]	=	x₁ + 849
[B(x₁)]	=	x₁ + 849
[C^#(x₁)]	=	x₁ + 565
[A(x₁)]	=	x₁ + 849
[A^#(x₁)]	=	x₁ + 565
[c^#(x₁)]	=	x₁ + 0
[a^#(x₁)]	=	x₁ + 281
[b^#(x₁)]	=	x₁ + 0

together with the usable rules

C(C(C(a(x1))))	→	c(c(c(c(B(x1)))))	(18)
A(C(x1))	→	b(x1)	(4)
C(b(b(b(b(x1)))))	→	a(B(B(B(x1))))	(15)
A(A(A(A(x1))))	→	a(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(b(A(x1)))))	(16)
b(B(x1))	→	x1	(21)
a(A(x1))	→	x1	(19)
A(c(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(b(x1))))	(10)
a(a(a(a(a(x1)))))	→	A(A(A(x1)))	(7)
A(a(x1))	→	x1	(20)
A(A(A(b(x1))))	→	a(a(a(a(C(x1)))))	(14)
C(C(C(C(x1))))	→	c(c(c(c(x1))))	(12)
c(C(x1))	→	x1	(23)
C(c(x1))	→	x1	(24)
c(c(c(c(c(x1)))))	→	C(C(C(x1)))	(11)
b(b(b(b(b(x1)))))	→	B(B(B(x1)))	(9)
B(a(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^#(a(a(C(x1))))	(78)
C^#(C(C(a(x1))))	→	c^#(c(c(c(B(x1)))))	(77)
B^#(B(B(B(x1))))	→	b^#(b(b(b(x1))))	(52)
C^#(C(C(a(x1))))	→	c^#(c(B(x1)))	(50)
A^#(C(x1))	→	b^#(x1)	(51)
B^#(a(a(a(a(x1)))))	→	A^#(A(A(x1)))	(76)
A^#(c(c(c(c(x1)))))	→	b^#(C(C(C(x1))))	(49)
C^#(C(C(C(x1))))	→	c^#(c(c(x1)))	(48)
C^#(C(C(C(x1))))	→	c^#(c(x1))	(75)
A^#(c(c(c(c(x1)))))	→	C^#(C(C(x1)))	(47)
c^#(c(c(c(c(x1)))))	→	C^#(x1)	(46)
b^#(b(b(b(b(x1)))))	→	B^#(B(x1))	(74)
C^#(b(b(b(b(x1)))))	→	a^#(B(B(B(x1))))	(45)
C^#(C(C(a(x1))))	→	B^#(x1)	(73)
b^#(c(x1))	→	A^#(x1)	(72)
a^#(a(a(a(a(x1)))))	→	A^#(A(x1))	(44)
B^#(a(a(a(a(x1)))))	→	c^#(A(A(A(x1))))	(71)
a^#(a(a(a(a(x1)))))	→	A^#(x1)	(43)
C^#(C(C(C(x1))))	→	c^#(x1)	(70)
A^#(A(A(b(x1))))	→	C^#(x1)	(69)
B^#(B(B(c(x1))))	→	b^#(b(A(x1)))	(68)
B^#(B(B(B(x1))))	→	b^#(b(b(x1)))	(67)
c^#(c(c(c(c(x1)))))	→	C^#(C(x1))	(42)
b^#(b(b(b(b(x1)))))	→	B^#(x1)	(41)
C^#(C(C(C(x1))))	→	c^#(c(c(c(x1))))	(40)
C^#(C(C(a(x1))))	→	c^#(c(c(B(x1))))	(39)
A^#(c(c(c(c(x1)))))	→	C^#(C(x1))	(65)
A^#(A(A(b(x1))))	→	a^#(a(C(x1)))	(66)
A^#(A(A(b(x1))))	→	a^#(a(a(a(C(x1)))))	(64)
a^#(b(x1))	→	C^#(x1)	(38)
B^#(a(a(a(a(x1)))))	→	A^#(x1)	(37)
B^#(B(B(B(x1))))	→	b^#(b(x1))	(63)
B^#(B(B(c(x1))))	→	A^#(x1)	(36)
B^#(B(B(c(x1))))	→	b^#(b(b(b(A(x1)))))	(62)
C^#(b(b(b(b(x1)))))	→	B^#(x1)	(35)
a^#(a(a(a(a(x1)))))	→	A^#(A(A(x1)))	(61)
C^#(C(C(a(x1))))	→	c^#(B(x1))	(34)
B^#(B(B(B(x1))))	→	b^#(x1)	(60)
C^#(b(b(b(b(x1)))))	→	B^#(B(x1))	(33)
A^#(A(A(A(x1))))	→	a^#(x1)	(59)
B^#(a(a(a(a(x1)))))	→	A^#(A(x1))	(58)
B^#(B(B(c(x1))))	→	b^#(A(x1))	(32)
A^#(c(c(c(c(x1)))))	→	C^#(x1)	(57)
A^#(A(A(A(x1))))	→	a^#(a(a(a(x1))))	(31)
A^#(A(A(A(x1))))	→	a^#(a(a(x1)))	(30)
c^#(c(c(c(c(x1)))))	→	C^#(C(C(x1)))	(56)
C^#(b(b(b(b(x1)))))	→	B^#(B(B(x1)))	(29)
c^#(a(x1))	→	B^#(x1)	(55)
b^#(b(b(b(b(x1)))))	→	B^#(B(B(x1)))	(54)
B^#(B(B(c(x1))))	→	b^#(b(b(A(x1))))	(28)
C^#(B(x1))	→	a^#(x1)	(27)
A^#(A(A(A(x1))))	→	a^#(a(x1))	(26)
B^#(A(x1))	→	c^#(x1)	(25)
A^#(A(A(b(x1))))	→	a^#(C(x1))	(53)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.