Certification Problem

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

The rewrite relation of the following TRS is considered.

a(x1)	→	b(x1)	(1)
a(c(x1))	→	x1	(2)
c(b(b(x1)))	→	a(a(a(c(c(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 b b b b b b →⁺ a a a c b b b b b b c c c

The derivation can be derived as follows.

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