Certification Problem

Input (TPDB SRS_Standard/Waldmann_07_size11/size-11-alpha-3-num-1)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

c c b c b c b c →⁺ b c b b c b b c b c c b c b c b c ε

The derivation can be derived as follows.

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