Certification Problem

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

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

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

The derivation can be derived as follows.

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