Certification Problem

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

The rewrite relation of the following TRS is considered.

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

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

The derivation can be derived as follows.

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