Certification Problem

Input (TPDB SRS_Standard/Secret_07_SRS/num-514)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

a a a b a a b b a b →⁺ a b b a b b a b c b a b b a a a b a a b b a b c c c

The derivation can be derived as follows.

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