Certification Problem

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

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 b b b c b b →⁺ ε a b b b c b b c a

The derivation can be derived as follows.

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