Certification Problem

Input (TPDB SRS_Standard/Secret_06_SRS/multum4)

The rewrite relation of the following TRS is considered.

b(b(a(b(b(a(b(b(b(b(b(b(a(b(x1))))))))))))))

→

b(b(b(b(b(a(b(b(a(b(b(a(b(b(b(b(b(b(x1))))))))))))))))))

(1)

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

b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b(b_b(b_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))))))))))))	(2)
b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b(b_b(b_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))))))))))))	(3)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_b(b_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))))))))))))	(4)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1)))))))))))))))))	(5)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))))))))))	(6)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1)))))))))))))))	(7)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))))))	(8)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1)))))))))	(9)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_b(b_b(b_b(b_b(b_b(x1))))))	(10)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_b(b_b(b_b(b_b(x1)))))	(11)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_b(b_b(b_b(x1))))	(12)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_b(b_b(x1)))	(13)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_b(x1))	(14)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_b(b_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))))))))))))	(15)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1)))))))))))))))))	(16)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))))))))))	(17)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1)))))))))))))))	(18)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))))))	(19)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1)))))))))	(20)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_b(b_b(b_b(b_b(b_a(x1))))))	(21)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_b(b_b(b_b(b_a(x1)))))	(22)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_b(b_b(b_a(x1))))	(23)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_b(b_a(x1)))	(24)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_a(x1))	(25)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_a(x1))	(25)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))))))	(19)

1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[b_b^#(x₁)]	=	1 · x₁
[b_a(x₁)]	=	1 · x₁
[a_b(x₁)]	=	1 + 1 · x₁
[b_b(x₁)]	=	1 · x₁

the pairs

b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_a(x1))	(25)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_a(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(x1))))))))))))	(19)

could be deleted.

1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))))))	(8)
b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))	→	b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1)))))))))))))))	(7)

1.1.1.2 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[b_b^#(x₁)]	=	1 · x₁
[b_a(x₁)]	=	1 + 1 · x₁
[a_b(x₁)]	=	1 · x₁
[b_b(x₁)]	=	1 · x₁

the pair

b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_a(a_b(b_b(x1))))))))))))))

→

b_b^#(b_a(a_b(b_b(b_a(a_b(b_b(b_b(b_b(b_b(b_b(b_b(x1))))))))))))

(8)

could be deleted.

1.1.1.2.1 Semantic Labeling Processor

The following interpretations form a model of the rules.

As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

[b_b(x₁)]	=	0
[b_a(x₁)]	=	1
[b_b^#(x₁)]	=	0
[a_b(x₁)]	=	0

We obtain the set of labeled pairs

b_b^#₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₀(b_b₀(x1))))))))))))))	→	b_b^#₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₀(x1)))))))))))))))	(26)
b_b^#₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₀(b_b₁(x1))))))))))))))	→	b_b^#₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(x1)))))))))))))))	(27)

and the set of labeled rules:

b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₀(b_b₀(x1))))))))))))))	→	b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₀(x1))))))))))))))))))	(28)
b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₀(b_b₁(x1))))))))))))))	→	b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(x1))))))))))))))))))	(29)
b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₁(b_a₀(x1))))))))))))))	→	b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(x1))))))))))))))))))	(30)
b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₁(b_a₁(x1))))))))))))))	→	b_b₀(b_b₀(b_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₁(b_a₀(a_b₀(b_b₀(b_b₀(b_b₀(b_b₀(b_b₁(b_a₁(x1))))))))))))))))))	(31)

1.1.1.2.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.