Certification Problem

Input (TPDB SRS_Standard/Secret_07_SRS/num-519)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

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

The derivation can be derived as follows.

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