Certificate for #2707 ⟨a, b | abbab=aabba⟩

Completion settings:

• Reduction order:
  • Right-to-left shortlex with a < b

Axiom: abbab=aabba.

Defines rule #1.

Referenced by [2].

Overlap of [1] abbab=aabba with [1] abbab=aabba:

Critical pair: abbaabba=aabbabab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.