Certificate for #5075 ⟨a, b | aaabbaa=abba⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with b < a

Axiom: aaabbaa=abba.

Defines rule #1.

Referenced by [2].

Overlap of [1] aaabbaa=abba with [1] aaabbaa=abba:

Critical pair: aaabbabba=abbaabbaa.

Defines rule #2.