Certification Problem

Input (TPDB SRS_Standard/Waldmann_19/random-400)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

a b a a a b b a a b a b b a a a b b b →⁺ ε a b a a a b b a a b a b b a a a b b b ε

The derivation can be derived as follows.

a b a a →⁺ a b b b: This is an original rule (OC1).
b b a b →⁺ a a a a: This is an original rule (OC1).
a b a a a b →⁺ a b a a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- a b a a →⁺ a b b b
- b b a b →⁺ a a a a
a b a a →⁺ b a b b: This is an original rule (OC1).
a b a a a b →⁺ b a a a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- a b a a →⁺ b a b b
- b b a b →⁺ a a a a
b b a b b a a a b →⁺ a a a b a a a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- b b a b →⁺ a a a a
- a b a a a b →⁺ b a a a a a
b b a b b a a a b →⁺ a a b a b b a a a: The overlap closure is obtained from the following two overlap closures (OC3).
- b b a b b a a a b →⁺ a a a b a a a a a
- a b a a →⁺ b a b b
a b a a b a b b a a a b →⁺ b a b a a b a b b a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- a b a a →⁺ b a b b
- b b a b b a a a b →⁺ a a b a b b a a a
a b a a b a b b a a a b →⁺ b b a b b b a b b a a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b →⁺ b a b a a b a b b a a a
- a b a a →⁺ b a b b
a b a a b a b b a a a b →⁺ b b a b a a a a b a a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b →⁺ b b a b b b a b b a a a
- b b a b →⁺ a a a a
a b a a b a b b a a a b →⁺ b b b a b b a a b a a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b →⁺ b b a b a a a a b a a a
- a b a a →⁺ b a b b
a b a a b a b b a a a b →⁺ b b b a b b a b a b b a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b →⁺ b b b a b b a a b a a a
- a b a a →⁺ b a b b
a b a a b a b b a a a b b →⁺ b b b a b b a b a a a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- a b a a b a b b a a a b →⁺ b b b a b b a b a b b a
- b b a b →⁺ a a a a
a b a a b a b b a a a b b →⁺ b b b a b b b a b b a a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b →⁺ b b b a b b a b a a a a a
- a b a a →⁺ b a b b
a b a a b a b b a a a b b →⁺ b b b a b a a a a b a a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b →⁺ b b b a b b b a b b a a a
- b b a b →⁺ a a a a
a b a a b a b b a a a b b →⁺ b b b a b b b a a b a a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b →⁺ b b b a b a a a a b a a a
- a b a a →⁺ a b b b
a b a a b a b b a a a b b →⁺ b b b a b b b a a b b b a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b →⁺ b b b a b b b a a b a a a
- a b a a →⁺ a b b b
a b a a b a b b a a a b b b →⁺ b b b a b b b a a b a a a a: The overlap closure is obtained from the following two overlap closures (OC2).
- a b a a b a b b a a a b b →⁺ b b b a b b b a a b b b a
- b b a b →⁺ a a a a
a b a a b a b b a a a b b b →⁺ b b b a b b b a b a b b a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b b →⁺ b b b a b b b a a b a a a a
- a b a a →⁺ b a b b
a b a a b a b b a a a b b b →⁺ b b b a b a a a a a b b a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b b →⁺ b b b a b b b a b a b b a a
- b b a b →⁺ a a a a
a b a a b a b b a a a b b b →⁺ b b b b a b b a a a b b a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b b →⁺ b b b a b a a a a a b b a a
- a b a a →⁺ b a b b
a b a a b a b b a a a b b b →⁺ b b a a a a b a a a b b a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b b →⁺ b b b b a b b a a a b b a a
- b b a b →⁺ a a a a
a b a a b a b b a a a b b b →⁺ b b a a a b a b b a b b a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b b →⁺ b b a a a a b a a a b b a a
- a b a a →⁺ b a b b
a b a a b a b b a a a b b b →⁺ b b a a a b a a a a a b a a: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b b →⁺ b b a a a b a b b a b b a a
- b b a b →⁺ a a a a
a b a a b a b b a a a b b b →⁺ b b a a a b a a a a a b b b: The overlap closure is obtained from the following two overlap closures (OC2).
- a b a a b a b b a a a b b b →⁺ b b a a a b a a a a a b a a
- a b a a →⁺ a b b b
a b a a b a b b a a a b b b →⁺ b b a a b a b b a a a b b b: The overlap closure is obtained from the following two overlap closures (OC3).
- a b a a b a b b a a a b b b →⁺ b b a a a b a a a a a b b b
- a b a a →⁺ b a b b
a b a a a b b a a b a b b a a a b b b →⁺ a b a a a b b a a b a b b a a a b b b: The overlap closure is obtained from the following two overlap closures (OC2).
- a b a a a b →⁺ a b a a a a
- a b a a b a b b a a a b b b →⁺ b b a a b a b b a a a b b b