Certificate for #5342 ⟨a, b | ababaab=aabb⟩

Completion settings:

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

Axiom: ababaab=aabb.

Defines rule #1.

Referenced by [2].

Overlap of [1] ababaab=aabb with [1] ababaab=aabb:

Critical pair: ababaaabb=aabbabaab.

Defines rule #2.