Certificate for #2701 ⟨a, b | abbaa=abaab⟩

Completion settings:

• Auxiliary generators:
  1. c = abbaab
• Reduction order:
  • Left-to-right shortlex with b < a < c

Axiom: abbaa=abaab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5], [6], [7], [10], [12].

Axiom: abbaab=c.

Defines rule #7.

Referenced by [3], [4], [5], [6], [7], [9], [12].

Overlap of [2] abbaab=c with [2] abbaab=c:

Critical pair: abbac=cbaab.

Flip LHS and RHS.

Referenced by [8].

Overlap of [1] abaab=abbaa with [1] abaab=abbaa:

Critical pair: abaabbaa=abbaaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [12], [13], [14].

Overlap of [1] abaab=abbaa with [2] abbaab=c:

Critical pair: abac=abbaabaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [6], [7], [11], [13], [14].

Overlap of [2] abbaab=c with [1] abaab=abbaa:

Critical pair: abbaabbaa=caab.

Reduce LHS:

Reduce RHS:

Defines rule #1.

Referenced by [7], [8], [10], [11].

Overlap of [5] caab=abac with [2] abbaab=c:

Critical pair: cac=abacbaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Simplify [3] cbaab=abbac.

Reduce LHS:

Defines rule #5.

Referenced by [9], [10], [13], [14].

Overlap of [2] abbaab=c with [8] abacb=abbac:

Critical pair: abbaabbac=cacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [11].

Overlap of [8] abacb=abbac with [6] cbaa=abac:

Critical pair: abaabac=abbacaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [14].

Overlap of [9] cacb=cbac with [6] cbaa=abac:

Critical pair: caabac=cbacaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [1] abaab=abbaa with [4] abbaaaab=caa:

Critical pair: abacaa=abbaabaaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [4] abbaaaab=caa with [8] abacb=abbac:

Critical pair: abbaaaabbac=caaacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [5] caab=abac with [4] abbaaaab=caa:

Critical pair: cacaa=abacbaaaab.

Reduce RHS:

Defines rule #6.