Certification Problem

Input (TPDB SRS_Standard/Trafo_06/dup13)

The rewrite relation of the following TRS is considered.

a(a(a(a(x1))))	→	a(a(b(b(b(b(b(b(x1))))))))	(1)
b(b(a(a(x1))))	→	b(b(b(b(c(c(x1))))))	(2)
a(a(b(b(b(b(c(c(x1))))))))	→	a(a(a(a(a(a(b(b(x1))))))))	(3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

a_a(a_a(a_a(a_a(x1))))	→	a_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))	(4)
a_a(a_a(a_a(a_b(x1))))	→	a_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))	(5)
a_a(a_a(a_a(a_c(x1))))	→	a_a(a_b(b_b(b_b(b_b(b_b(b_b(b_c(x1))))))))	(6)
b_b(b_a(a_a(a_a(x1))))	→	b_b(b_b(b_b(b_c(c_c(c_a(x1))))))	(7)
b_b(b_a(a_a(a_b(x1))))	→	b_b(b_b(b_b(b_c(c_c(c_b(x1))))))	(8)
b_b(b_a(a_a(a_c(x1))))	→	b_b(b_b(b_b(b_c(c_c(c_c(x1))))))	(9)
a_a(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a(a_a(a_a(a_a(a_a(a_b(b_b(b_a(x1))))))))	(10)
a_a(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a(a_a(a_a(a_a(a_a(a_b(b_b(b_b(x1))))))))	(11)
a_a(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a(a_a(a_a(a_a(a_a(a_b(b_b(b_c(x1))))))))	(12)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[a_a(x₁)]	=	1 · x₁
[a_b(x₁)]	=	1 · x₁
[b_b(x₁)]	=	1 · x₁
[b_a(x₁)]	=	1 · x₁
[a_c(x₁)]	=	1 · x₁ + 1
[b_c(x₁)]	=	1 · x₁
[c_c(x₁)]	=	1 · x₁
[c_a(x₁)]	=	1 · x₁
[c_b(x₁)]	=	1 · x₁

all of the following rules can be deleted.

a_a(a_a(a_a(a_c(x1))))	→	a_a(a_b(b_b(b_b(b_b(b_b(b_b(b_c(x1))))))))	(6)
b_b(b_a(a_a(a_c(x1))))	→	b_b(b_b(b_b(b_c(c_c(c_c(x1))))))	(9)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a_a^#(a_a(a_a(a_a(x1))))	→	a_a^#(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))	(13)
a_a^#(a_a(a_a(a_a(x1))))	→	b_b^#(b_b(b_b(b_b(b_b(b_a(x1))))))	(14)
a_a^#(a_a(a_a(a_a(x1))))	→	b_b^#(b_b(b_b(b_b(b_a(x1)))))	(15)
a_a^#(a_a(a_a(a_a(x1))))	→	b_b^#(b_b(b_b(b_a(x1))))	(16)
a_a^#(a_a(a_a(a_a(x1))))	→	b_b^#(b_b(b_a(x1)))	(17)
a_a^#(a_a(a_a(a_a(x1))))	→	b_b^#(b_a(x1))	(18)
a_a^#(a_a(a_a(a_b(x1))))	→	a_a^#(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))	(19)
a_a^#(a_a(a_a(a_b(x1))))	→	b_b^#(b_b(b_b(b_b(b_b(b_b(x1))))))	(20)
a_a^#(a_a(a_a(a_b(x1))))	→	b_b^#(b_b(b_b(b_b(b_b(x1)))))	(21)
a_a^#(a_a(a_a(a_b(x1))))	→	b_b^#(b_b(b_b(b_b(x1))))	(22)
a_a^#(a_a(a_a(a_b(x1))))	→	b_b^#(b_b(b_b(x1)))	(23)
a_a^#(a_a(a_a(a_b(x1))))	→	b_b^#(b_b(x1))	(24)
a_a^#(a_a(a_a(a_b(x1))))	→	b_b^#(x1)	(25)
b_b^#(b_a(a_a(a_a(x1))))	→	b_b^#(b_b(b_b(b_c(c_c(c_a(x1))))))	(26)
b_b^#(b_a(a_a(a_a(x1))))	→	b_b^#(b_b(b_c(c_c(c_a(x1)))))	(27)
b_b^#(b_a(a_a(a_a(x1))))	→	b_b^#(b_c(c_c(c_a(x1))))	(28)
b_b^#(b_a(a_a(a_b(x1))))	→	b_b^#(b_b(b_b(b_c(c_c(c_b(x1))))))	(29)
b_b^#(b_a(a_a(a_b(x1))))	→	b_b^#(b_b(b_c(c_c(c_b(x1)))))	(30)
b_b^#(b_a(a_a(a_b(x1))))	→	b_b^#(b_c(c_c(c_b(x1))))	(31)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_a(x1))))))))	(32)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_a(x1)))))))	(33)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_a(x1))))))	(34)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_b(b_b(b_a(x1)))))	(35)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_b(b_b(b_a(x1))))	(36)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	b_b^#(b_a(x1))	(37)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_b(x1))))))))	(38)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_b(x1)))))))	(39)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_b(x1))))))	(40)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_b(b_b(b_b(x1)))))	(41)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_b(b_b(b_b(x1))))	(42)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	b_b^#(b_b(x1))	(43)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	b_b^#(x1)	(44)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_c(x1))))))))	(45)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_c(x1)))))))	(46)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_c(x1))))))	(47)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_b(b_b(b_c(x1)))))	(48)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_b(b_b(b_c(x1))))	(49)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	b_b^#(b_c(x1))	(50)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_a(x1))))))))	(32)
a_a^#(a_a(a_a(a_a(x1))))	→	a_a^#(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))	(13)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_a(x1)))))))	(33)
a_a^#(a_a(a_a(a_b(x1))))	→	a_a^#(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))	(19)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_a(x1))))))	(34)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_b(b_b(b_a(x1)))))	(35)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_b(b_b(b_a(x1))))	(36)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_b(x1))))))))	(38)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_b(x1)))))))	(39)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_b(x1))))))	(40)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_b(b_b(b_b(x1)))))	(41)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_b(b_b(b_b(x1))))	(42)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_c(x1))))))))	(45)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_c(x1)))))))	(46)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_c(x1))))))	(47)

1.1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[a_a^#(x₁)]	=	2 · x₁
[a_b(x₁)]	=	x₁
[b_b(x₁)]	=	-1 + x₁
[b_a(x₁)]	=	2 + x₁
[a_a(x₁)]	=	x₁
[b_c(x₁)]	=	2 + x₁
[c_c(x₁)]	=	2 + x₁
[c_a(x₁)]	=	x₁
[c_b(x₁)]	=	x₁

the pairs

a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_b(x1))))))))	(38)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_b(x1)))))))	(39)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_b(x1))))))	(40)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_a(a_b(b_b(b_b(x1)))))	(41)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_b(x1))))))))	→	a_a^#(a_b(b_b(b_b(x1))))	(42)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_c(x1))))))))	(45)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_c(x1)))))))	(46)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_c(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_c(x1))))))	(47)

