Certificate for #4154 ⟨a, b | aabbaaaab=bb⟩

Completion settings:

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

Axiom: aabbaaaab=bb.

Referenced by [3].

Axiom: aaaab=c.

Defines rule #3.

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

Overlap of [1] aabbaaaab=bb with [2] aaaab=c:

Critical pair: aabbc=bb.

Referenced by [4], [6], [7].

Overlap of [2] aaaab=c with [3] aabbc=bb:

Critical pair: aabb=cbc.

Defines rule #1.

Referenced by [5], [6], [7].

Overlap of [2] aaaab=c with [4] aabb=cbc:

Critical pair: aacbc=cb.

Defines rule #4.

Referenced by [8].

Overlap of [3] aabbc=bb with [4] aabb=cbc:

Critical pair: cbcc=bb.

Defines rule #2.

Referenced by [7], [8].

Overlap of [3] aabbc=bb with [6] cbcc=bb:

Critical pair: aabbbb=bbbcc.

Reduce LHS:

Defines rule #5.

Overlap of [5] aacbc=cb with [6] cbcc=bb:

Critical pair: aacbbb=cbbcc.

Defines rule #6.