Certificate for #9474 ⟨a, b | aa=1, abbabbbb=1⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with a < b

Axiom: aa=1.

Defines rule #1.

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

Axiom: abbabbbb=1.

Referenced by [3], [5].

Overlap of [1] aa=1 with [2] abbabbbb=1:

Critical pair: a=bbabbbb.

Flip LHS and RHS.

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

Overlap of [3] bbabbbb=a with [3] bbabbbb=a:

Critical pair: bbabba=aabbbb.

Reduce RHS:

Referenced by [5], [6].

Overlap of [2] abbabbbb=1 with [4] bbabba=bbbb:

Critical pair: abbabbbbbb=abba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [7].

Overlap of [3] bbabbbb=a with [4] bbabba=bbbb:

Critical pair: bbabbbbbb=aabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

Overlap of [3] bbabbbb=a with [6] bba=abb:

Critical pair: bbabbabb=aa.

Reduce LHS:

Reduce RHS:

Defines rule #3.