could be deleted.

1.1.1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the integers

[a_a^#(x₁)]

1	0	0
0	0	0
0	0	0

· x₁

[a_b(x₁)]

0	1	0
1	1	1
0	1	0

· x₁

[b_b(x₁)]

0	1	0
0	0	1
1	0	0

· x₁

[b_c(x₁)]

0	0	0
1	0	0
0	1	0

· x₁

[c_c(x₁)]

1	1	0
0	0	0
0	0	0

· x₁

[c_a(x₁)]

0	1	0
0	0	0
1	1	1

· x₁

[a_a(x₁)]

1	0	0
0	1	1
0	0	0

· x₁

[b_a(x₁)]

0	0	0
0	0	0
0	1	0

· x₁

[c_b(x₁)]

1	1	1
0	1	0
1	1	1

· x₁

the pairs

a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_a(a_b(b_b(b_a(x1))))))))	(32)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_a(a_b(b_b(b_a(x1)))))))	(33)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_a(a_b(b_b(b_a(x1))))))	(34)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_a(a_b(b_b(b_a(x1)))))	(35)
a_a^#(a_b(b_b(b_b(b_b(b_c(c_c(c_a(x1))))))))	→	a_a^#(a_b(b_b(b_a(x1))))	(36)

could be deleted.

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.