Certificate for #5730 ⟨a, b | aaaa=1, bbabb=a⟩

Completion settings:

• Auxiliary generators:
  1. c = bb
• Reduction order:
  • Left-to-right recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1

Axiom: aaaa=1.

Defines rule #3.

Referenced by [9].

Axiom: bbabb=a.

Referenced by [4].

Axiom: bb=c.

Defines rule #6.

Referenced by [4], [5].

Overlap of [2] bbabb=a with [3] bb=c:

Critical pair: cabb=a.

Reduce LHS:

Defines rule #2.

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

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

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

Overlap of [4] cac=a with [4] cac=a:

Critical pair: caa=aac.

Defines rule #1.

Referenced by [9].

Overlap of [4] cac=a with [5] cb=bc:

Critical pair: cabc=ab.

Referenced by [8].

Overlap of [7] cabc=ab with [4] cac=a:

Critical pair: caba=abac.

Referenced by [9].

Overlap of [8] caba=abac with [1] aaaa=1:

Critical pair: cab=abacaaa.

Reduce RHS:

Defines rule #5.