Certificate for #9478 ⟨a, b | aa=1, abbbabbb=1⟩

Completion settings:

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

Axiom: aa=1.

Defines rule #5.

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

Axiom: abbbabbb=1.

Referenced by [4].

Axiom: abbba=c.

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

Overlap of [2] abbbabbb=1 with [3] abbba=c:

Critical pair: cbbb=1.

Referenced by [7], [9].

Overlap of [1] aa=1 with [3] abbba=c:

Critical pair: ac=bbba.

Flip LHS and RHS.

Defines rule #4.

Overlap of [3] abbba=c with [1] aa=1:

Critical pair: abbb=ca.

Flip LHS and RHS.

Defines rule #3.

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

Critical pair: abbbc=cbbba.

Reduce RHS:

Referenced by [8].

Overlap of [1] aa=1 with [7] abbbc=a:

Critical pair: aa=bbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

Overlap of [4] cbbb=1 with [8] bbbc=1:

Critical pair: cb=bc.

Defines rule #1.