Certification Problem

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

The rewrite relation of the following TRS is considered.

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

The derivation can be derived as follows.

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