Certificate for #2343 ⟨a, b | abbaaab=aaa⟩

Completion settings:

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

Axiom: abbaaab=aaa.

Referenced by [3].

Axiom: abb=c.

Defines rule #1.

Referenced by [3], [4], [5].

Overlap of [1] abbaaab=aaa with [2] abb=c:

Critical pair: caaab=aaa.

Referenced by [4], [6].

Overlap of [3] caaab=aaa with [2] abb=c:

Critical pair: caac=aaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6].

Overlap of [4] aaab=caac with [2] abb=c:

Critical pair: aac=caacb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

Overlap of [3] caaab=aaa with [4] aaab=caac:

Critical pair: ccaac=aaa.

Defines rule #3.

Referenced by [7], [8].

Overlap of [6] ccaac=aaa with [5] caacb=aac:

Critical pair: ccaaaac=aaaaacb.

Flip LHS and RHS.

Defines rule #6.

Overlap of [6] ccaac=aaa with [6] ccaac=aaa:

Critical pair: ccaaaaa=aaacaac.

Flip LHS and RHS.

Defines rule #5.