Certification Problem

Input (TPDB SRS_Standard/Secret_06_SRS/1-matchbox)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Looping derivation

There is a looping derivation.

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

The derivation can be derived as follows.

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