Certificate for #16324 ⟨a, b | aab=bb, bbaa=bb⟩

Completion settings:

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

Axiom: aab=bb.

Referenced by [4].

Axiom: bbaa=bb.

Referenced by [5].

Axiom: bb=c.

Defines rule #3.

Referenced by [4], [5], [6], [7], [8], [11].

Simplify [1] aab=bb.

Reduce RHS:

Defines rule #5.

Referenced by [8], [9], [10].

Simplify [2] bbaa=bb.

Reduce RHS:

Referenced by [6].

Overlap of [5] bbaa=c with [3] bb=c:

Critical pair: caa=c.

Defines rule #6.

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

Overlap of [3] bb=c with [3] bb=c:

Critical pair: bc=cb.

Referenced by [14].

Overlap of [4] aab=c with [3] bb=c:

Critical pair: aac=cb.

Referenced by [12].

Overlap of [6] caa=c with [4] aab=c:

Critical pair: cc=cb.

Flip LHS and RHS.

Defines rule #1.

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

Overlap of [6] caa=c with [4] aab=c:

Critical pair: cac=cab.

Flip LHS and RHS.

Defines rule #7.

Overlap of [9] cb=cc with [3] bb=c:

Critical pair: cc=ccb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Simplify [8] aac=cb.

Reduce RHS:

Defines rule #4.

Referenced by [13].

Overlap of [6] caa=c with [12] aac=cc:

Critical pair: cacc=cac.

Defines rule #9.

Simplify [7] bc=cb.

Reduce RHS:

Defines rule #2.