Certification Problem

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

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

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

The derivation can be derived as follows.

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