Certificate for #4679 ⟨a, b | aabbaaab=aaa⟩

Completion settings:

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

Axiom: aabbaaab=aaa.

Referenced by [3].

Axiom: aabb=c.

Defines rule #3.

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

Overlap of [1] aabbaaab=aaa with [2] aabb=c:

Critical pair: caaab=aaa.

Referenced by [4], [6].

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

Critical pair: cac=aaab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6].

Overlap of [4] aaab=cac with [2] aabb=c:

Critical pair: ac=cacb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

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

Critical pair: ccac=aaa.

Defines rule #1.

Referenced by [7], [8].

Overlap of [6] ccac=aaa with [5] cacb=ac:

Critical pair: ccaac=aaaacb.

Flip LHS and RHS.

Defines rule #6.

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

Critical pair: ccaaaa=aaacac.

Flip LHS and RHS.

Defines rule #5.