Certification Problem

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

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

The derivation can be derived as follows.

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