Certification Problem

Input (TPDB SRS_Standard/Waldmann_07_size12/size-12-alpha-3-num-95)

The rewrite relation of the following TRS is considered.

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

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 b b →⁺ ε c b b b b b b c

The derivation can be derived as follows.

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